let psi, fi 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 = {} & ex B being Ordinal st
( B in dom psi & ( for C being Ordinal st B c= C & C in dom psi holds
psi . C = {} ) ) ) or ( A <> {} & ( 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 13 :: thesis: A is_limes_of fi ^ psi
A2: dom (fi ^ psi) = (dom fi) +^ (dom psi) by Def1;
per cases ( A = {} or A <> {} ) ;
:: according to ORDINAL2:def 13
case A = {} ; :: thesis: ex b1 being set st
( b1 in dom (fi ^ psi) & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom (fi ^ psi) or (fi ^ psi) . b2 = {} ) ) )
then consider B being Ordinal such that
A3: ( B in dom psi & ( 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 b1 being set holds
( not B1 c= b1 or not b1 in dom (fi ^ psi) or (fi ^ psi) . b1 = {} ) ) )
thus B1 in dom (fi ^ psi) by A2, A3, ORDINAL2:49; :: thesis: for b1 being set holds
( not B1 c= b1 or not b1 in dom (fi ^ psi) or (fi ^ psi) . b1 = {} )
let C be Ordinal; :: thesis: ( not B1 c= C or not C in dom (fi ^ psi) or (fi ^ psi) . C = {} )
assume A4: ( B1 c= C & C in dom (fi ^ psi) ) ; :: thesis: (fi ^ psi) . C = {}
then A5: C = B1 +^ (C -^ B1) by ORDINAL3:def 6
.= (dom fi) +^ (B +^ (C -^ B1)) by ORDINAL3:33 ;
then ( B c= B +^ (C -^ B1) & B +^ (C -^ B1) in dom psi ) by A2, A4, ORDINAL3:25, ORDINAL3:27;
then ( (fi ^ psi) . C = psi . (B +^ (C -^ B1)) & psi . (B +^ (C -^ B1)) = {} ) by A3, A5, Def1;
hence (fi ^ psi) . C = {} ; :: thesis: verum
end;
case A <> {} ; :: 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 ^ psi) & ( for b4 being set holds
( not b3 c= b4 or not b4 in dom (fi ^ psi) or ( b1 in (fi ^ psi) . b4 & (fi ^ psi) . 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 ^ psi) & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom (fi ^ psi) or ( B in (fi ^ psi) . b2 & (fi ^ psi) . b2 in C ) ) ) ) )
assume ( B in A & A in C ) ; :: thesis: ex b1 being set st
( b1 in dom (fi ^ psi) & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom (fi ^ psi) or ( B in (fi ^ psi) . b2 & (fi ^ psi) . b2 in C ) ) ) )
then consider D being Ordinal such that
A6: D in dom psi and
A7: for E being Ordinal st D c= E & E in dom psi holds
( B in psi . E & psi . E in C ) by A1;
take D1 = (dom fi) +^ D; :: thesis: ( D1 in dom (fi ^ psi) & ( for b1 being set holds
( not D1 c= b1 or not b1 in dom (fi ^ psi) or ( B in (fi ^ psi) . b1 & (fi ^ psi) . b1 in C ) ) ) )
thus D1 in dom (fi ^ psi) by A2, A6, ORDINAL2:49; :: thesis: for b1 being set holds
( not D1 c= b1 or not b1 in dom (fi ^ psi) or ( B in (fi ^ psi) . b1 & (fi ^ psi) . b1 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 A8: ( D1 c= E & E in dom (fi ^ psi) ) ; :: thesis: ( B in (fi ^ psi) . E & (fi ^ psi) . E in C )
then A9: E = D1 +^ (E -^ D1) by ORDINAL3:def 6
.= (dom fi) +^ (D +^ (E -^ D1)) by ORDINAL3:33 ;
then ( D c= D +^ (E -^ D1) & D +^ (E -^ D1) in dom psi ) by A2, A8, ORDINAL3:25, ORDINAL3:27;
then ( (fi ^ psi) . E = psi . (D +^ (E -^ D1)) & B in psi . (D +^ (E -^ D1)) & psi . (D +^ (E -^ D1)) in C ) by A7, A9, Def1;
hence ( B in (fi ^ psi) . E & (fi ^ psi) . E in C ) ; :: thesis: verum
end;
end;