Proofgold Proof

pf
Let x0 of type ι be given. Assume H0: RealsStruct x0. Apply Field_of_RealsStruct_0 with x0, λ x1 x2 . ∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ omega ⟶ CRing_with_id_omega_exp (Field_of_RealsStruct x0) x3 x4 ∈ x1. Apply CRing_with_id_omega_exp_clos with Field_of_RealsStruct x0. Apply Field_of_RealsStruct_is_CRing_with_id with x0. The subproof is completed by applying H0. ■