let fi, psi be Ordinal-Sequence; :: thesis: for A being Ordinal st A is_limes_of psi holds

A is_limes_of fi ^ psi

let A be Ordinal; :: thesis: ( A is_limes_of psi implies A is_limes_of fi ^ psi )

assume A1: ( ( A = 0 & ex B being Ordinal st

( B in dom psi & ( for C being Ordinal st B c= C & C in dom psi holds

psi . 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 psi & ( for E being Ordinal st D c= E & E in dom psi holds

( B in psi . E & psi . E in C ) ) ) ) ) ) ; :: according to ORDINAL2:def 9 :: thesis: A is_limes_of fi ^ psi

A2: dom (fi ^ psi) = (dom fi) +^ (dom psi) by Def1;

A is_limes_of fi ^ psi

let A be Ordinal; :: thesis: ( A is_limes_of psi implies A is_limes_of fi ^ psi )

assume A1: ( ( A = 0 & ex B being Ordinal st

( B in dom psi & ( for C being Ordinal st B c= C & C in dom psi holds

psi . 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 psi & ( for E being Ordinal st D c= E & E in dom psi holds

( B in psi . E & psi . E in C ) ) ) ) ) ) ; :: according to ORDINAL2:def 9 :: thesis: A is_limes_of fi ^ psi

A2: dom (fi ^ psi) = (dom fi) +^ (dom psi) by Def1;

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 ^ psi) & ( for b_{2} being set holds

( not b_{1} c= b_{2} or not b_{2} in dom (fi ^ psi) or (fi ^ psi) . b_{2} = 0 ) ) )

( b

( not b

then consider B being Ordinal such that

A3: B in dom psi and

A4: for C being Ordinal st B c= C & C in dom psi holds

psi . C = {} by A1;

take B1 = (dom fi) +^ B; :: thesis: ( B1 in dom (fi ^ psi) & ( for b_{1} being set holds

( not B1 c= b_{1} or not b_{1} in dom (fi ^ psi) or (fi ^ psi) . b_{1} = 0 ) ) )

thus B1 in dom (fi ^ psi) by A2, A3, ORDINAL2:32; :: thesis: for b_{1} being set holds

( not B1 c= b_{1} or not b_{1} in dom (fi ^ psi) or (fi ^ psi) . b_{1} = 0 )

let C be Ordinal; :: thesis: ( not B1 c= C or not C in dom (fi ^ psi) or (fi ^ psi) . C = 0 )

assume that

A5: B1 c= C and

A6: C in dom (fi ^ psi) ; :: thesis: (fi ^ psi) . C = 0

A7: C = B1 +^ (C -^ B1) by A5, ORDINAL3:def 5

.= (dom fi) +^ (B +^ (C -^ B1)) by ORDINAL3:30 ;

then A8: B +^ (C -^ B1) in dom psi by A2, A6, ORDINAL3:22;

B c= B +^ (C -^ B1) by ORDINAL3:24;

then psi . (B +^ (C -^ B1)) = {} by A2, A4, A6, A7, ORDINAL3:22;

hence (fi ^ psi) . C = 0 by A7, A8, Def1; :: thesis: verum

end;A3: B in dom psi and

A4: for C being Ordinal st B c= C & C in dom psi holds

psi . C = {} by A1;

take B1 = (dom fi) +^ B; :: thesis: ( B1 in dom (fi ^ psi) & ( for b

( not B1 c= b

thus B1 in dom (fi ^ psi) by A2, A3, ORDINAL2:32; :: thesis: for b

( not B1 c= b

let C be Ordinal; :: thesis: ( not B1 c= C or not C in dom (fi ^ psi) or (fi ^ psi) . C = 0 )

assume that

A5: B1 c= C and

A6: C in dom (fi ^ psi) ; :: thesis: (fi ^ psi) . C = 0

A7: C = B1 +^ (C -^ B1) by A5, ORDINAL3:def 5

.= (dom fi) +^ (B +^ (C -^ B1)) by ORDINAL3:30 ;

then A8: B +^ (C -^ B1) in dom psi by A2, A6, ORDINAL3:22;

B c= B +^ (C -^ B1) by ORDINAL3:24;

then psi . (B +^ (C -^ B1)) = {} by A2, A4, A6, A7, ORDINAL3:22;

hence (fi ^ psi) . C = 0 by A7, A8, Def1; :: 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 ^ psi) & ( for b_{4} being set holds

( not b_{3} c= b_{4} or not b_{4} in dom (fi ^ psi) or ( b_{1} in (fi ^ psi) . b_{4} & (fi ^ psi) . 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 ^ psi) & ( for b_{2} being set holds

( not b_{1} c= b_{2} or not b_{2} in dom (fi ^ psi) or ( B in (fi ^ psi) . b_{2} & (fi ^ psi) . b_{2} in C ) ) ) ) )

assume that

A9: B in A and

A10: A in C ; :: thesis: ex b_{1} being set st

( b_{1} in dom (fi ^ psi) & ( for b_{2} being set holds

( not b_{1} c= b_{2} or not b_{2} in dom (fi ^ psi) or ( B in (fi ^ psi) . b_{2} & (fi ^ psi) . b_{2} in C ) ) ) )

consider D being Ordinal such that

A11: D in dom psi and

A12: for E being Ordinal st D c= E & E in dom psi holds

( B in psi . E & psi . E in C ) by A1, A9, A10;

take D1 = (dom fi) +^ D; :: thesis: ( D1 in dom (fi ^ psi) & ( for b_{1} being set holds

( not D1 c= b_{1} or not b_{1} in dom (fi ^ psi) or ( B in (fi ^ psi) . b_{1} & (fi ^ psi) . b_{1} in C ) ) ) )

thus D1 in dom (fi ^ psi) by A2, A11, ORDINAL2:32; :: thesis: for b_{1} being set holds

( not D1 c= b_{1} or not b_{1} in dom (fi ^ psi) or ( B in (fi ^ psi) . b_{1} & (fi ^ psi) . b_{1} in C ) )

let E be Ordinal; :: thesis: ( not D1 c= E or not E in dom (fi ^ psi) or ( B in (fi ^ psi) . E & (fi ^ psi) . E in C ) )

assume that

A13: D1 c= E and

A14: E in dom (fi ^ psi) ; :: thesis: ( B in (fi ^ psi) . E & (fi ^ psi) . E in C )

A15: D c= D +^ (E -^ D1) by ORDINAL3:24;

A16: E = D1 +^ (E -^ D1) by A13, ORDINAL3:def 5

.= (dom fi) +^ (D +^ (E -^ D1)) by ORDINAL3:30 ;

then A17: D +^ (E -^ D1) in dom psi by A2, A14, ORDINAL3:22;

then (fi ^ psi) . E = psi . (D +^ (E -^ D1)) by A16, Def1;

hence ( B in (fi ^ psi) . E & (fi ^ psi) . E in C ) by A12, A15, A17; :: thesis: verum

end;( b

( not b

assume that

A9: B in A and

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

( b

( not b

consider D being Ordinal such that

A11: D in dom psi and

A12: for E being Ordinal st D c= E & E in dom psi holds

( B in psi . E & psi . E in C ) by A1, A9, A10;

take D1 = (dom fi) +^ D; :: thesis: ( D1 in dom (fi ^ psi) & ( for b

( not D1 c= b

thus D1 in dom (fi ^ psi) by A2, A11, ORDINAL2:32; :: thesis: for b

( not D1 c= b

let E be Ordinal; :: thesis: ( not D1 c= E or not E in dom (fi ^ psi) or ( B in (fi ^ psi) . E & (fi ^ psi) . E in C ) )

assume that

A13: D1 c= E and

A14: E in dom (fi ^ psi) ; :: thesis: ( B in (fi ^ psi) . E & (fi ^ psi) . E in C )

A15: D c= D +^ (E -^ D1) by ORDINAL3:24;

A16: E = D1 +^ (E -^ D1) by A13, ORDINAL3:def 5

.= (dom fi) +^ (D +^ (E -^ D1)) by ORDINAL3:30 ;

then A17: D +^ (E -^ D1) in dom psi by A2, A14, ORDINAL3:22;

then (fi ^ psi) . E = psi . (D +^ (E -^ D1)) by A16, Def1;

hence ( B in (fi ^ psi) . E & (fi ^ psi) . E in C ) by A12, A15, A17; :: thesis: verum