let fi be Ordinal-Sequence; :: thesis: for A being Ordinal

for f1, f2 being Ordinal-Sequence st dom f1 = dom fi & dom fi = dom f2 & A is_limes_of f1 & A is_limes_of f2 & ( for A being Ordinal st A in dom fi holds

( f1 . A c= fi . A & fi . A c= f2 . A ) ) holds

A is_limes_of fi

let A be Ordinal; :: thesis: for f1, f2 being Ordinal-Sequence st dom f1 = dom fi & dom fi = dom f2 & A is_limes_of f1 & A is_limes_of f2 & ( for A being Ordinal st A in dom fi holds

( f1 . A c= fi . A & fi . A c= f2 . A ) ) holds

A is_limes_of fi

let f1, f2 be Ordinal-Sequence; :: thesis: ( dom f1 = dom fi & dom fi = dom f2 & A is_limes_of f1 & A is_limes_of f2 & ( for A being Ordinal st A in dom fi holds

( f1 . A c= fi . A & fi . A c= f2 . A ) ) implies A is_limes_of fi )

assume that

A1: dom f1 = dom fi and

A2: dom fi = dom f2 and

A3: ( ( A = 0 & ex B being Ordinal st

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

f1 . 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 f1 & ( for E being Ordinal st D c= E & E in dom f1 holds

( B in f1 . E & f1 . E in C ) ) ) ) ) ) and

A4: ( ( A = 0 & ex B being Ordinal st

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

f2 . 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 f2 & ( for E being Ordinal st D c= E & E in dom f2 holds

( B in f2 . E & f2 . E in C ) ) ) ) ) ) and

A5: for A being Ordinal st A in dom fi holds

( f1 . A c= fi . A & fi . A c= f2 . A ) ; :: according to ORDINAL2:def 9 :: thesis: A is_limes_of fi

for f1, f2 being Ordinal-Sequence st dom f1 = dom fi & dom fi = dom f2 & A is_limes_of f1 & A is_limes_of f2 & ( for A being Ordinal st A in dom fi holds

( f1 . A c= fi . A & fi . A c= f2 . A ) ) holds

A is_limes_of fi

let A be Ordinal; :: thesis: for f1, f2 being Ordinal-Sequence st dom f1 = dom fi & dom fi = dom f2 & A is_limes_of f1 & A is_limes_of f2 & ( for A being Ordinal st A in dom fi holds

( f1 . A c= fi . A & fi . A c= f2 . A ) ) holds

A is_limes_of fi

let f1, f2 be Ordinal-Sequence; :: thesis: ( dom f1 = dom fi & dom fi = dom f2 & A is_limes_of f1 & A is_limes_of f2 & ( for A being Ordinal st A in dom fi holds

( f1 . A c= fi . A & fi . A c= f2 . A ) ) implies A is_limes_of fi )

assume that

A1: dom f1 = dom fi and

A2: dom fi = dom f2 and

A3: ( ( A = 0 & ex B being Ordinal st

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

f1 . 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 f1 & ( for E being Ordinal st D c= E & E in dom f1 holds

( B in f1 . E & f1 . E in C ) ) ) ) ) ) and

A4: ( ( A = 0 & ex B being Ordinal st

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

f2 . 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 f2 & ( for E being Ordinal st D c= E & E in dom f2 holds

( B in f2 . E & f2 . E in C ) ) ) ) ) ) and

A5: for A being Ordinal st A in dom fi holds

( f1 . A c= fi . A & fi . A c= f2 . A ) ; :: according to ORDINAL2:def 9 :: thesis: A is_limes_of fi

per cases
( A = 0 or A <> 0 )
;

:: according to ORDINAL2:def 9end;

:: according to ORDINAL2:def 9

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

( b_{1} in dom fi & ( for b_{2} being set holds

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

( b

( not b

then consider B being Ordinal such that

A6: B in dom f2 and

A7: for C being Ordinal st B c= C & C in dom f2 holds

f2 . C = {} by A4;

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

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

thus B in dom fi by A2, A6; :: thesis: for b_{1} being set holds

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

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

assume that

A8: B c= C and

A9: C in dom fi ; :: thesis: fi . C = 0

f2 . C = {} by A2, A7, A8, A9;

hence fi . C = 0 by A5, A9, XBOOLE_1:3; :: thesis: verum

end;A6: B in dom f2 and

A7: for C being Ordinal st B c= C & C in dom f2 holds

f2 . C = {} by A4;

take B ; :: thesis: ( B in dom fi & ( for b

( not B c= b

thus B in dom fi by A2, A6; :: thesis: for b

( not B c= b

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

assume that

A8: B c= C and

A9: C in dom fi ; :: thesis: fi . C = 0

f2 . C = {} by A2, A7, A8, A9;

hence fi . C = 0 by A5, A9, XBOOLE_1:3; :: thesis: verum

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

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

( b_{3} in dom fi & ( for b_{4} being set holds

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

( not b

( b

( not b

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

( b_{1} in dom fi & ( for b_{2} being set holds

( not b_{1} c= b_{2} or not b_{2} in dom fi or ( B in fi . b_{2} & fi . b_{2} in C ) ) ) ) )

assume that

A10: B in A and

A11: A in C ; :: thesis: ex b_{1} being set st

( b_{1} in dom fi & ( for b_{2} being set holds

( not b_{1} c= b_{2} or not b_{2} in dom fi or ( B in fi . b_{2} & fi . b_{2} in C ) ) ) )

consider D2 being Ordinal such that

A12: D2 in dom f2 and

A13: for A1 being Ordinal st D2 c= A1 & A1 in dom f2 holds

( B in f2 . A1 & f2 . A1 in C ) by A4, A10, A11;

consider D1 being Ordinal such that

A14: D1 in dom f1 and

A15: for A1 being Ordinal st D1 c= A1 & A1 in dom f1 holds

( B in f1 . A1 & f1 . A1 in C ) by A3, A10, A11;

take D = D1 \/ D2; :: thesis: ( D in dom fi & ( for b_{1} being set holds

( not D c= b_{1} or not b_{1} in dom fi or ( B in fi . b_{1} & fi . b_{1} in C ) ) ) )

thus D in dom fi by A1, A2, A14, A12, ORDINAL3:12; :: thesis: for b_{1} being set holds

( not D c= b_{1} or not b_{1} in dom fi or ( B in fi . b_{1} & fi . b_{1} in C ) )

let A1 be Ordinal; :: thesis: ( not D c= A1 or not A1 in dom fi or ( B in fi . A1 & fi . A1 in C ) )

assume that

A16: D c= A1 and

A17: A1 in dom fi ; :: thesis: ( B in fi . A1 & fi . A1 in C )

reconsider B1 = fi . A1, B2 = f2 . A1 as Ordinal ;

A18: B1 c= B2 by A5, A17;

D2 c= D by XBOOLE_1:7;

then D2 c= A1 by A16;

then A19: B2 in C by A2, A13, A17;

D1 c= D by XBOOLE_1:7;

then D1 c= A1 by A16;

then A20: B in f1 . A1 by A1, A15, A17;

f1 . A1 c= fi . A1 by A5, A17;

hence ( B in fi . A1 & fi . A1 in C ) by A20, A18, A19, ORDINAL1:12; :: thesis: verum

end;( b

( not b

assume that

A10: B in A and

A11: A in C ; :: thesis: ex b

( b

( not b

consider D2 being Ordinal such that

A12: D2 in dom f2 and

A13: for A1 being Ordinal st D2 c= A1 & A1 in dom f2 holds

( B in f2 . A1 & f2 . A1 in C ) by A4, A10, A11;

consider D1 being Ordinal such that

A14: D1 in dom f1 and

A15: for A1 being Ordinal st D1 c= A1 & A1 in dom f1 holds

( B in f1 . A1 & f1 . A1 in C ) by A3, A10, A11;

take D = D1 \/ D2; :: thesis: ( D in dom fi & ( for b

( not D c= b

thus D in dom fi by A1, A2, A14, A12, ORDINAL3:12; :: thesis: for b

( not D c= b

let A1 be Ordinal; :: thesis: ( not D c= A1 or not A1 in dom fi or ( B in fi . A1 & fi . A1 in C ) )

assume that

A16: D c= A1 and

A17: A1 in dom fi ; :: thesis: ( B in fi . A1 & fi . A1 in C )

reconsider B1 = fi . A1, B2 = f2 . A1 as Ordinal ;

A18: B1 c= B2 by A5, A17;

D2 c= D by XBOOLE_1:7;

then D2 c= A1 by A16;

then A19: B2 in C by A2, A13, A17;

D1 c= D by XBOOLE_1:7;

then D1 c= A1 by A16;

then A20: B in f1 . A1 by A1, A15, A17;

f1 . A1 c= fi . A1 by A5, A17;

hence ( B in fi . A1 & fi . A1 in C ) by A20, A18, A19, ORDINAL1:12; :: thesis: verum