Let x0 of type ι be given.

Assume H0: CRing_with_id x0.

Apply explicit_CRing_with_id_E with field0 x0, field3 x0, field4 x0, field1b x0, field2b x0, ∀ x1 . x1 ∈ field0 x0 ⟶ field2b x0 (field4 x0) x1 = x1 leaving 2 subgoals.

Assume H2: ∀ x1 . x1 ∈ field0 x0 ⟶ ∀ x2 . x2 ∈ field0 x0 ⟶ field1b x0 x1 x2 ∈ field0 x0.

Assume H3: ∀ x1 . x1 ∈ field0 x0 ⟶ ∀ x2 . x2 ∈ field0 x0 ⟶ ∀ x3 . x3 ∈ field0 x0 ⟶ field1b x0 x1 (field1b x0 x2 x3) = field1b x0 (field1b x0 x1 x2) x3.

Assume H4: ∀ x1 . x1 ∈ field0 x0 ⟶ ∀ x2 . x2 ∈ field0 x0 ⟶ field1b x0 x1 x2 = field1b x0 x2 x1.

Assume H5: field3 x0 ∈ field0 x0.

Assume H6: ∀ x1 . x1 ∈ field0 x0 ⟶ field1b x0 (field3 x0) x1 = x1.

Assume H7: ∀ x1 . x1 ∈ field0 x0 ⟶ ∃ x2 . and (x2 ∈ field0 x0) (field1b x0 x1 x2 = field3 x0).

Assume H8: ∀ x1 . x1 ∈ field0 x0 ⟶ ∀ x2 . x2 ∈ field0 x0 ⟶ field2b x0 x1 x2 ∈ field0 x0.

Assume H9: ∀ x1 . x1 ∈ field0 x0 ⟶ ∀ x2 . x2 ∈ field0 x0 ⟶ ∀ x3 . x3 ∈ field0 x0 ⟶ field2b x0 x1 (field2b x0 x2 x3) = field2b x0 (field2b x0 x1 x2) x3.

Assume H10: ∀ x1 . x1 ∈ field0 x0 ⟶ ∀ x2 . x2 ∈ field0 x0 ⟶ field2b x0 x1 x2 = field2b x0 x2 x1.

Assume H11: field4 x0 ∈ field0 x0.

Assume H12: field4 x0 = field3 x0 ⟶ ∀ x1 : ο . x1.

Assume H13: ∀ x1 . x1 ∈ field0 x0 ⟶ field2b x0 (field4 x0) x1 = x1.

Assume H14: ∀ x1 . x1 ∈ field0 x0 ⟶ ∀ x2 . x2 ∈ field0 x0 ⟶ ∀ x3 . x3 ∈ field0 x0 ⟶ field2b x0 x1 (field1b x0 x2 x3) = field1b x0 (field2b x0 x1 x2) (field2b x0 x1 x3).

The subproof is completed by applying H13.

...

■

Proofgold Proof