Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι → ι → ι be given.
Let x4 of type ι → ι → ι be given.
Apply explicit_Ring_with_id_E with
x0,
x1,
x2,
x3,
x4,
∀ x5 . x5 ∈ x0 ⟶ x4 x5 x1 = x1.
Assume H1: ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ x3 x5 x6 ∈ x0.
Assume H2: ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ x3 x5 (x3 x6 x7) = x3 (x3 x5 x6) x7.
Assume H3: ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ x3 x5 x6 = x3 x6 x5.
Assume H4: x1 ∈ x0.
Assume H5: ∀ x5 . x5 ∈ x0 ⟶ x3 x1 x5 = x5.
Assume H6:
∀ x5 . x5 ∈ x0 ⟶ ∃ x6 . and (x6 ∈ x0) (x3 x5 x6 = x1).
Assume H7: ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ x4 x5 x6 ∈ x0.
Assume H8: ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ x4 x5 (x4 x6 x7) = x4 (x4 x5 x6) x7.
Assume H9: x2 ∈ x0.
Assume H10: x2 = x1 ⟶ ∀ x5 : ο . x5.
Assume H11: ∀ x5 . x5 ∈ x0 ⟶ x4 x2 x5 = x5.
Assume H12: ∀ x5 . x5 ∈ x0 ⟶ x4 x5 x2 = x5.
Assume H13: ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ x4 x5 (x3 x6 x7) = x3 (x4 x5 x6) (x4 x5 x7).
Assume H14: ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ x4 (x3 x5 x6) x7 = x3 (x4 x5 x7) (x4 x6 x7).
Let x5 of type ι be given.
Assume H15: x5 ∈ x0.
Apply explicit_Ring_with_id_plus_cancelR with
x0,
x1,
x2,
x3,
x4,
x4 x5 x1,
x1,
x4 x5 x1 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L16.
The subproof is completed by applying H4.
The subproof is completed by applying L16.
Apply H5 with
x4 x5 x1,
λ x6 x7 . x3 (x4 x5 x1) (x4 x5 x1) = x7 leaving 2 subgoals.
The subproof is completed by applying L16.
Apply H13 with
x5,
x1,
x1,
λ x6 x7 . x6 = x4 x5 x1 leaving 4 subgoals.
The subproof is completed by applying H15.
The subproof is completed by applying H4.
The subproof is completed by applying H4.
Apply H5 with
x1,
λ x6 x7 . x4 x5 x7 = x4 x5 x1 leaving 2 subgoals.
The subproof is completed by applying H4.
Let x6 of type ι → ι → ο be given.
Assume H17: x6 (x4 x5 x1) (x4 x5 x1).
The subproof is completed by applying H17.