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_Field_E with x0, x1, x2, x3, x4, ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ x4 (explicit_Field_minus x0 x1 x2 x3 x4 x5) x6 = explicit_Field_minus x0 x1 x2 x3 x4 (x4 x5 x6).

Assume H0: explicit_Field x0 x1 x2 x3 x4.

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: ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ x4 x5 x6 = x4 x6 x5.

Assume H10: x2 ∈ x0.

Assume H11: x2 = x1 ⟶ ∀ x5 : ο . x5.

Assume H12: ∀ x5 . x5 ∈ x0 ⟶ x4 x2 x5 = x5.

Assume H13: ∀ x5 . x5 ∈ x0 ⟶ (x5 = x1 ⟶ ∀ x6 : ο . x6) ⟶ ∃ x6 . and (x6 ∈ x0) (x4 x5 x6 = x2).

Assume H14: ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ x4 x5 (x3 x6 x7) = x3 (x4 x5 x6) (x4 x5 x7).

Let x5 of type ι be given.

Assume H15: x5 ∈ x0.

Let x6 of type ι be given.

Assume H16: x6 ∈ x0.

Claim L17: ...

...

set y7 to be ...

set y8 to be ...

Claim L18: ∀ x9 : ι → ο . x9 y8 ⟶ x9 y7

Let x9 of type ι → ο be given.

Assume H18: x9 (explicit_Field_minus x2 x3 x4 x5 x6 (x6 y7 y8)).

...

Let x9 of type ι → ι → ο be given.

Apply L18 with λ x10 . x9 x10 y8 ⟶ x9 y8 x10.

Assume H19: x9 y8 y8.

The subproof is completed by applying H19.

■

Proofgold Proof