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 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₂ = 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 A3, A5, ORDINAL2:21;
consider x being object such that
A9: x in dom f1 and
A10: B1 = f1 . x by A7, FUNCT_1:def 3;
reconsider x = x as Ordinal by A9;
take x ; :: thesis: ( x in dom fi & ( for b₁ being set holds
( not x c= b₁ or not b₁ in dom fi or fi . b₁ = 0 ) ) )
B1 in dom f2 by A3, A7, ORDINAL2:19;
hence x in dom fi by A4, A9, A10, FUNCT_1:11; :: thesis: for b₁ being set holds
( not x c= b₁ or not b₁ in dom fi or fi . b₁ = 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 A4, RELAT_1:25;
then B1 c= C1 by A1, A10, A11, A12, Th9;
then A14: B c= C1 by A8;
C1 in rng f1 by A12, A13, FUNCT_1:def 3;
then f2 . C1 = {} by A3, A6, A14, ORDINAL2:19;
hence fi . C = 0 by A4, A12, FUNCT_1:12; :: thesis: verum

end;

case A <> 0 ; :: 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 that
A15: B in A and
A16: 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 ) ) ) )
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 A3, A17, ORDINAL2:21;
consider x being object such that
A21: x in dom f1 and
A22: B1 = f1 . x by A19, FUNCT_1:def 3;
reconsider x = x as Ordinal by A21;
take x ; :: thesis: ( x in dom fi & ( for b₁ being set holds
( not x c= b₁ or not b₁ in dom fi or ( B in fi . b₁ & fi . b₁ in C ) ) ) )
B1 in dom f2 by A3, A19, ORDINAL2:19;
hence x in dom fi by A4, A21, A22, FUNCT_1:11; :: thesis: for b₁ being set holds
( not x c= b₁ or not b₁ in dom fi or ( B in fi . b₁ & fi . b₁ 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 A4, RELAT_1:25;
then E1 in rng f1 by A24, FUNCT_1:def 3;
then A26: E1 in dom f2 by A3, ORDINAL2:19;
B1 c= E1 by A1, A22, A23, A24, A25, Th9;
then A27: D c= E1 by A20;
then A28: f2 . E1 in C by A18, A26;
B in f2 . E1 by A18, A27, A26;
hence ( B in fi . E & fi . E in C ) by A4, A24, A28, FUNCT_1:12; :: thesis: verum

end;

end;