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 )
A1: dom fi = dom (fi *^ B) by ORDINAL3:def 4;
assume A2: A is_limes_of fi ; :: thesis: A *^ B is_limes_of fi *^ B
then A3: dom fi <> {} by Lm4;
per cases ( A *^ B = 0 or A *^ B <> 0 ) ;
:: according to ORDINAL2:def 9
case A *^ B = 0 ; :: thesis: ex b1 being set st
( b1 in dom (fi *^ B) & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom (fi *^ B) or (fi *^ B) . b2 = 0 ) ) )

then A4: ( B = {} or A = {} ) by ORDINAL3:31;
now :: 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 = {} ) )
per cases ( B = {} or B <> {} ) ;
suppose A5: 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 = {} ) )

set x = the Element of dom fi;
reconsider x = the Element of dom fi 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 A1, A3; :: 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 that
A1 c= C and
A6: C in dom (fi *^ B) ; :: thesis: (fi *^ B) . C = {}
thus (fi *^ B) . C = (fi . C) *^ B by
.= {} by ; :: 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
A7: A1 in dom fi and
A8: for C being Ordinal st A1 c= C & C in dom fi holds
fi . C = {} by ;
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 ; :: 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 that
A9: A1 c= C and
A10: C in dom (fi *^ B) ; :: thesis: (fi *^ B) . C = {}
A11: (fi *^ B) . C = (fi . C) *^ B by ;
fi . C = {} by A1, A8, A9, A10;
hence (fi *^ B) . C = {} by ; :: thesis: verum
end;
end;
end;
hence ex b1 being set st
( b1 in dom (fi *^ B) & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom (fi *^ B) or (fi *^ B) . b2 = 0 ) ) ) ; :: thesis: verum
end;
case A12: A *^ B <> 0 ; :: thesis: for b1, b2 being set holds
( not b1 in A *^ B or not A *^ B in b2 or ex b3 being set st
( b3 in dom (fi *^ B) & ( for b4 being set holds
( not b3 c= b4 or not b4 in dom (fi *^ B) or ( b1 in (fi *^ B) . b4 & (fi *^ B) . b4 in b2 ) ) ) ) )

let B1, B2 be Ordinal; :: thesis: ( not B1 in A *^ B or not A *^ B in B2 or ex b1 being set st
( b1 in dom (fi *^ B) & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom (fi *^ B) or ( B1 in (fi *^ B) . b2 & (fi *^ B) . b2 in B2 ) ) ) ) )

assume that
A13: B1 in A *^ B and
A14: A *^ B in B2 ; :: thesis: ex b1 being set st
( b1 in dom (fi *^ B) & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom (fi *^ B) or ( B1 in (fi *^ B) . b2 & (fi *^ B) . b2 in B2 ) ) ) )

A15: B <> {} by ;
A16: now :: thesis: ( ( for A1 being Ordinal holds not A = succ A1 ) implies 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 ) ) ) )
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:29;
then consider C being Ordinal such that
A17: C in A and
A18: B1 in C *^ B by ;
A in succ A by ORDINAL1:6;
then consider D being Ordinal such that
A19: D in dom fi and
A20: for A1 being Ordinal st D c= A1 & A1 in dom fi holds
( C in fi . A1 & fi . A1 in succ A ) by ;
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 ; :: 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 that
A21: D c= A1 and
A22: A1 in dom (fi *^ B) ; :: thesis: ( B1 in (fi *^ B) . A1 & (fi *^ B) . A1 in B2 )
reconsider E = fi . A1 as Ordinal ;
fi . A1 in succ A by A1, A20, A21, A22;
then A23: E c= A by ORDINAL1:22;
C in fi . A1 by A1, A20, A21, A22;
then C *^ B in E *^ B by ;
then A24: B1 in E *^ B by ;
(fi *^ B) . A1 = (fi . A1) *^ B by ;
hence ( B1 in (fi *^ B) . A1 & (fi *^ B) . A1 in B2 ) by ; :: thesis: verum
end;
now :: thesis: ( ex A1 being Ordinal st A = succ A1 implies 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 ) ) ) )
A25: A in succ A by ORDINAL1:6;
given A1 being Ordinal such that A26: 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 by ;
then consider D being Ordinal such that
A27: D in dom fi and
A28: for C being Ordinal st D c= C & C in dom fi holds
( A1 in fi . C & fi . C in succ A ) by ;
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 ; :: 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 that
A29: D c= C and
A30: C in dom (fi *^ B) ; :: thesis: ( B1 in (fi *^ B) . C & (fi *^ B) . C in B2 )
reconsider E = fi . C as Ordinal ;
A1 in E by A1, A28, A29, A30;
then A31: A c= E by ;
E in succ A by A1, A28, A29, A30;
then A32: E c= A by ORDINAL1:22;
(fi *^ B) . C = E *^ B by ;
hence ( B1 in (fi *^ B) . C & (fi *^ B) . C in B2 ) by ; :: thesis: verum
end;
hence ex b1 being set st
( b1 in dom (fi *^ B) & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom (fi *^ B) or ( B1 in (fi *^ B) . b2 & (fi *^ B) . b2 in B2 ) ) ) ) by A16; :: thesis: verum
end;
end;