Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Assume H0: x2 ∈ omega.

Let x3 of type ι be given.

Assume H1: ap x3 0 = x0.

Assume H2: ap x3 x2 = x1.

Assume H3: ∀ x4 . x4 ∈ ordsucc x2 ⟶ Field (ap x3 x4).

Assume H4: ∀ x4 . x4 ∈ x2 ⟶ ∃ x5 . and (x5 ∈ field0 (ap x3 (ordsucc x4))) (∃ x6 . and (x6 ∈ omega) (and (CRing_with_id_omega_exp (ap x3 (ordsucc x4)) x5 x6 ∈ field0 (ap x3 x4)) (Field_extension_by_1 (ap x3 x4) (ap x3 (ordsucc x4)) x5))).

Let x4 of type ο be given.

Assume H5: ∀ x5 . and (x5 ∈ omega) (∃ x6 . and (and (and (ap x6 0 = x0) (ap x6 x5 = x1)) (∀ x7 . x7 ∈ ordsucc x5 ⟶ Field (ap x6 x7))) (∀ x7 . x7 ∈ x5 ⟶ ∃ x8 . and (x8 ∈ field0 (ap x6 (ordsucc x7))) (∃ x9 . and (x9 ∈ omega) (and (CRing_with_id_omega_exp (ap x6 (ordsucc x7)) x8 x9 ∈ field0 (ap x6 x7)) (Field_extension_by_1 (ap x6 x7) (ap x6 (ordsucc x7)) x8))))) ⟶ x4.

Apply H5 with x2.

Apply andI with x2 ∈ omega, ∃ x5 . and (and (and (ap x5 0 = x0) (ap x5 x2 = x1)) (∀ x6 . x6 ∈ ordsucc x2 ⟶ Field (ap x5 x6))) (∀ x6 . x6 ∈ x2 ⟶ ∃ x7 . and (x7 ∈ field0 (ap x5 (ordsucc x6))) (∃ x8 . and (x8 ∈ omega) (and (CRing_with_id_omega_exp (ap x5 (ordsucc x6)) x7 x8 ∈ field0 (ap x5 x6)) (Field_extension_by_1 (ap x5 x6) (ap x5 (ordsucc x6)) x7)))) leaving 2 subgoals.

The subproof is completed by applying H0.

Let x5 of type ο be given.

Assume H6: ∀ x6 . and (and (and (ap x6 0 = x0) (ap x6 x2 = x1)) (∀ x7 . x7 ∈ ordsucc x2 ⟶ Field (ap x6 x7))) (∀ x7 . ... ∈ ... ⟶ ∃ x8 . and (x8 ∈ field0 (ap x6 (ordsucc x7))) (∃ x9 . and (x9 ∈ omega) (and (CRing_with_id_omega_exp (ap x6 (ordsucc x7)) x8 x9 ∈ field0 (ap x6 x7)) (Field_extension_by_1 (ap x6 x7) (ap x6 (ordsucc x7)) x8)))) ⟶ x5.

...

■

Proofgold Proof