Let x0 of type ι be given.

Assume H0: x0 ∈ octonion.

Apply octonion_E with x0, OSNo_proj1 x0 ∈ quaternion 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_proj1 x4 ∈ quaternion.

Apply octonion_p1_eq with x1, x2, λ x3 x4 . x4 ∈ quaternion leaving 3 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H2.

■

Proofgold Proof