Let x0 of type ι be given.
Apply Field_of_RealsStruct_0 with
x0,
λ x1 x2 . ∀ x3 . x3 ∈ x1 ⟶ 4a41c.. (Field_of_RealsStruct x0) x3 1 = x3.
Apply unknownprop_d42950c3f12a0a1bd59ad028e6131cf8cd8c077fb27dae2f0fb2adeb65747c62 with
Field_of_RealsStruct x0.
Apply Field_of_RealsStruct_is_CRing_with_id with
x0.
The subproof is completed by applying H0.