let a, c be ordinal number ; :: thesis: ( 0 in a & c = omega -exponent a implies a div^ (exp omega ,c) in omega )
assume A0: ( 0 in a & c = omega -exponent a ) ; :: thesis: a div^ (exp omega ,c) in omega
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 a div^ (exp omega ,c) in omega ; :: thesis: contradiction
then omega *^ (exp omega ,c) c= (a div^ (exp omega ,c)) *^ (exp omega ,c) by ORDINAL2:58, ORDINAL1:26;
then ( exp omega ,(succ c) c= (a div^ (exp omega ,c)) *^ (exp omega ,c) & (a div^ (exp omega ,c)) *^ (exp omega ,c) c= a ) by A2, ORDINAL2:61, ORDINAL3:27;
then exp omega ,(succ c) c= a by XBOOLE_1:1;
then ( succ c c= c & c in succ c ) by A0, EXP, ORDINAL1:10;
then c in c ;
hence contradiction ; :: thesis: verum