let a, c be ordinal number ; :: thesis: ( 0 in a & c = omega -exponent a implies 0 in a div^ (exp omega ,c) )
assume A0: ( 0 in a & c = omega -exponent a ) ; :: thesis: 0 in a div^ (exp omega ,c)
set n = a div^ (exp omega ,c);
set b = a mod^ (exp omega ,c);
exp omega ,c <> 0 by ORDINAL4:22;
then consider d being ordinal number such that
A2: ( a = ((a div^ (exp omega ,c)) *^ (exp omega ,c)) +^ d & d in exp omega ,c ) by ORDINAL3:def 7;
assume not 0 in a div^ (exp omega ,c) ; :: thesis: contradiction
then a div^ (exp omega ,c) = 0 by ORDINAL3:10;
then a = 0 +^ d by A2, ORDINAL2:52
.= d by ORDINAL2:47 ;
then exp omega ,c c= d by A0, EXP;
then d in d by A2;
hence contradiction ; :: thesis: verum