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