let a, b, c be Ordinal; :: thesis: ( 0 in a & 1 in b & c = b -exponent a implies a div^ (exp (b,c)) in b )
assume A1: ( 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 A1;
then consider d being Ordinal such that
A2: ( a = ((a div^ (exp (b,c))) *^ (exp (b,c))) +^ d & d in exp (b,c) ) by ORDINAL3:def 6;
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 ORDINAL1:16, ORDINAL2:41;
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:44, ORDINAL3:24;
then exp (b,(succ c)) c= a ;
then ( succ c c= c & c in succ c ) by A1, Def10, ORDINAL1:6;
then c in c ;
hence contradiction ; :: thesis: verum