Let x0 of type ι be given.

Assume H0: RealsStruct x0.

Apply Field_of_RealsStruct_1f with x0, λ x1 x2 : ι → ι → ι . ∀ x3 . x3 ∈ field0 x0 ⟶ ∀ x4 . x4 ∈ field0 x0 ⟶ ∀ x5 . x5 ∈ field0 x0 ⟶ field2b x0 (x1 x3 x4) x5 = x1 (field2b x0 x3 x5) (field2b x0 x4 x5) leaving 2 subgoals.

The subproof is completed by applying H0.

Apply Field_of_RealsStruct_2f with x0, λ x1 x2 : ι → ι → ι . ∀ x3 . x3 ∈ field0 x0 ⟶ ∀ x4 . x4 ∈ field0 x0 ⟶ ∀ x5 . x5 ∈ field0 x0 ⟶ x1 ((λ x6 . ap (ap (ap (Field_of_RealsStruct x0) 1) x6)) x3 x4) x5 = (λ x6 . ap (ap (ap (Field_of_RealsStruct x0) 1) x6)) (x1 x3 x5) (x1 x4 x5) leaving 2 subgoals.

The subproof is completed by applying H0.

Apply explicit_Field_dist_R with field0 x0, ap (Field_of_RealsStruct x0) 3, ap (Field_of_RealsStruct x0) 4, decode_b (ap (Field_of_RealsStruct x0) 1), decode_b (ap (Field_of_RealsStruct x0) 2).

Apply explicit_Field_of_RealsStruct_2 with x0.

The subproof is completed by applying H0.

■

Proofgold Proof