let fi be Ordinal-Sequence; :: thesis: for A, B being Ordinal st A is_limes_of fi holds
A *^ B is_limes_of fi *^ B
let A, B be Ordinal; :: thesis: ( A is_limes_of fi implies A *^ B is_limes_of fi *^ B )
assume A1: A is_limes_of fi ; :: thesis: A *^ B is_limes_of fi *^ B
then A2: ( dom fi = dom (fi *^ B) & dom fi <> {} ) by Lm4, ORDINAL3:def 5;

per cases ( A *^ B = {} or A *^ B <> {} ) ;
:: according to ORDINAL2:def 13

case A *^ B = {} ; :: thesis: ex b₁ being set st
( b₁ in dom (fi *^ B) & ( for b₂ being set holds
( not b₁ c= b₂ or not b₂ in dom (fi *^ B) or (fi *^ B) . b₂ = {} ) ) )

then A3: ( B = {} or A = {} ) by ORDINAL3:34;

now

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

suppose A4: B = {} ; :: thesis: ex A1 being Ordinal st
( A1 in dom (fi *^ B) & ( for C being Ordinal st A1 c= C & C in dom (fi *^ B) holds
(fi *^ B) . C = {} ) )

consider x being Element of dom fi;
reconsider x = x as Ordinal ;
take A1 = x; :: thesis: ( A1 in dom (fi *^ B) & ( for C being Ordinal st A1 c= C & C in dom (fi *^ B) holds
(fi *^ B) . C = {} ) )
thus A1 in dom (fi *^ B) by A2; :: thesis: for C being Ordinal st A1 c= C & C in dom (fi *^ B) holds
(fi *^ B) . C = {}
let C be Ordinal; :: thesis: ( A1 c= C & C in dom (fi *^ B) implies (fi *^ B) . C = {} )
assume ( A1 c= C & C in dom (fi *^ B) ) ; :: thesis: (fi *^ B) . C = {}
hence (fi *^ B) . C = (fi . C) *^ B by A2, ORDINAL3:def 5
.= {} by A4, ORDINAL2:55 ;
:: thesis: verum

end;

suppose B <> {} ; :: thesis: ex A1 being Ordinal st
( A1 in dom (fi *^ B) & ( for C being Ordinal st A1 c= C & C in dom (fi *^ B) holds
(fi *^ B) . C = {} ) )

then consider A1 being Ordinal such that
A5: ( A1 in dom fi & ( for C being Ordinal st A1 c= C & C in dom fi holds
fi . C = {} ) ) by A1, A3, ORDINAL2:def 13;
take A1 = A1; :: thesis: ( A1 in dom (fi *^ B) & ( for C being Ordinal st A1 c= C & C in dom (fi *^ B) holds
(fi *^ B) . C = {} ) )
thus A1 in dom (fi *^ B) by A5, ORDINAL3:def 5; :: thesis: for C being Ordinal st A1 c= C & C in dom (fi *^ B) holds
(fi *^ B) . C = {}
let C be Ordinal; :: thesis: ( A1 c= C & C in dom (fi *^ B) implies (fi *^ B) . C = {} )
assume ( A1 c= C & C in dom (fi *^ B) ) ; :: thesis: (fi *^ B) . C = {}
then ( (fi *^ B) . C = (fi . C) *^ B & fi . C = {} & {} = {} ) by A2, A5, ORDINAL3:def 5;
hence (fi *^ B) . C = {} by ORDINAL2:52; :: thesis: verum

end;

end;

end;

hence ex b₁ being set st
( b₁ in dom (fi *^ B) & ( for b₂ being set holds
( not b₁ c= b₂ or not b₂ in dom (fi *^ B) or (fi *^ B) . b₂ = {} ) ) ) ; :: thesis: verum

end;

case A *^ B <> {} ; :: thesis: for b₁, b₂ being set holds
( not b₁ in A *^ B or not A *^ B in b₂ or ex b₃ being set st
( b₃ in dom (fi *^ B) & ( for b₄ being set holds
( not b₃ c= b₄ or not b₄ in dom (fi *^ B) or ( b₁ in (fi *^ B) . b₄ & (fi *^ B) . b₄ in b₂ ) ) ) ) )

then A6: ( A <> {} & B <> {} ) by ORDINAL2:52, ORDINAL2:55;
let B1, B2 be Ordinal; :: thesis: ( not B1 in A *^ B or not A *^ B in B2 or ex b₁ being set st
( b₁ in dom (fi *^ B) & ( for b₂ being set holds
( not b₁ c= b₂ or not b₂ in dom (fi *^ B) or ( B1 in (fi *^ B) . b₂ & (fi *^ B) . b₂ in B2 ) ) ) ) )
assume A7: ( B1 in A *^ B & A *^ B in B2 ) ; :: thesis: ex b₁ being set st
( b₁ in dom (fi *^ B) & ( for b₂ being set holds
( not b₁ c= b₂ or not b₂ in dom (fi *^ B) or ( B1 in (fi *^ B) . b₂ & (fi *^ B) . b₂ in B2 ) ) ) )

A8: now

given A1 being Ordinal such that A9: A = succ A1 ; :: thesis: ex D being Ordinal st
( D in dom (fi *^ B) & ( for C being Ordinal st D c= C & C in dom (fi *^ B) holds
( B1 in (fi *^ B) . C & (fi *^ B) . C in B2 ) ) )
( A1 in A & A in succ A ) by A9, ORDINAL1:10;
then consider D being Ordinal such that
A10: ( D in dom fi & ( for C being Ordinal st D c= C & C in dom fi holds
( A1 in fi . C & fi . C in succ A ) ) ) by A1, ORDINAL2:def 13;
take D = D; :: thesis: ( D in dom (fi *^ B) & ( for C being Ordinal st D c= C & C in dom (fi *^ B) holds
( B1 in (fi *^ B) . C & (fi *^ B) . C in B2 ) ) )
thus D in dom (fi *^ B) by A10, ORDINAL3:def 5; :: thesis: for C being Ordinal st D c= C & C in dom (fi *^ B) holds
( B1 in (fi *^ B) . C & (fi *^ B) . C in B2 )
let C be Ordinal; :: thesis: ( D c= C & C in dom (fi *^ B) implies ( B1 in (fi *^ B) . C & (fi *^ B) . C in B2 ) )
assume A11: ( D c= C & C in dom (fi *^ B) ) ; :: thesis: ( B1 in (fi *^ B) . C & (fi *^ B) . C in B2 )
reconsider E = fi . C as Ordinal ;
A12: ( A1 in E & E in succ A & (fi *^ B) . C = E *^ B ) by A2, A10, A11, ORDINAL3:def 5;
then ( A c= E & E c= A ) by A9, ORDINAL1:33, ORDINAL1:34;
hence ( B1 in (fi *^ B) . C & (fi *^ B) . C in B2 ) by A7, A12, XBOOLE_0:def 10; :: thesis: verum

end;

now

assume for A1 being Ordinal holds not A = succ A1 ; :: thesis: ex D being Ordinal st
( D in dom (fi *^ B) & ( for A1 being Ordinal st D c= A1 & A1 in dom (fi *^ B) holds
( B1 in (fi *^ B) . A1 & (fi *^ B) . A1 in B2 ) ) )
then A is limit_ordinal by ORDINAL1:42;
then consider C being Ordinal such that
A13: ( C in A & B1 in C *^ B ) by A7, ORDINAL3:49;
A in succ A by ORDINAL1:10;
then consider D being Ordinal such that
A14: ( D in dom fi & ( for A1 being Ordinal st D c= A1 & A1 in dom fi holds
( C in fi . A1 & fi . A1 in succ A ) ) ) by A1, A13, ORDINAL2:def 13;
take D = D; :: thesis: ( D in dom (fi *^ B) & ( for A1 being Ordinal st D c= A1 & A1 in dom (fi *^ B) holds
( B1 in (fi *^ B) . A1 & (fi *^ B) . A1 in B2 ) ) )
thus D in dom (fi *^ B) by A14, ORDINAL3:def 5; :: thesis: for A1 being Ordinal st D c= A1 & A1 in dom (fi *^ B) holds
( B1 in (fi *^ B) . A1 & (fi *^ B) . A1 in B2 )
let A1 be Ordinal; :: thesis: ( D c= A1 & A1 in dom (fi *^ B) implies ( B1 in (fi *^ B) . A1 & (fi *^ B) . A1 in B2 ) )
assume A15: ( D c= A1 & A1 in dom (fi *^ B) ) ; :: thesis: ( B1 in (fi *^ B) . A1 & (fi *^ B) . A1 in B2 )
reconsider E = fi . A1 as Ordinal ;
( C in fi . A1 & fi . A1 in succ A ) by A2, A14, A15;
then ( C *^ B in E *^ B & E c= A ) by A6, ORDINAL1:34, ORDINAL2:57;
then ( B1 in E *^ B & E *^ B c= A *^ B & E = E & (fi *^ B) . A1 = (fi . A1) *^ B ) by A2, A13, A15, ORDINAL1:19, ORDINAL2:58, ORDINAL3:def 5;
hence ( B1 in (fi *^ B) . A1 & (fi *^ B) . A1 in B2 ) by A7, ORDINAL1:22; :: thesis: verum

end;

hence ex b₁ being set st
( b₁ in dom (fi *^ B) & ( for b₂ being set holds
( not b₁ c= b₂ or not b₂ in dom (fi *^ B) or ( B1 in (fi *^ B) . b₂ & (fi *^ B) . b₂ in B2 ) ) ) ) by A8; :: thesis: verum

end;

end;