let a, b be Ordinal; :: thesis: ( a +^ b = b iff omega *^ a c= b )

hereby :: thesis: ( omega *^ a c= b implies a +^ b = b )

assume A1: a +^ b = b ; :: thesis: omega *^ a c= b
defpred S₁[ Nat] means ($1 *^ a) +^ b = b;
0 *^ a = 0 by ORDINAL2:35;
then A2: S₁[ 0 ] by ORDINAL2:30;
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
thus ((n + 1) *^ a) +^ b = ((succ n) *^ a) +^ b by Lm5
.= ((n *^ a) +^ a) +^ b by ORDINAL2:36
.= b by A1, A4, ORDINAL3:30 ; :: thesis: verum

end;

A5: for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3);

per cases ( a = {} or a <> {} ) ;

suppose a = {} ; :: thesis: omega *^ a c= b

then omega *^ a = {} by ORDINAL2:38;
hence omega *^ a c= b ; :: thesis: verum

end;

suppose A6: a <> {} ; :: thesis: omega *^ a c= b

reconsider fi = id omega as Ordinal-Sequence ;
A7: sup fi = sup (rng fi) by ORDINAL2:def 5
.= omega by ORDINAL2:18 ;
set psi = fi *^ a;
A8: 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 A9: sup (fi *^ a) = omega *^ a by A6, A7, A8, ORDINAL3:42;

now :: thesis: for A being Ordinal st A in rng (fi *^ a) holds
A in b

let A be Ordinal; :: thesis: ( A in rng (fi *^ a) implies A in b )
assume A in rng (fi *^ a) ; :: thesis: A in b
then consider n being object such that
A10: ( n in dom (fi *^ a) & (fi *^ a) . n = A ) by FUNCT_1:def 3;
reconsider n = n as Nat by A8, A10;
A = (fi . n) *^ a by A8, A10, ORDINAL3:def 4
.= n *^ a by A8, A10, FUNCT_1:18 ;
then A11: A +^ b = b by A5;
then A12: A c= b by ORDINAL3:24;
A <> b

proof

assume A = b ; :: thesis: contradiction
then 2 *^ b = A +^ b by Th2
.= 1 *^ b by A11, ORDINAL2:39 ;
hence contradiction by A1, A6, ORDINAL3:33; :: thesis: verum

end;

hence A in b by A12, XBOOLE_0:def 8, ORDINAL1:11; :: thesis: verum

end;

then sup (rng (fi *^ a)) c= b by ORDINAL2:20;
hence omega *^ a c= b by A9, ORDINAL2:def 5; :: thesis: verum

end;

end;

end;

assume omega *^ a c= b ; :: thesis: a +^ b = b
then consider c being Ordinal such that
A13: b = (omega *^ a) +^ c by ORDINAL3:27;
thus a +^ b = (1 *^ a) +^ ((omega *^ a) +^ c) by A13, ORDINAL2:39
.= ((1 *^ a) +^ (omega *^ a)) +^ c by ORDINAL3:30
.= ((1 +^ omega) *^ a) +^ c by ORDINAL3:46
.= b by A13, CARD_2:74 ; :: thesis: verum