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