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 & dom fi = dom f2 ) and
A2: ( ( A = {} & ex B being Ordinal st
( B in dom f1 & ( for C being Ordinal st B c= C & C in dom f1 holds
f1 . C = {} ) ) ) or ( A <> {} & ( 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
A3: ( ( A = {} & ex B being Ordinal st
( B in dom f2 & ( for C being Ordinal st B c= C & C in dom f2 holds
f2 . C = {} ) ) ) or ( A <> {} & ( 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
A4: for A being Ordinal st A in dom fi holds
( f1 . A c= fi . A & fi . A c= f2 . A ) ; :: according to ORDINAL2:def 13 :: thesis: A is_limes_of fi

per cases ( A = {} or A <> {} ) ;
:: according to ORDINAL2:def 13

case A = {} ; :: thesis: ex b₁ being set st
( b₁ in dom fi & ( for b₂ being set holds
( not b₁ c= b₂ or not b₂ in dom fi or fi . b₂ = {} ) ) )

then consider B being Ordinal such that
A5: ( B in dom f2 & ( for C being Ordinal st B c= C & C in dom f2 holds
f2 . C = {} ) ) by A3;
take B ; :: thesis: ( B in dom fi & ( for b₁ being set holds
( not B c= b₁ or not b₁ in dom fi or fi . b₁ = {} ) ) )
thus B in dom fi by A1, A5; :: thesis: for b₁ being set holds
( not B c= b₁ or not b₁ in dom fi or fi . b₁ = {} )
let C be Ordinal; :: thesis: ( not B c= C or not C in dom fi or fi . C = {} )
assume ( B c= C & C in dom fi ) ; :: thesis: fi . C = {}
then ( f2 . C = {} & fi . C c= f2 . C ) by A1, A4, A5;
hence fi . C = {} by XBOOLE_1:3; :: thesis: verum

end;

case A <> {} ; :: thesis: for b₁, b₂ being set holds
( not b₁ in A or not A in b₂ or ex b₃ being set st
( b₃ in dom fi & ( for b₄ being set holds
( not b₃ c= b₄ or not b₄ in dom fi or ( b₁ in fi . b₄ & fi . b₄ in b₂ ) ) ) ) )

let B, C be Ordinal; :: thesis: ( not B in A or not A in C or ex b₁ being set st
( b₁ in dom fi & ( for b₂ being set holds
( not b₁ c= b₂ or not b₂ in dom fi or ( B in fi . b₂ & fi . b₂ in C ) ) ) ) )
assume A6: ( B in A & A in C ) ; :: thesis: ex b₁ being set st
( b₁ in dom fi & ( for b₂ being set holds
( not b₁ c= b₂ or not b₂ in dom fi or ( B in fi . b₂ & fi . b₂ in C ) ) ) )
then consider D1 being Ordinal such that
A7: ( D1 in dom f1 & ( for A1 being Ordinal st D1 c= A1 & A1 in dom f1 holds
( B in f1 . A1 & f1 . A1 in C ) ) ) by A2;
consider D2 being Ordinal such that
A8: ( D2 in dom f2 & ( for A1 being Ordinal st D2 c= A1 & A1 in dom f2 holds
( B in f2 . A1 & f2 . A1 in C ) ) ) by A3, A6;
take D = D1 \/ D2; :: thesis: ( D in dom fi & ( for b₁ being set holds
( not D c= b₁ or not b₁ in dom fi or ( B in fi . b₁ & fi . b₁ in C ) ) ) )
thus D in dom fi by A1, A7, A8, ORDINAL3:15; :: thesis: for b₁ being set holds
( not D c= b₁ or not b₁ in dom fi or ( B in fi . b₁ & fi . b₁ 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 A9: ( D c= A1 & A1 in dom fi ) ; :: thesis: ( B in fi . A1 & fi . A1 in C )
reconsider B1 = fi . A1, B2 = f2 . A1 as Ordinal ;
( D1 c= D & D2 c= D ) by XBOOLE_1:7;
then ( D1 c= A1 & D2 c= A1 ) by A9, XBOOLE_1:1;
then ( B in f1 . A1 & f1 . A1 c= fi . A1 & B1 c= B2 & B2 in C ) by A1, A4, A7, A8, A9;
hence ( B in fi . A1 & fi . A1 in C ) by ORDINAL1:22; :: thesis: verum

end;

end;