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

now

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

end;

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