Let x0 of type ι be given.
Apply Field_of_RealsStruct_4 with
x0,
λ x1 x2 . ∀ x3 . 4a41c.. (Field_of_RealsStruct x0) x3 0 = x1.
Apply unknownprop_4ab72f93767fc325730724758d3093e7af2a82217c4d5ee8a2692818e418bf07 with
Field_of_RealsStruct x0.
Apply Field_of_RealsStruct_is_CRing_with_id with
x0.
The subproof is completed by applying H0.