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