Let x0 of type ι be given.

Assume H0: RealsStruct x0.

Apply Field_of_RealsStruct_0 with x0, λ x1 x2 . ∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ setminus x1 (Sing (field4 x0)) ⟶ x3 = field2b x0 x4 (Field_div (Field_of_RealsStruct x0) x3 x4).

Apply Field_of_RealsStruct_2f with x0, λ x1 x2 : ι → ι → ι . ∀ x3 . x3 ∈ ap (Field_of_RealsStruct x0) 0 ⟶ ∀ x4 . x4 ∈ setminus (ap (Field_of_RealsStruct x0) 0) (Sing (field4 x0)) ⟶ x3 = x1 x4 (Field_div (Field_of_RealsStruct x0) x3 x4) leaving 2 subgoals.

The subproof is completed by applying H0.

Apply Field_of_RealsStruct_3 with x0, λ x1 x2 . ∀ x3 . x3 ∈ ap (Field_of_RealsStruct x0) 0 ⟶ ∀ x4 . x4 ∈ setminus (ap (Field_of_RealsStruct x0) 0) (Sing x1) ⟶ x3 = (λ x5 . ap (ap (ap (Field_of_RealsStruct x0) 2) x5)) x4 (Field_div (Field_of_RealsStruct x0) x3 x4).

Apply Field_mult_div with Field_of_RealsStruct x0.

Apply Field_Field_of_RealsStruct with x0.

The subproof is completed by applying H0.

■

Proofgold Proof