let a be ordinal number ; :: thesis:
assume A0: 0 in a ; :: thesis:
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:
take a mod^ (exp omega ,(omega -exponent a)) ; :: thesis:
thus a = (n *^ (exp omega ,(omega -exponent a))) +^ (a mod^ (exp omega ,(omega -exponent a))) by ORDINAL3:78; :: thesis:
thus 0 in n by A0, Th43b; :: thesis:
thus a mod^ (exp omega ,(omega -exponent a)) in exp omega ,(omega -exponent a) by Th43c; :: thesis: