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 A1: ( 0 in n & n in b ) ; :: thesis: b -exponent (n *^ (exp (b,a))) = a
then A2: succ 0 c= n by ORDINAL1:21;
then A3: ( 1 *^ (exp (b,a)) = exp (b,a) & 1 *^ (exp (b,a)) c= n *^ (exp (b,a)) ) by ORDINAL2:39, ORDINAL2:41;
A4: ( exp (b,a) <> 0 & n <> 0 ) by A1, ORDINAL4:22;
then 0 <> n *^ (exp (b,a)) by ORDINAL3:31;
then A5: ( 1 in b & 0 in n *^ (exp (b,a)) ) by A2, A1, ORDINAL1:12, ORDINAL3:8;

now

let c be ordinal number ; :: thesis: ( exp (b,c) c= n *^ (exp (b,a)) implies not c c/= a )
assume A6: ( exp (b,c) c= n *^ (exp (b,a)) & c c/= a ) ; :: thesis: contradiction
then a in c by ORDINAL1:16;
then succ a c= c by ORDINAL1:21;
then A7: exp (b,(succ a)) c= exp (b,c) by A1, ORDINAL4:27;
exp (b,(succ a)) = b *^ (exp (b,a)) by ORDINAL2:44;
then b *^ (exp (b,a)) c= n *^ (exp (b,a)) by A6, A7, XBOOLE_1:1;
then b c= n by A4, ORDINAL3:35;
then n in n by A1;
hence contradiction ; :: thesis: verum

end;

hence b -exponent (n *^ (exp (b,a))) = a by A3, A5, Def10; :: thesis: verum