let fi, psi be Ordinal-Sequence; for A being Ordinal st A is_limes_of psi holds
A is_limes_of fi ^ psi
let A be Ordinal; ( 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 ) ) ) ) ) )
; ORDINAL2:def 9 A is_limes_of fi ^ psi
A2:
dom (fi ^ psi) = (dom fi) +^ (dom psi)
by Def1;
per cases
( A = 0 or A <> 0 )
;
ORDINAL2:def 9case
A = 0
;
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 = 0 ) ) )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;
( 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 = 0 ) ) )thus
B1 in dom (fi ^ psi)
by A2, A3, ORDINAL2:32;
for b1 being set holds
( not B1 c= b1 or not b1 in dom (fi ^ psi) or (fi ^ psi) . b1 = 0 )let C be
Ordinal;
( 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)
;
(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;
verum end; case
A <> 0
;
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;
( 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 that A9:
B in A
and A10:
A in C
;
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 ) ) ) )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;
( 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, A11, ORDINAL2:32;
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;
( 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)
;
( 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;
verum end; end;