let a, b, c be Ordinal; :: thesis: ( 0 in a & 1 in b & c = b -exponent a implies 0 in a div^ (exp (b,c)) )
assume A1: ( 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 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 0 in a div^ (exp (b,c)) ; :: thesis: contradiction
then a div^ (exp (b,c)) = 0 by ORDINAL3:8;
then a = 0 +^ d by A2, ORDINAL2:35
.= d by ORDINAL2:30 ;
then exp (b,c) c= d by A1, Def10;
then d in d by A2;
hence contradiction ; :: thesis: verum