let fi, psi be Ordinal-Sequence; :: thesis: for C being Ordinal st dom fi = dom psi & C <> {} & sup fi is limit_ordinal & ( for A, B being Ordinal st A in dom fi & B = fi . A holds
psi . A = B *^ C ) holds
sup psi = (sup fi) *^ C
let C be Ordinal; :: thesis: ( dom fi = dom psi & C <> {} & sup fi is limit_ordinal & ( for A, B being Ordinal st A in dom fi & B = fi . A holds
psi . A = B *^ C ) implies sup psi = (sup fi) *^ C )
assume that
A1:
dom fi = dom psi
and
A2:
C <> {}
and
A3:
sup fi is limit_ordinal
and
A4:
for A, B being Ordinal st A in dom fi & B = fi . A holds
psi . A = B *^ C
; :: thesis: sup psi = (sup fi) *^ C
A5:
(sup (rng fi)) *^ C c= sup (rng psi)
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in (sup (rng fi)) *^ C or x in sup (rng psi) )
assume A6:
x in (sup (rng fi)) *^ C
;
:: thesis: x in sup (rng psi)
then reconsider A =
x as
Ordinal ;
consider B being
Ordinal such that A7:
B in sup (rng fi)
and A8:
A in B *^ C
by A3, A6, Th49;
consider D being
Ordinal such that A9:
D in rng fi
and A10:
B c= D
by A7, ORDINAL2:29;
consider y being
set such that A11:
y in dom fi
and A12:
D = fi . y
by A9, FUNCT_1:def 5;
reconsider y =
y as
Ordinal by A11;
reconsider y' =
psi . y as
Ordinal ;
A13:
y' in rng psi
by A1, A11, FUNCT_1:def 5;
y' = D *^ C
by A4, A11, A12;
then A14:
D *^ C in sup (rng psi)
by A13, ORDINAL2:27;
B *^ C c= D *^ C
by A10, ORDINAL2:58;
hence
x in sup (rng psi)
by A8, A14, ORDINAL1:19;
:: thesis: verum
end;
sup (rng psi) c= (sup (rng fi)) *^ C
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in sup (rng psi) or x in (sup (rng fi)) *^ C )
assume A15:
x in sup (rng psi)
;
:: thesis: x in (sup (rng fi)) *^ C
then reconsider A =
x as
Ordinal ;
consider B being
Ordinal such that A16:
B in rng psi
and A17:
A c= B
by A15, ORDINAL2:29;
consider y being
set such that A18:
y in dom psi
and A19:
B = psi . y
by A16, FUNCT_1:def 5;
reconsider y =
y as
Ordinal by A18;
reconsider y' =
fi . y as
Ordinal ;
y' in rng fi
by A1, A18, FUNCT_1:def 5;
then A20:
y' in sup (rng fi)
by ORDINAL2:27;
B = y' *^ C
by A1, A4, A18, A19;
then
B in (sup (rng fi)) *^ C
by A2, A20, ORDINAL2:57;
hence
x in (sup (rng fi)) *^ C
by A17, ORDINAL1:22;
:: thesis: verum
end;
hence
sup psi = (sup fi) *^ C
by A5, XBOOLE_0:def 10; :: thesis: verum