let a, c be ordinal number ; :: thesis: ( 0 in a & c = omega -exponent a implies a mod^ (exp omega ,c) in exp omega ,c )
assume ( 0 in a & c = omega -exponent a ) ; :: thesis: a mod^ (exp omega ,c) in 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;
d = a -^ ((a div^ (exp omega ,c)) *^ (exp omega ,c)) by A2, ORDINAL3:65
.= a mod^ (exp omega ,c) by ORDINAL3:def 8 ;
hence a mod^ (exp omega ,c) in exp omega ,c by A2; :: thesis: verum