let a, b be non empty Ordinal; :: thesis: ( omega *^ a c= b iff omega -exponent a in omega -exponent b )
A1: ( 0 in a & 0 in b & 1 in omega ) by XBOOLE_1:61, ORDINAL1:11;

hereby :: thesis: ( omega -exponent a in omega -exponent b implies omega *^ a c= b )

assume A2: omega *^ a c= b ; :: thesis: omega -exponent a in omega -exponent b
exp (omega,(omega -exponent a)) c= a by A1, ORDINAL5:def 10;
then omega *^ (exp (omega,(omega -exponent a))) c= omega *^ a by ORDINAL2:42;
then exp (omega,(succ (omega -exponent a))) c= omega *^ a by ORDINAL2:44;
then exp (omega,(succ (omega -exponent a))) c= b by A2, XBOOLE_1:1;
then succ (omega -exponent a) c= omega -exponent b by A1, ORDINAL5:def 10;
hence omega -exponent a in omega -exponent b by ORDINAL1:6, TARSKI:def 3; :: thesis: verum

end;

assume omega -exponent a in omega -exponent b ; :: thesis: omega *^ a c= b
then A3: a in exp (omega,(omega -exponent b)) by Th102;
reconsider fi = id omega as Ordinal-Sequence ;
A4: sup fi = sup (rng fi) by ORDINAL2:def 5
.= omega by ORDINAL2:18 ;
set psi = fi *^ a;
A5: dom fi = dom (fi *^ a) by ORDINAL3:def 4;
for A, B being Ordinal st A in dom fi & B = fi . A holds
(fi *^ a) . A = B *^ a by ORDINAL3:def 4;
then A6: sup (fi *^ a) = omega *^ a by A4, A5, ORDINAL3:42;

now :: thesis: for A being Ordinal st A in rng (fi *^ a) holds
A in exp (omega,(omega -exponent b))

let A be Ordinal; :: thesis: ( A in rng (fi *^ a) implies A in exp (omega,(omega -exponent b)) )
assume A in rng (fi *^ a) ; :: thesis: A in exp (omega,(omega -exponent b))
then consider n being object such that
A7: ( n in dom (fi *^ a) & (fi *^ a) . n = A ) by FUNCT_1:def 3;
reconsider n = n as Nat by A5, A7;
A = (fi . n) *^ a by A5, A7, ORDINAL3:def 4
.= n *^ a by A5, A7, FUNCT_1:18 ;
hence A in exp (omega,(omega -exponent b)) by A3, Th42; :: thesis: verum

end;

then sup (rng (fi *^ a)) c= exp (omega,(omega -exponent b)) by ORDINAL2:20;
then A8: omega *^ a c= exp (omega,(omega -exponent b)) by A6, ORDINAL2:def 5;
( 0 in b & 1 in omega ) by XBOOLE_1:61, ORDINAL1:11;
then exp (omega,(omega -exponent b)) c= b by ORDINAL5:def 10;
hence omega *^ a c= b by A8, XBOOLE_1:1; :: thesis: verum