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

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 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

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_{1} being set holds

( not x c= b_{1} or not b_{1} in dom fi or fi . b_{1} = 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_{1} being set holds

( not x c= b_{1} or not b_{1} in dom fi or fi . b_{1} = 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;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

( not x c= b

B1 in dom f2 by A3, A7, ORDINAL2:19;

hence x in dom fi by A4, A9, A10, FUNCT_1:11; :: thesis: for b

( not x c= b

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

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

A15: B in A and

A16: 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 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_{1} being set holds

( not x c= b_{1} or not b_{1} in dom fi or ( B in fi . b_{1} & fi . b_{1} 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_{1} being set holds

( not x c= b_{1} or not b_{1} in dom fi or ( B in fi . b_{1} & fi . b_{1} 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;( b

( not b

assume that

A15: B in A and

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

( b

( not b

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

( not x c= b

B1 in dom f2 by A3, A19, ORDINAL2:19;

hence x in dom fi by A4, A21, A22, FUNCT_1:11; :: thesis: for b

( not x c= b

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