let a be ordinal number ; :: thesis: ( 0 in a implies ex n being natural number ex c being ordinal number st
( a = (n *^ (exp (omega,(omega -exponent a)))) +^ c & 0 in n & c in exp (omega,(omega -exponent a)) ) )
assume A0: 0 in a ; :: thesis: ex n being natural number ex c being ordinal number st
( a = (n *^ (exp (omega,(omega -exponent a)))) +^ c & 0 in n & c in exp (omega,(omega -exponent a)) )
set c = omega -exponent a;
set n = a div^ (exp (omega,(omega -exponent a)));
set b = a mod^ (exp (omega,(omega -exponent a)));
a div^ (exp (omega,(omega -exponent a))) in omega by A0, Th43a;
then reconsider n = a div^ (exp (omega,(omega -exponent a))) as Nat ;
take n ; :: thesis: ex c being ordinal number st
( a = (n *^ (exp (omega,(omega -exponent a)))) +^ c & 0 in n & c in exp (omega,(omega -exponent a)) )
take a mod^ (exp (omega,(omega -exponent a))) ; :: thesis: ( a = (n *^ (exp (omega,(omega -exponent a)))) +^ (a mod^ (exp (omega,(omega -exponent a)))) & 0 in n & a mod^ (exp (omega,(omega -exponent a))) in exp (omega,(omega -exponent a)) )
thus a = (n *^ (exp (omega,(omega -exponent a)))) +^ (a mod^ (exp (omega,(omega -exponent a)))) by ORDINAL3:78; :: thesis: ( 0 in n & a mod^ (exp (omega,(omega -exponent a))) in exp (omega,(omega -exponent a)) )
thus 0 in n by A0, Th43b; :: thesis: a mod^ (exp (omega,(omega -exponent a))) in exp (omega,(omega -exponent a))
thus a mod^ (exp (omega,(omega -exponent a))) in exp (omega,(omega -exponent a)) by Th43c; :: thesis: verum