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
per cases ( A = 0 or A <> 0 ) ;
:: according to ORDINAL2:def 9
case A = 0 ; :: thesis: ex b1 being set st
( b1 in dom fi & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom fi or fi . b2 = 0 ) ) )
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 b1 being set holds
( not B c= b1 or not b1 in dom fi or fi . b1 = 0 ) ) )
thus B in dom fi by A2, A6; :: thesis: for b1 being set holds
( not B c= b1 or not b1 in dom fi or fi . b1 = 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;
case A <> 0 ; :: thesis: for b1, b2 being set holds
( not b1 in A or not A in b2 or ex b3 being set st
( b3 in dom fi & ( for b4 being set holds
( not b3 c= b4 or not b4 in dom fi or ( b1 in fi . b4 & fi . b4 in b2 ) ) ) ) )
let B, C be Ordinal; :: thesis: ( not B in A or not A in C or ex b1 being set st
( b1 in dom fi & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom fi or ( B in fi . b2 & fi . b2 in C ) ) ) ) )
assume that
A10: B in A and
A11: A in C ; :: thesis: ex b1 being set st
( b1 in dom fi & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom fi or ( B in fi . b2 & fi . b2 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 b1 being set holds
( not D c= b1 or not b1 in dom fi or ( B in fi . b1 & fi . b1 in C ) ) ) )
thus D in dom fi by A1, A2, A14, A12, ORDINAL3:12; :: thesis: for b1 being set holds
( not D c= b1 or not b1 in dom fi or ( B in fi . b1 & fi . b1 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;
end;