let fi, psi be Ordinal-Sequence; 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; ( 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
; sup psi = (sup fi) *^ C
A5:
(sup (rng fi)) *^ C c= sup (rng psi)
proof
let x be
object ;
TARSKI:def 3 ( not x in (sup (rng fi)) *^ C or x in sup (rng psi) )
assume A6:
x in (sup (rng fi)) *^ C
;
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, Th41;
consider D being
Ordinal such that A9:
D in rng fi
and A10:
B c= D
by A7, ORDINAL2:21;
consider y being
object such that A11:
y in dom fi
and A12:
D = fi . y
by A9, FUNCT_1:def 3;
reconsider y =
y as
Ordinal by A11;
reconsider y9 =
psi . y as
Ordinal ;
A13:
y9 in rng psi
by A1, A11, FUNCT_1:def 3;
y9 = D *^ C
by A4, A11, A12;
then A14:
D *^ C in sup (rng psi)
by A13, ORDINAL2:19;
B *^ C c= D *^ C
by A10, ORDINAL2:41;
hence
x in sup (rng psi)
by A8, A14, ORDINAL1:10;
verum
end;
sup (rng psi) c= (sup (rng fi)) *^ C
proof
let x be
object ;
TARSKI:def 3 ( not x in sup (rng psi) or x in (sup (rng fi)) *^ C )
assume A15:
x in sup (rng psi)
;
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:21;
consider y being
object such that A18:
y in dom psi
and A19:
B = psi . y
by A16, FUNCT_1:def 3;
reconsider y =
y as
Ordinal by A18;
reconsider y9 =
fi . y as
Ordinal ;
y9 in rng fi
by A1, A18, FUNCT_1:def 3;
then A20:
y9 in sup (rng fi)
by ORDINAL2:19;
B = y9 *^ C
by A1, A4, A18, A19;
then
B in (sup (rng fi)) *^ C
by A2, A20, ORDINAL2:40;
hence
x in (sup (rng fi)) *^ C
by A17, ORDINAL1:12;
verum
end;
hence
sup psi = (sup fi) *^ C
by A5; verum