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.
Let x5 of type ι → ι → ο be given.
Apply explicit_OrderedField_E with
x0,
x1,
x2,
x3,
x4,
x5,
∀ x6 : ο . ({x7 ∈ x0|explicit_OrderedField_rationalp x0 x1 x2 x3 x4 x5 x7} ⊆ x0 ⟶ (∀ x7 . x7 ∈ {x8 ∈ x0|explicit_OrderedField_rationalp x0 x1 x2 x3 x4 x5 x8} ⟶ ∀ x8 : ο . (x7 ∈ x0 ⟶ ∀ x9 . x9 ∈ {x10 ∈ x0|or (or (explicit_Field_minus x0 x1 x2 x3 x4 x10 ∈ {x11 ∈ {x11 ∈ x0|natOfOrderedField_p x0 x1 x2 x3 x4 x5 x11}|x11 = x1 ⟶ ∀ x12 : ο . x12}) (x10 = x1)) (x10 ∈ {x11 ∈ {x11 ∈ x0|natOfOrderedField_p x0 x1 x2 x3 x4 x5 x11}|x11 = x1 ⟶ ∀ x12 : ο . x12})} ⟶ ∀ x10 . x10 ∈ {x11 ∈ {x11 ∈ x0|natOfOrderedField_p x0 x1 x2 x3 x4 x5 x11}|x11 = x1 ⟶ ∀ x12 : ο . x12} ⟶ x4 x10 x7 = x9 ⟶ x8) ⟶ x8) ⟶ (∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ {x9 ∈ x0|or (or (explicit_Field_minus x0 x1 x2 x3 x4 x9 ∈ {x10 ∈ {x10 ∈ x0|natOfOrderedField_p x0 x1 x2 x3 x4 x5 x10}|x10 = x1 ⟶ ∀ x11 : ο . x11}) (x9 = x1)) (x9 ∈ {x10 ∈ {x10 ∈ x0|natOfOrderedField_p x0 x1 x2 x3 x4 x5 x10}|x10 = x1 ⟶ ∀ x11 : ο . x11})} ⟶ ∀ x9 . x9 ∈ {x10 ∈ {x10 ∈ x0|natOfOrderedField_p x0 x1 x2 x3 x4 x5 x10}|x10 = x1 ⟶ ∀ x11 : ο . x11} ⟶ x4 x9 x7 = x8 ⟶ x7 ∈ {x10 ∈ x0|explicit_OrderedField_rationalp x0 x1 x2 x3 x4 x5 x10}) ⟶ x6) ⟶ x6.
Apply explicit_Field_E with
x0,
x1,
x2,
x3,
x4,
... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ∀ x6 : ο . (... ⟶ ... ⟶ (∀ x7 . ... ⟶ ∀ x8 . x8 ∈ {x9 ∈ x0|or (or (explicit_Field_minus x0 x1 x2 x3 x4 x9 ∈ {x10 ∈ {x10 ∈ x0|natOfOrderedField_p ... ... ... ... ... ... ...}|...}) ...) ...} ⟶ ∀ x9 . x9 ∈ {x10 ∈ {x10 ∈ x0|natOfOrderedField_p x0 x1 x2 x3 x4 x5 x10}|x10 = x1 ⟶ ∀ x11 : ο . x11} ⟶ x4 x9 x7 = x8 ⟶ x7 ∈ {x10 ∈ x0|explicit_OrderedField_rationalp x0 x1 x2 x3 x4 x5 x10}) ⟶ x6) ⟶ x6.