Let x0 of type ι be given.

Assume H0: x0 ∈ octonion.

Apply octonion_E with x0, OSNo x0 leaving 2 subgoals.

The subproof is completed by applying H0.

Let x1 of type ι be given.

Assume H1: x1 ∈ quaternion.

Let x2 of type ι be given.

Assume H2: x2 ∈ quaternion.

Assume H3: x0 = HSNo_pair x1 x2.

Apply H3 with λ x3 x4 . OSNo x4.

Apply OSNo_I with x1, x2 leaving 2 subgoals.

Apply quaternion_HSNo with x1.

The subproof is completed by applying H1.

Apply quaternion_HSNo with x2.

The subproof is completed by applying H2.

■

Proofgold Proof