Let x0 of type ι be given.
Let x1 of type ι → ι → ι be given.
Apply H0 with
∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x1 x2 x3 = x1 x2 x4 ⟶ x3 = x4.
Assume H1:
and (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ∈ x0) (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4).
Apply H1 with
(∃ x2 . and (x2 ∈ x0) (and (∀ x3 . x3 ∈ x0 ⟶ and (x1 x2 x3 = x3) (x1 x3 x2 = x3)) (∀ x3 . x3 ∈ x0 ⟶ ∃ x4 . and (x4 ∈ x0) (and (x1 x3 x4 = x2) (x1 x4 x3 = x2))))) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x1 x2 x3 = x1 x2 x4 ⟶ x3 = x4.
Assume H2: ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ∈ x0.
Assume H3: ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4.
Assume H4:
∃ x2 . and (x2 ∈ x0) (and (∀ x3 . x3 ∈ x0 ⟶ and (x1 x2 x3 = x3) (x1 x3 x2 = x3)) (∀ x3 . x3 ∈ x0 ⟶ ∃ x4 . and (x4 ∈ x0) (and (x1 x3 x4 = x2) (x1 x4 x3 = x2)))).
Let x2 of type ι be given.
Assume H5: x2 ∈ x0.
Let x3 of type ι be given.
Assume H6: x3 ∈ x0.
Let x4 of type ι be given.
Assume H7: x4 ∈ x0.
Assume H8: x1 x2 x3 = x1 x2 x4.
Let x5 of type ι be given.
Assume H9: x5 ∈ x0.
Apply H3 with
explicit_Group_inverse x0 x1 x2,
x2,
x5,
λ x6 x7 . x7 = x5 leaving 4 subgoals.
Apply explicit_Group_inverse_in with
x0,
x1,
x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H5.
The subproof is completed by applying H5.
The subproof is completed by applying H9.
Apply explicit_Group_inverse_linv with
x0,
x1,
x2,
λ x6 x7 . x1 ... ... = ... leaving 3 subgoals.
Apply L9 with
x3,
λ x5 x6 . x5 = x4 leaving 2 subgoals.
The subproof is completed by applying H6.
Apply H8 with
λ x5 x6 . x1 (explicit_Group_inverse x0 x1 x2) x6 = x4.
Apply L9 with
x4.
The subproof is completed by applying H7.