Proofgold Proposition

∀ x0 . Field x0 ⟶ ∀ x1 x2 . x2 ∈ omega ⟶ CRing_with_id_omega_exp x0 x1 (ordsucc x2) = field2b x0 x1 (CRing_with_id_omega_exp x0 x1 x2)

type
prop

theory
HotG

name
Field_omega_exp_S

proof
PUMpo..

Megalodon
Field_omega_exp_S

proofgold address
TMXUt..^{Field_omega_exp_S}

creator
5881 Pr6Pc../8f394..

owner
5881 Pr6Pc../8f394..

term root
d2e51..