Let x0 of type ι be given.

Assume H0: x0 ∈ quaternion.

Apply quaternion_E with x0, HSNo x0 leaving 2 subgoals.

The subproof is completed by applying H0.

Let x1 of type ι be given.

Assume H1: x1 ∈ complex.

Let x2 of type ι be given.

Assume H2: x2 ∈ complex.

Assume H3: x0 = CSNo_pair x1 x2.

Apply H3 with λ x3 x4 . HSNo x4.

Apply HSNo_I with x1, x2 leaving 2 subgoals.

Apply complex_CSNo with x1.

The subproof is completed by applying H1.

Apply complex_CSNo with x2.

The subproof is completed by applying H2.

■

Proofgold Proof