| ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 x4 x5 . ∀ x6 x7 : ι → ι → ι . explicit_Field x0 x3 x4 x6 x7 ⟶ (∀ x8 : ο . (∀ x9 : ι → ι → ο . explicit_Reals {x10 ∈ x0|x1 x10 = x10} x3 x4 x6 x7 x9 ⟶ x8) ⟶ x8) ⟶ (∀ x8 . x8 ∈ x0 ⟶ x2 x8 ∈ {x9 ∈ x0|x1 x9 = x9}) ⟶ x5 ∈ x0 ⟶ (∀ x8 . x8 ∈ x0 ⟶ x1 x8 ∈ x0) ⟶ (∀ x8 . x8 ∈ x0 ⟶ x2 x8 ∈ x0) ⟶ (∀ x8 . x8 ∈ x0 ⟶ x8 = x6 (x1 x8) (x7 x5 (x2 x8))) ⟶ (∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ x1 x8 = x1 x9 ⟶ x2 x8 = x2 x9 ⟶ x8 = x9) ⟶ x6 (x7 x5 x5) x4 = x3 ⟶ explicit_Complex x0 x1 x2 x3 x4 x5 x6 x7 |
|