let fi be Ordinal-Sequence; :: thesis: for A being Ordinal
for f1, f2 being Ordinal-Sequence st f1 is increasing & A is_limes_of f2 & sup (rng f1) = dom f2 & fi = f2 * f1 holds
A is_limes_of fi

let A be Ordinal; :: thesis: for f1, f2 being Ordinal-Sequence st f1 is increasing & A is_limes_of f2 & sup (rng f1) = dom f2 & fi = f2 * f1 holds
A is_limes_of fi

let f1, f2 be Ordinal-Sequence; :: thesis: ( f1 is increasing & A is_limes_of f2 & sup (rng f1) = dom f2 & fi = f2 * f1 implies A is_limes_of fi )
assume that
A1: f1 is increasing and
A2: ( ( 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
A3: sup (rng f1) = dom f2 and
A4: fi = f2 * f1 ; :: 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
A5: B in dom f2 and
A6: for C being Ordinal st B c= C & C in dom f2 holds
f2 . C = {} by A2;
consider B1 being Ordinal such that
A7: B1 in rng f1 and
A8: B c= B1 by ;
consider x being object such that
A9: x in dom f1 and
A10: B1 = f1 . x by ;
reconsider x = x as Ordinal by A9;
take x ; :: thesis: ( x in dom fi & ( for b1 being set holds
( not x c= b1 or not b1 in dom fi or fi . b1 = 0 ) ) )

B1 in dom f2 by ;
hence x in dom fi by ; :: thesis: for b1 being set holds
( not x c= b1 or not b1 in dom fi or fi . b1 = 0 )

let C be Ordinal; :: thesis: ( not x c= C or not C in dom fi or fi . C = 0 )
assume that
A11: x c= C and
A12: C in dom fi ; :: thesis: fi . C = 0
reconsider C1 = f1 . C as Ordinal ;
A13: dom fi c= dom f1 by ;
then B1 c= C1 by A1, A10, A11, A12, Th9;
then A14: B c= C1 by A8;
C1 in rng f1 by ;
then f2 . C1 = {} by ;
hence fi . C = 0 by ; :: 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
A15: B in A and
A16: 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 D being Ordinal such that
A17: D in dom f2 and
A18: for A1 being Ordinal st D c= A1 & A1 in dom f2 holds
( B in f2 . A1 & f2 . A1 in C ) by A2, A15, A16;
consider B1 being Ordinal such that
A19: B1 in rng f1 and
A20: D c= B1 by ;
consider x being object such that
A21: x in dom f1 and
A22: B1 = f1 . x by ;
reconsider x = x as Ordinal by A21;
take x ; :: thesis: ( x in dom fi & ( for b1 being set holds
( not x c= b1 or not b1 in dom fi or ( B in fi . b1 & fi . b1 in C ) ) ) )

B1 in dom f2 by ;
hence x in dom fi by ; :: thesis: for b1 being set holds
( not x c= b1 or not b1 in dom fi or ( B in fi . b1 & fi . b1 in C ) )

let E be Ordinal; :: thesis: ( not x c= E or not E in dom fi or ( B in fi . E & fi . E in C ) )
assume that
A23: x c= E and
A24: E in dom fi ; :: thesis: ( B in fi . E & fi . E in C )
reconsider E1 = f1 . E as Ordinal ;
A25: dom fi c= dom f1 by ;
then E1 in rng f1 by ;
then A26: E1 in dom f2 by ;
B1 c= E1 by A1, A22, A23, A24, A25, Th9;
then A27: D c= E1 by A20;
then A28: f2 . E1 in C by ;
B in f2 . E1 by ;
hence ( B in fi . E & fi . E in C ) by ; :: thesis: verum
end;
end;