Let x0 of type ι be given.
Apply Field_of_RealsStruct_2f with
x0,
λ x1 x2 : ι → ι → ι . ∀ x3 x4 . x4 ∈ omega ⟶ 4a41c.. (Field_of_RealsStruct x0) x3 (ordsucc x4) = x1 x3 (4a41c.. (Field_of_RealsStruct x0) x3 x4) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_99ced72b0a1cc72e56a6449ae7f85ace98b316636257ef59b14e002a0cde881d with
Field_of_RealsStruct x0.
Apply Field_of_RealsStruct_is_CRing_with_id with
x0.
The subproof is completed by applying H0.