let b, a be ordinal number ; :: thesis: for n being natural number st 0 in n & n in b holds
b -exponent (n *^ (exp (b,a))) = a
let n be natural number ; :: thesis: ( 0 in n & n in b implies b -exponent (n *^ (exp (b,a))) = a )
assume Z0: ( 0 in n & n in b ) ; :: thesis: b -exponent (n *^ (exp (b,a))) = a
then A0: succ 0 c= n by ORDINAL1:33;
then Z1: ( 1 *^ (exp (b,a)) = exp (b,a) & 1 *^ (exp (b,a)) c= n *^ (exp (b,a)) ) by ORDINAL2:56, ORDINAL2:58;
Z5: ( exp (b,a) <> 0 & n <> 0 ) by Z0, ORDINAL4:22;
then 0 <> n *^ (exp (b,a)) by ORDINAL3:34;
then Z2: ( 1 in b & 0 in n *^ (exp (b,a)) ) by A0, Z0, ORDINAL1:22, ORDINAL3:10;

now

let c be ordinal number ; :: thesis: ( exp (b,c) c= n *^ (exp (b,a)) implies not c c/= a )
assume Z3: ( exp (b,c) c= n *^ (exp (b,a)) & c c/= a ) ; :: thesis: contradiction
then a in c by ORDINAL1:26;
then succ a c= c by ORDINAL1:33;
then Z4: exp (b,(succ a)) c= exp (b,c) by Z0, ORDINAL4:27;
exp (b,(succ a)) = b *^ (exp (b,a)) by ORDINAL2:61;
then b *^ (exp (b,a)) c= n *^ (exp (b,a)) by Z3, Z4, XBOOLE_1:1;
then b c= n by Z5, ORDINAL3:38;
then n in n by Z0;
hence contradiction ; :: thesis: verum

end;

hence b -exponent (n *^ (exp (b,a))) = a by Z1, Z2, EXP; :: thesis: verum