Let x0 of type ι be given.
Apply RealsStruct_minus_mult with
x0,
Field_minus (Field_of_RealsStruct x0) (RealsStruct_one x0),
λ x1 x2 . x1 = RealsStruct_one x0 leaving 3 subgoals.
The subproof is completed by applying H0.
Apply RealsStruct_minus_one_In with
x0.
The subproof is completed by applying H0.
Apply RealsStruct_minus_invol with
x0,
RealsStruct_one x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply RealsStruct_one_In with
x0.
The subproof is completed by applying H0.