Let x0 of type ι be given.

Assume H0: RealsStruct x0.

Apply explicit_Nats_E with RealsStruct_N x0, field4 x0, λ x1 . field1b x0 x1 (RealsStruct_one x0), ∀ x1 . x1 ∈ omega ⟶ RealsStruct_omega_embedding x0 x1 ∈ RealsStruct_N x0 leaving 2 subgoals.

Assume H1: explicit_Nats (RealsStruct_N x0) (field4 x0) (λ x1 . field1b x0 x1 (RealsStruct_one x0)).

Assume H2: field4 x0 ∈ RealsStruct_N x0.

Assume H3: ∀ x1 . x1 ∈ RealsStruct_N x0 ⟶ (λ x2 . field1b x0 x2 (RealsStruct_one x0)) x1 ∈ RealsStruct_N x0.

Assume H4: ∀ x1 . x1 ∈ RealsStruct_N x0 ⟶ (λ x2 . field1b x0 x2 (RealsStruct_one x0)) x1 = field4 x0 ⟶ ∀ x2 : ο . x2.

Assume H5: ∀ x1 . x1 ∈ RealsStruct_N x0 ⟶ ∀ x2 . x2 ∈ RealsStruct_N x0 ⟶ (λ x3 . field1b x0 x3 (RealsStruct_one x0)) x1 = (λ x3 . field1b x0 x3 (RealsStruct_one x0)) x2 ⟶ x1 = x2.

Assume H6: ∀ x1 : ι → ο . x1 (field4 x0) ⟶ (∀ x2 . x1 x2 ⟶ x1 ((λ x3 . field1b x0 x3 (RealsStruct_one x0)) x2)) ⟶ ∀ x2 . x2 ∈ RealsStruct_N x0 ⟶ x1 x2.

Claim L7: ∀ x1 . nat_p x1 ⟶ RealsStruct_omega_embedding x0 x1 ∈ RealsStruct_N x0

Apply nat_ind with λ x1 . RealsStruct_omega_embedding x0 x1 ∈ RealsStruct_N x0 leaving 2 subgoals.

Apply nat_primrec_0 with field4 x0, λ x1 x2 . field1b x0 x2 (RealsStruct_one x0), λ x1 x2 . x2 ∈ RealsStruct_N x0.

The subproof is completed by applying H2.

Let x1 of type ι be given.

Assume H7: nat_p x1.

Assume H8: RealsStruct_omega_embedding x0 x1 ∈ RealsStruct_N x0.

Apply nat_primrec_S with field4 x0, λ x2 x3 . field1b x0 x3 (RealsStruct_one x0), x1, λ x2 x3 . x3 ∈ RealsStruct_N x0 leaving 2 subgoals.

The subproof is completed by applying H7.

Apply H3 with RealsStruct_omega_embedding x0 x1.

The subproof is completed by applying H8.

Let x1 of type ι be given.

Assume H8: x1 ∈ omega.

Apply L7 with x1.

Apply omega_nat_p with x1.

The subproof is completed by applying H8.

Apply RealsStruct_natOfOrderedField with x0.

The subproof is completed by applying H0.

■

Proofgold Proof