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 . and (x5 ∈ field0 (ap x3 (ordsucc x4))) (∃ x7 . and (x7 ∈ omega) (and (CRing_with_id_omega_exp (ap x3 (ordsucc x4)) x5 x7 ∈ field0 (ap x3 x4)) (Field_extension_by_1 (ap x3 x4) (ap x3 (ordsucc x4)) 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..