Let x0 of type ι be given.

Assume H0: CRing_with_id x0.

Apply explicit_CRing_with_id_E with K_field_0 x0 x0, K_field_3 x0 x0, K_field_4 x0 x0, K_field_1_b x0 x0, K_field_2_b x0 x0, ∀ x1 . x1 ∈ K_field_0 x0 x0 ⟶ K_field_2_b x0 x0 (K_field_4 x0 x0) x1 = x1 leaving 2 subgoals.

Assume H2: ∀ x1 . x1 ∈ K_field_0 x0 x0 ⟶ ∀ x2 . x2 ∈ K_field_0 x0 x0 ⟶ K_field_1_b x0 x0 x1 x2 ∈ K_field_0 x0 x0.

Assume H3: ∀ x1 . x1 ∈ K_field_0 x0 x0 ⟶ ∀ x2 . x2 ∈ K_field_0 x0 x0 ⟶ ∀ x3 . x3 ∈ K_field_0 x0 x0 ⟶ K_field_1_b x0 x0 x1 (K_field_1_b x0 x0 x2 x3) = K_field_1_b x0 x0 (K_field_1_b x0 x0 x1 x2) x3.

Assume H4: ∀ x1 . x1 ∈ K_field_0 x0 x0 ⟶ ∀ x2 . x2 ∈ K_field_0 x0 x0 ⟶ K_field_1_b x0 x0 x1 x2 = K_field_1_b x0 x0 x2 x1.

Assume H5: K_field_3 x0 x0 ∈ K_field_0 x0 x0.

Assume H6: ∀ x1 . x1 ∈ K_field_0 x0 x0 ⟶ K_field_1_b x0 x0 (K_field_3 x0 x0) x1 = x1.

Assume H7: ∀ x1 . x1 ∈ K_field_0 x0 x0 ⟶ ∃ x2 . and (x2 ∈ K_field_0 x0 x0) (K_field_1_b x0 x0 x1 x2 = K_field_3 x0 x0).

Assume H8: ∀ x1 . x1 ∈ K_field_0 x0 x0 ⟶ ∀ x2 . x2 ∈ K_field_0 x0 x0 ⟶ K_field_2_b x0 x0 x1 x2 ∈ K_field_0 x0 x0.

Assume H9: ∀ x1 . x1 ∈ K_field_0 x0 x0 ⟶ ∀ x2 . x2 ∈ K_field_0 x0 x0 ⟶ ∀ x3 . x3 ∈ K_field_0 x0 x0 ⟶ K_field_2_b x0 x0 x1 (K_field_2_b x0 x0 x2 x3) = K_field_2_b x0 x0 (K_field_2_b x0 x0 x1 x2) x3.

Assume H10: ∀ x1 . x1 ∈ K_field_0 x0 x0 ⟶ ∀ x2 . x2 ∈ K_field_0 x0 x0 ⟶ K_field_2_b x0 x0 x1 x2 = K_field_2_b x0 x0 x2 x1.

Assume H11: K_field_4 x0 x0 ∈ K_field_0 x0 x0.

...

■

Proofgold Proof