| ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 x6 x7 . ∀ x8 x9 : ι → ι → ι . ∀ x10 : ι → ι . explicit_Field x0 x1 x2 x3 x4 ⟶ bij x0 x5 x10 ⟶ x10 x1 = x6 ⟶ x10 x2 = x7 ⟶ (∀ x11 . prim1 x11 x0 ⟶ ∀ x12 . prim1 x12 x0 ⟶ x10 (x3 x11 x12) = x8 (x10 x11) (x10 x12)) ⟶ (∀ x11 . prim1 x11 x0 ⟶ ∀ x12 . prim1 x12 x0 ⟶ x10 (x4 x11 x12) = x9 (x10 x11) (x10 x12)) ⟶ explicit_Field x5 x6 x7 x8 x9 |
|