Apply equip_sym with real, prim4 omega, False leaving 2 subgoals.

The subproof is completed by applying equip_real_Power_omega.

Let x0 of type ι → ι be given.

Assume H1: bij (prim4 omega) real x0.

Apply H0 with False.

Let x1 of type ι → ι be given.

Assume H2: inj real omega x1.

Apply form100_22_v2 with λ x2 . x1 (x0 x2).

Apply inj_comp with prim4 omega, real, omega, x0, x1 leaving 2 subgoals.

Apply bij_inj with prim4 omega, real, x0.

The subproof is completed by applying H1.

The subproof is completed by applying H2.

■

Proofgold Proof