let fi be Ordinal-Sequence; :: thesis: for A, B being Ordinal st A is_limes_of fi holds

B +^ A is_limes_of B +^ fi

let A, B be Ordinal; :: thesis: ( A is_limes_of fi implies B +^ A is_limes_of B +^ fi )

assume A1: ( ( A = 0 & ex B being Ordinal st

( B in dom fi & ( for C being Ordinal st B c= C & C in dom fi holds

fi . C = 0 ) ) ) or ( A <> 0 & ( for B, C being Ordinal st B in A & A in C holds

ex D being Ordinal st

( D in dom fi & ( for E being Ordinal st D c= E & E in dom fi holds

( B in fi . E & fi . E in C ) ) ) ) ) ) ; :: according to ORDINAL2:def 9 :: thesis: B +^ A is_limes_of B +^ fi

A2: dom fi = dom (B +^ fi) by ORDINAL3:def 1;

B +^ A is_limes_of B +^ fi

let A, B be Ordinal; :: thesis: ( A is_limes_of fi implies B +^ A is_limes_of B +^ fi )

assume A1: ( ( A = 0 & ex B being Ordinal st

( B in dom fi & ( for C being Ordinal st B c= C & C in dom fi holds

fi . C = 0 ) ) ) or ( A <> 0 & ( for B, C being Ordinal st B in A & A in C holds

ex D being Ordinal st

( D in dom fi & ( for E being Ordinal st D c= E & E in dom fi holds

( B in fi . E & fi . E in C ) ) ) ) ) ) ; :: according to ORDINAL2:def 9 :: thesis: B +^ A is_limes_of B +^ fi

A2: dom fi = dom (B +^ fi) by ORDINAL3:def 1;

per cases
( B +^ A = 0 or B +^ A <> 0 )
;

:: according to ORDINAL2:def 9end;

:: according to ORDINAL2:def 9

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

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

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

( b

( not b

then consider A1 being Ordinal such that

A4: A1 in dom fi and

A5: for C being Ordinal st A1 c= C & C in dom fi holds

fi . C = {} by A1, ORDINAL3:26;

take A1 ; :: thesis: ( A1 in dom (B +^ fi) & ( for b_{1} being set holds

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

thus A1 in dom (B +^ fi) by A4, ORDINAL3:def 1; :: thesis: for b_{1} being set holds

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

let C be Ordinal; :: thesis: ( not A1 c= C or not C in dom (B +^ fi) or (B +^ fi) . C = 0 )

assume that

A6: A1 c= C and

A7: C in dom (B +^ fi) ; :: thesis: (B +^ fi) . C = 0

A8: (B +^ fi) . C = B +^ (fi . C) by A2, A7, ORDINAL3:def 1;

fi . C = {} by A2, A5, A6, A7;

hence (B +^ fi) . C = 0 by A3, A8, ORDINAL3:26; :: thesis: verum

end;A4: A1 in dom fi and

A5: for C being Ordinal st A1 c= C & C in dom fi holds

fi . C = {} by A1, ORDINAL3:26;

take A1 ; :: thesis: ( A1 in dom (B +^ fi) & ( for b

( not A1 c= b

thus A1 in dom (B +^ fi) by A4, ORDINAL3:def 1; :: thesis: for b

( not A1 c= b

let C be Ordinal; :: thesis: ( not A1 c= C or not C in dom (B +^ fi) or (B +^ fi) . C = 0 )

assume that

A6: A1 c= C and

A7: C in dom (B +^ fi) ; :: thesis: (B +^ fi) . C = 0

A8: (B +^ fi) . C = B +^ (fi . C) by A2, A7, ORDINAL3:def 1;

fi . C = {} by A2, A5, A6, A7;

hence (B +^ fi) . C = 0 by A3, A8, ORDINAL3:26; :: thesis: verum

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

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

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

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

_{1}, b_{2} being set holds

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

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

( not b_{3} c= b_{4} or not b_{4} in dom (B +^ fi) or ( b_{1} in (B +^ fi) . b_{4} & (B +^ fi) . b_{4} in b_{2} ) ) ) ) )
; :: thesis: verum

end;

( not b

( b

( not b

now :: thesis: for B1, B2 being Ordinal st B1 in B +^ A & B +^ A in B2 holds

ex A1 being Ordinal st

( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds

( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) )end;

hence
for bex A1 being Ordinal st

( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds

( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) )

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

end;

suppose A9:
A = {}
; :: thesis: for B1, B2 being Ordinal st B1 in B +^ A & B +^ A in B2 holds

ex A1 being Ordinal st

( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds

( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) )

ex A1 being Ordinal st

( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds

( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) )

then consider A1 being Ordinal such that

A10: A1 in dom fi and

A11: for C being Ordinal st A1 c= C & C in dom fi holds

fi . C = {} by A1;

let B1, B2 be Ordinal; :: thesis: ( B1 in B +^ A & B +^ A in B2 implies ex A1 being Ordinal st

( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds

( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) ) )

assume that

A12: B1 in B +^ A and

A13: B +^ A in B2 ; :: thesis: ex A1 being Ordinal st

( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds

( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) )

take A1 = A1; :: thesis: ( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds

( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) )

thus A1 in dom (B +^ fi) by A10, ORDINAL3:def 1; :: thesis: for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds

( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 )

let C be Ordinal; :: thesis: ( A1 c= C & C in dom (B +^ fi) implies ( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) )

assume that

A14: A1 c= C and

A15: C in dom (B +^ fi) ; :: thesis: ( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 )

(B +^ fi) . C = B +^ (fi . C) by A2, A15, ORDINAL3:def 1;

hence ( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) by A2, A9, A11, A12, A13, A14, A15; :: thesis: verum

end;A10: A1 in dom fi and

A11: for C being Ordinal st A1 c= C & C in dom fi holds

fi . C = {} by A1;

let B1, B2 be Ordinal; :: thesis: ( B1 in B +^ A & B +^ A in B2 implies ex A1 being Ordinal st

( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds

( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) ) )

assume that

A12: B1 in B +^ A and

A13: B +^ A in B2 ; :: thesis: ex A1 being Ordinal st

( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds

( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) )

take A1 = A1; :: thesis: ( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds

( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) )

thus A1 in dom (B +^ fi) by A10, ORDINAL3:def 1; :: thesis: for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds

( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 )

let C be Ordinal; :: thesis: ( A1 c= C & C in dom (B +^ fi) implies ( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) )

assume that

A14: A1 c= C and

A15: C in dom (B +^ fi) ; :: thesis: ( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 )

(B +^ fi) . C = B +^ (fi . C) by A2, A15, ORDINAL3:def 1;

hence ( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) by A2, A9, A11, A12, A13, A14, A15; :: thesis: verum

suppose A16:
A <> {}
; :: thesis: for B1, B2 being Ordinal st B1 in B +^ A & B +^ A in B2 holds

ex A1 being Ordinal st

( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds

( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) )

ex A1 being Ordinal st

( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds

( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) )

let B1, B2 be Ordinal; :: thesis: ( B1 in B +^ A & B +^ A in B2 implies ex A1 being Ordinal st

( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds

( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) ) )

assume that

A17: B1 in B +^ A and

A18: B +^ A in B2 ; :: thesis: ex A1 being Ordinal st

( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds

( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) )

B1 -^ B in A by A16, A17, ORDINAL3:60;

then consider A1 being Ordinal such that

A19: A1 in dom fi and

A20: for C being Ordinal st A1 c= C & C in dom fi holds

( B1 -^ B in fi . C & fi . C in B2 -^ B ) by A1, A18, ORDINAL3:61;

A21: B1 c= B +^ (B1 -^ B) by ORDINAL3:62;

A22: B c= B +^ A by ORDINAL3:24;

B +^ A c= B2 by A18, ORDINAL1:def 2;

then B c= B2 by A22;

then A23: B +^ (B2 -^ B) = B2 by ORDINAL3:def 5;

take A1 = A1; :: thesis: ( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds

( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) )

thus A1 in dom (B +^ fi) by A19, ORDINAL3:def 1; :: thesis: for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds

( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 )

let C be Ordinal; :: thesis: ( A1 c= C & C in dom (B +^ fi) implies ( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) )

assume that

A24: A1 c= C and

A25: C in dom (B +^ fi) ; :: thesis: ( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 )

A26: (B +^ fi) . C = B +^ (fi . C) by A2, A25, ORDINAL3:def 1;

reconsider E = fi . C as Ordinal ;

B1 -^ B in E by A2, A20, A24, A25;

then A27: B +^ (B1 -^ B) in B +^ E by ORDINAL2:32;

E in B2 -^ B by A2, A20, A24, A25;

hence ( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) by A21, A26, A23, A27, ORDINAL1:12, ORDINAL2:32; :: thesis: verum

end;( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds

( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) ) )

assume that

A17: B1 in B +^ A and

A18: B +^ A in B2 ; :: thesis: ex A1 being Ordinal st

( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds

( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) )

B1 -^ B in A by A16, A17, ORDINAL3:60;

then consider A1 being Ordinal such that

A19: A1 in dom fi and

A20: for C being Ordinal st A1 c= C & C in dom fi holds

( B1 -^ B in fi . C & fi . C in B2 -^ B ) by A1, A18, ORDINAL3:61;

A21: B1 c= B +^ (B1 -^ B) by ORDINAL3:62;

A22: B c= B +^ A by ORDINAL3:24;

B +^ A c= B2 by A18, ORDINAL1:def 2;

then B c= B2 by A22;

then A23: B +^ (B2 -^ B) = B2 by ORDINAL3:def 5;

take A1 = A1; :: thesis: ( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds

( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) )

thus A1 in dom (B +^ fi) by A19, ORDINAL3:def 1; :: thesis: for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds

( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 )

let C be Ordinal; :: thesis: ( A1 c= C & C in dom (B +^ fi) implies ( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) )

assume that

A24: A1 c= C and

A25: C in dom (B +^ fi) ; :: thesis: ( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 )

A26: (B +^ fi) . C = B +^ (fi . C) by A2, A25, ORDINAL3:def 1;

reconsider E = fi . C as Ordinal ;

B1 -^ B in E by A2, A20, A24, A25;

then A27: B +^ (B1 -^ B) in B +^ E by ORDINAL2:32;

E in B2 -^ B by A2, A20, A24, A25;

hence ( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) by A21, A26, A23, A27, ORDINAL1:12, ORDINAL2:32; :: thesis: verum

( not b

( b

( not b