Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Claim L3: ∀ x5 : ι → ο . x5 y4 ⟶ x5 y3
Let x5 of type ι → ο be given.
Apply RealsStruct_mult_com with
x2,
y3,
Field_minus (Field_of_RealsStruct x2) y4,
λ x6 . x5 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply RealsStruct_minus_clos with
x2,
y4 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Apply RealsStruct_minus_mult_L with
x2,
y4,
y3,
λ x6 . x5 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H1.
Claim L4: ∀ x8 : ι → ο . x8 y7 ⟶ x8 y6
Let x8 of type ι → ο be given.
set y9 to be λ x9 . x8
Apply RealsStruct_mult_com with
y4,
y6,
x5,
λ x10 x11 . y9 (Field_minus (Field_of_RealsStruct y4) x10) (Field_minus (Field_of_RealsStruct y4) x11) leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H1.
The subproof is completed by applying H4.
set y8 to be λ x8 . y7
Apply L4 with
λ x9 . y8 x9 y7 ⟶ y8 y7 x9 leaving 2 subgoals.
Assume H5: y8 y7 y7.
The subproof is completed by applying H5.
The subproof is completed by applying L4.
Let x5 of type ι → ι → ο be given.
Apply L3 with
λ x6 . x5 x6 y4 ⟶ x5 y4 x6.
Assume H4: x5 y4 y4.
The subproof is completed by applying H4.