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;

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 9end;

:: according to ORDINAL2:def 9

case
A *^ B = 0
; :: thesis: ex b_{1} being set st

( b_{1} in dom (fi *^ B) & ( for b_{2} being set holds

( not b_{1} c= b_{2} or not b_{2} in dom (fi *^ B) or (fi *^ B) . b_{2} = 0 ) ) )

( b

( not b

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

_{1} being set st

( b_{1} in dom (fi *^ B) & ( for b_{2} being set holds

( not b_{1} c= b_{2} or not b_{2} in dom (fi *^ B) or (fi *^ B) . b_{2} = 0 ) ) )
; :: thesis: verum

end;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 = {} ) )end;

hence
ex b( 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 <> {} )
;

end;

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 = {} ) )

( 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 A1, A6, ORDINAL3:def 4

.= {} by A5, ORDINAL2:38 ; :: thesis: verum

end;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 A1, A6, ORDINAL3:def 4

.= {} by A5, ORDINAL2:38 ; :: thesis: verum

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 = {} ) )

( 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 A2, A4, ORDINAL2:def 9;

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 A7, ORDINAL3:def 4; :: 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 A1, A10, ORDINAL3:def 4;

fi . C = {} by A1, A8, A9, A10;

hence (fi *^ B) . C = {} by A11, ORDINAL2:35; :: thesis: verum

end;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: ( 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 A7, ORDINAL3:def 4; :: 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 A1, A10, ORDINAL3:def 4;

fi . C = {} by A1, A8, A9, A10;

hence (fi *^ B) . C = {} by A11, ORDINAL2:35; :: thesis: verum

( b

( not b

case A12:
A *^ B <> 0
; :: thesis: for b_{1}, b_{2} being set holds

( not b_{1} in A *^ B or not A *^ B in b_{2} or ex b_{3} being set st

( b_{3} in dom (fi *^ B) & ( for b_{4} being set holds

( not b_{3} c= b_{4} or not b_{4} in dom (fi *^ B) or ( b_{1} in (fi *^ B) . b_{4} & (fi *^ B) . b_{4} in b_{2} ) ) ) ) )

( not b

( b

( not b

let B1, B2 be Ordinal; :: thesis: ( not B1 in A *^ B or not A *^ B in B2 or ex b_{1} being set st

( b_{1} in dom (fi *^ B) & ( for b_{2} being set holds

( not b_{1} c= b_{2} or not b_{2} in dom (fi *^ B) or ( B1 in (fi *^ B) . b_{2} & (fi *^ B) . b_{2} in B2 ) ) ) ) )

assume that

A13: B1 in A *^ B and

A14: A *^ B in B2 ; :: thesis: ex b_{1} being set st

( b_{1} in dom (fi *^ B) & ( for b_{2} being set holds

( not b_{1} c= b_{2} or not b_{2} in dom (fi *^ B) or ( B1 in (fi *^ B) . b_{2} & (fi *^ B) . b_{2} in B2 ) ) ) )

A15: B <> {} by A12, ORDINAL2:38;

_{1} being set st

( b_{1} in dom (fi *^ B) & ( for b_{2} being set holds

( not b_{1} c= b_{2} or not b_{2} in dom (fi *^ B) or ( B1 in (fi *^ B) . b_{2} & (fi *^ B) . b_{2} in B2 ) ) ) )
by A16; :: thesis: verum

end;( b

( not b

assume that

A13: B1 in A *^ B and

A14: A *^ B in B2 ; :: thesis: ex b

( b

( not b

A15: B <> {} by A12, ORDINAL2:38;

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 ) ) ) )

( 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 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: ( 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 A19, ORDINAL3:def 4; :: 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 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: verum

end;( 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 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: ( 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 A19, ORDINAL3:def 4; :: 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 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: verum

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 ) ) ) )

hence
ex b( 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 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: ( 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 A27, ORDINAL3:def 4; :: 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 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: verum

end;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 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: ( 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 A27, ORDINAL3:def 4; :: 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 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: verum

( b

( not b