let a be Ordinal; ( 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
; 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
; 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)))
; ( 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; ( 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; 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; verum