let a, b be Ordinal; :: thesis: for n being Nat st 0 in n & n in b holds
b -exponent (n *^ (exp (b,a))) = a
let n be Nat; :: 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;
( exp (b,a) <> 0 & n <> 0 ) by A1, ORDINAL4:22;
then 0 <> n *^ (exp (b,a)) by ORDINAL3:31;
then A4: ( 1 in b & 0 in n *^ (exp (b,a)) ) by A2, A1, ORDINAL1:12, ORDINAL3:8;

now :: thesis: for c being Ordinal st exp (b,c) c= n *^ (exp (b,a)) holds
not c c/= a

let c be Ordinal; :: thesis: ( exp (b,c) c= n *^ (exp (b,a)) implies not c c/= a )
assume A5: ( 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 A6: 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 A5, A6;
then b c= n by ORDINAL3:35, ORDINAL4:22;
then n in n by A1;
hence contradiction ; :: thesis: verum

end;

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