let fi, psi be Ordinal-Sequence; :: thesis: for C being Ordinal st {} <> dom fi & 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 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
{} <> dom fi and
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 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 A6: x in sup (rng psi) ; :: thesis: x in (sup (rng fi)) *^ C
then reconsider A = x as Ordinal ;
consider B being Ordinal such that
A7: ( B in rng psi & A c= B ) by A6, ORDINAL2:29;
consider y being set such that
A8: ( y in dom psi & B = psi . y ) by A7, FUNCT_1:def 5;
reconsider y = y as Ordinal by A8;
reconsider y' = fi . y as Ordinal ;
A9: ( B = y' *^ C & y' in rng fi ) by A1, A4, A8, FUNCT_1:def 5;
then y' in sup (rng fi) by ORDINAL2:27;
then B in (sup (rng fi)) *^ C by A2, A9, ORDINAL2:57;
hence x in (sup (rng fi)) *^ C by A7, ORDINAL1:22; :: thesis: verum

end;

(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 A10: x in (sup (rng fi)) *^ C ; :: thesis: x in sup (rng psi)
then reconsider A = x as Ordinal ;
consider B being Ordinal such that
A11: ( B in sup (rng fi) & A in B *^ C ) by A3, A10, Th49;
consider D being Ordinal such that
A12: ( D in rng fi & B c= D ) by A11, ORDINAL2:29;
consider y being set such that
A13: ( y in dom fi & D = fi . y ) by A12, FUNCT_1:def 5;
reconsider y = y as Ordinal by A13;
reconsider y' = psi . y as Ordinal ;
( y' in rng psi & y' = D *^ C ) by A1, A4, A13, FUNCT_1:def 5;
then ( D *^ C in sup (rng psi) & B *^ C c= D *^ C ) by A12, ORDINAL2:27, ORDINAL2:58;
hence x in sup (rng psi) by A11, ORDINAL1:19; :: thesis: verum

end;

hence sup psi = (sup fi) *^ C by A5, XBOOLE_0:def 10; :: thesis: verum