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