Let x0 of type ι be given.

Let x1 of type ι → ι → ι be given.

Let x2 of type ι be given.

Assume H1: x2 ∈ x0.

Apply explicit_Group_identity_prop with x0, x1, x1 x2 (explicit_Group_identity x0 x1) = x2 leaving 2 subgoals.

The subproof is completed by applying H0.

Assume H2: explicit_Group_identity x0 x1 ∈ x0.

Assume H3: and (∀ x3 . x3 ∈ x0 ⟶ and (x1 (explicit_Group_identity x0 x1) x3 = x3) (x1 x3 (explicit_Group_identity x0 x1) = x3)) (∀ x3 . x3 ∈ x0 ⟶ ∃ x4 . and (x4 ∈ x0) (and (x1 x3 x4 = explicit_Group_identity x0 x1) (x1 x4 x3 = explicit_Group_identity x0 x1))).

Apply H3 with x1 x2 (explicit_Group_identity x0 x1) = x2.

Assume H4: ∀ x3 . x3 ∈ x0 ⟶ and (x1 (explicit_Group_identity x0 x1) x3 = x3) (x1 x3 (explicit_Group_identity x0 x1) = x3).

Assume H5: ∀ x3 . x3 ∈ x0 ⟶ ∃ x4 . and (x4 ∈ x0) (and (x1 x3 x4 = explicit_Group_identity x0 x1) (x1 x4 x3 = explicit_Group_identity x0 x1)).

Apply H4 with x2, x1 x2 (explicit_Group_identity x0 x1) = x2 leaving 2 subgoals.

The subproof is completed by applying H1.

Assume H6: x1 (explicit_Group_identity x0 x1) x2 = x2.

Assume H7: x1 x2 (explicit_Group_identity x0 x1) = x2.

The subproof is completed by applying H7.

■

Proofgold Proof