let fi be Ordinal-Sequence; :: thesis:
let A, B be Ordinal; :: thesis:
A1: dom fi = dom (fi *^ B) by ORDINAL3:def 4;
assume A2: A is_limes_of fi ; :: thesis:
then A3: dom fi <> {} by Lm4;

per cases ;
:: according to ORDINAL2:def 9

case A *^ B = 0 ; :: thesis:

then A4: ( B = {} or A = {} ) by ORDINAL3:31;

now :: thesis:

per cases ;

suppose A5: B = {} ; :: thesis:

set x = the Element of dom fi;
reconsider x = the Element of dom fi as Ordinal ;
take A1 = x; :: thesis:
thus A1 in dom (fi *^ B) by A1, A3; :: thesis:
let C be Ordinal; :: thesis:
assume that
A1 c= C and
A6: C in dom (fi *^ B) ; :: thesis:
thus (fi *^ B) . C = (fi . C) *^ B by A1, A6, ORDINAL3:def 4
.= {} by A5, ORDINAL2:38 ; :: thesis:

end;

suppose B <> {} ; :: thesis:

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 A2, A4, ORDINAL2:def 9;
take A1 = A1; :: thesis:
thus A1 in dom (fi *^ B) by A7, ORDINAL3:def 4; :: thesis:
let C be Ordinal; :: thesis:
assume that
A9: A1 c= C and
A10: C in dom (fi *^ B) ; :: thesis:
A11: (fi *^ B) . C = (fi . C) *^ B by A1, A10, ORDINAL3:def 4;
fi . C = {} by A1, A8, A9, A10;
hence (fi *^ B) . C = {} by A11, ORDINAL2:35; :: thesis:

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₂ = 0 ) ) ) ; :: thesis:

end;

case A12: A *^ B <> 0 ; :: thesis:

let B1, B2 be Ordinal; :: thesis:
assume that
A13: B1 in A *^ B and
A14: A *^ B in B2 ; :: thesis:
A15: B <> {} by A12, ORDINAL2:38;

A16: now :: thesis:

assume for A1 being Ordinal holds not A = succ A1 ; :: thesis:
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 A13, ORDINAL3:41;
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 A2, A17, ORDINAL2:def 9;
take D = D; :: thesis:
thus D in dom (fi *^ B) by A19, ORDINAL3:def 4; :: thesis:
let A1 be Ordinal; :: thesis:
assume that
A21: D c= A1 and
A22: A1 in dom (fi *^ B) ; :: thesis:
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 A15, ORDINAL2:40;
then A24: B1 in E *^ B by A18, ORDINAL1:10;
(fi *^ B) . A1 = (fi . A1) *^ B by A1, A22, ORDINAL3:def 4;
hence ( B1 in (fi *^ B) . A1 & (fi *^ B) . A1 in B2 ) by A14, A23, A24, ORDINAL1:12, ORDINAL2:41; :: thesis:

end;

now :: thesis:

A25: A in succ A by ORDINAL1:6;
given A1 being Ordinal such that A26: A = succ A1 ; :: thesis:
A1 in A by A26, ORDINAL1:6;
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 A2, A25, ORDINAL2:def 9;
take D = D; :: thesis:
thus D in dom (fi *^ B) by A27, ORDINAL3:def 4; :: thesis:
let C be Ordinal; :: thesis:
assume that
A29: D c= C and
A30: C in dom (fi *^ B) ; :: thesis:
reconsider E = fi . C as Ordinal ;
A1 in E by A1, A28, A29, A30;
then A31: A c= E by A26, ORDINAL1:21;
E in succ A by A1, A28, A29, A30;
then A32: E c= A by ORDINAL1:22;
(fi *^ B) . C = E *^ B by A1, A30, ORDINAL3:def 4;
hence ( B1 in (fi *^ B) . C & (fi *^ B) . C in B2 ) by A13, A14, A31, A32, XBOOLE_0:def 10; :: thesis:

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 A16; :: thesis:

end;

end;