Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply RealsStruct_minus_one_In with
x0.
The subproof is completed by applying H0.
Claim L4: ∀ x5 : ι → ο . x5 y4 ⟶ x5 y3
Let x5 of type ι → ο be given.
Claim L5: ∀ x8 : ι → ο . x8 y7 ⟶ x8 y6
Let x8 of type ι → ο be given.
set y9 to be λ x9 . x8
Apply RealsStruct_minus_mult with
y4,
x5,
λ x10 x11 . y9 (field2b y4 x10 y6) (field2b y4 x11 y6) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H5.
set y8 to be λ x8 . y7
Apply L5 with
λ x9 . y8 x9 y7 ⟶ y8 y7 x9 leaving 2 subgoals.
Assume H6: y8 y7 y7.
The subproof is completed by applying H6.
set y9 to be λ x9 . y8
Apply RealsStruct_mult_assoc with
x5,
Field_minus (Field_of_RealsStruct x5) (RealsStruct_one x5),
y6,
y7,
λ x10 x11 . y9 x11 x10 leaving 5 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H4.
The subproof is completed by applying H2.
The subproof is completed by applying L3.
set y10 to be λ x10 . y9
Apply RealsStruct_minus_mult with
y6,
field2b y6 y7 y8,
λ x11 x12 . y10 x12 x11 leaving 3 subgoals.
The subproof is completed by applying H1.
Apply RealsStruct_mult_clos with
y6,
y7,
y8 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying L3.
The subproof is completed by applying L5.
Let x5 of type ι → ι → ο be given.
Apply L4 with
λ x6 . x5 x6 y4 ⟶ x5 y4 x6.
Assume H5: x5 y4 y4.
The subproof is completed by applying H5.