Proofgold Proposition

∀ x0 x1 x2 . x2 ∈ omega ⟶ ∀ x3 . ap x3 0 = x0 ⟶ ap x3 x2 = x1 ⟶ (∀ x4 . x4 ∈ ordsucc x2 ⟶ Field (ap x3 x4)) ⟶ (∀ x4 . x4 ∈ x2 ⟶ ∀ x5 : ο . (∀ x6 . and (x6 ∈ field0 (ap x3 (ordsucc x4))) (∀ x7 : ο . (∀ x8 . and (x8 ∈ omega) (and (CRing_with_id_omega_exp (ap x3 (ordsucc x4)) x6 x8 ∈ field0 (ap x3 x4)) (Field_extension_by_1 (ap x3 x4) (ap x3 (ordsucc x4)) x6)) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ radical_field_extension x0 x1

type
prop

theory
HotG

name
radical_field_extension_I

proof
PUXQg..

Megalodon
radical_field_extension_I

proofgold address
TMb2e..^{radical_field_extension_I}

creator
5919 Pr6Pc../9a990..

owner
5919 Pr6Pc../9a990..

term root
4e422..