let a be Ordinal; :: thesis: ( 0 in a implies ex n being Nat ex c being Ordinal st
( a = (n *^ (exp (omega,(omega -exponent a)))) +^ c & 0 in Segm n & c in exp (omega,(omega -exponent a)) ) )
assume A1: 0 in a ; :: thesis: ex n being Nat ex c being Ordinal st
( a = (n *^ (exp (omega,(omega -exponent a)))) +^ c & 0 in Segm 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 A1, Th59;
then reconsider n = a div^ (exp (omega,(omega -exponent a))) as Nat ;
take n ; :: thesis: ex c being Ordinal st
( a = (n *^ (exp (omega,(omega -exponent a)))) +^ c & 0 in Segm 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 Segm 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:65; :: thesis: ( 0 in Segm n & a mod^ (exp (omega,(omega -exponent a))) in exp (omega,(omega -exponent a)) )
thus 0 in Segm n by A1, Th60; :: 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 Th61; :: thesis: verum