let a, b, c be Ordinal; :: thesis: ( 0 in c & c in b implies b -exponent (c *^ (exp (b,a))) = a )
assume A1: ( 0 in c & c in b ) ; :: thesis: b -exponent (c *^ (exp (b,a))) = a
then A2: succ 0 c= c by ORDINAL1:21;
then A3: ( 1 *^ (exp (b,a)) = exp (b,a) & 1 *^ (exp (b,a)) c= c *^ (exp (b,a)) ) by ORDINAL2:39, ORDINAL2:41;
A4: ( 1 in b & 0 in c *^ (exp (b,a)) ) by A2, A1, ORDINAL1:12, ORDINAL3:8;
now :: thesis: for d being Ordinal st exp (b,d) c= c *^ (exp (b,a)) holds
not d c/= a
let d be Ordinal; :: thesis: ( exp (b,d) c= c *^ (exp (b,a)) implies not d c/= a )
assume A5: ( exp (b,d) c= c *^ (exp (b,a)) & d c/= a ) ; :: thesis: contradiction
then succ a c= d by ORDINAL1:16, ORDINAL1:21;
then A6: exp (b,(succ a)) c= exp (b,d) by A1, ORDINAL4:27;
exp (b,(succ a)) = b *^ (exp (b,a)) by ORDINAL2:44;
then b *^ (exp (b,a)) c= c *^ (exp (b,a)) by A5, A6;
then b c= c by ORDINAL3:35;
then c in c by A1;
hence contradiction ; :: thesis: verum
end;
hence b -exponent (c *^ (exp (b,a))) = a by A3, A4, Def10; :: thesis: verum