let fi, psi be Ordinal-Sequence; :: thesis: for C being Ordinal st {} <> dom fi & dom fi = dom psi & ( for A, B being Ordinal st A in dom fi & B = fi . A holds
psi . A = C +^ B ) holds
sup psi = C +^ (sup fi)
let C be Ordinal; :: thesis: ( {} <> dom fi & dom fi = dom psi & ( for A, B being Ordinal st A in dom fi & B = fi . A holds
psi . A = C +^ B ) implies sup psi = C +^ (sup fi) )
assume that
A1: {} <> dom fi and
A2: dom fi = dom psi and
A3: for A, B being Ordinal st A in dom fi & B = fi . A holds
psi . A = C +^ B ; :: thesis: sup psi = C +^ (sup fi)
A4: sup (rng psi) c= C +^ (sup (rng fi))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in sup (rng psi) or x in C +^ (sup (rng fi)) )
assume A5: x in sup (rng psi) ; :: thesis: x in C +^ (sup (rng fi))
then reconsider A = x as Ordinal ;
consider B being Ordinal such that
A6: ( B in rng psi & A c= B ) by A5, ORDINAL2:29;
consider y being set such that
A7: ( y in dom psi & B = psi . y ) by A6, FUNCT_1:def 5;
reconsider y = y as Ordinal by A7;
reconsider y' = fi . y as Ordinal ;
A8: ( B = C +^ y' & y' in rng fi ) by A2, A3, A7, FUNCT_1:def 5;
then y' in sup (rng fi) by ORDINAL2:27;
then B in C +^ (sup (rng fi)) by A8, ORDINAL2:49;
hence x in C +^ (sup (rng fi)) by A6, ORDINAL1:22; :: thesis: verum

end;

consider z being Element of dom fi;
reconsider z' = fi . z as Ordinal ;
C +^ (sup (rng fi)) c= sup (rng psi)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in C +^ (sup (rng fi)) or x in sup (rng psi) )
assume A9: x in C +^ (sup (rng fi)) ; :: thesis: x in sup (rng psi)
then reconsider A = x as Ordinal ;

A10: now

assume A11: A in C ; :: thesis: A in sup (rng psi)
( C c= C +^ z' & C +^ z' = psi . z ) by A1, A3, Th27;
then A12: ( C +^ z' in rng psi & A c= C +^ z' ) by A1, A2, A11, FUNCT_1:def 5, ORDINAL1:def 2;
then C +^ z' in sup (rng psi) by ORDINAL2:27;
hence A in sup (rng psi) by A12, ORDINAL1:22; :: thesis: verum

end;

now

given B being Ordinal such that A13: ( B in sup (rng fi) & A = C +^ B ) ; :: thesis: A in sup (rng psi)
consider D being Ordinal such that
A14: ( D in rng fi & B c= D ) by A13, ORDINAL2:29;
consider x being set such that
A15: ( x in dom fi & D = fi . x ) by A14, FUNCT_1:def 5;
reconsider x = x as Ordinal by A15;
psi . x = C +^ D by A3, A15;
then A16: ( C +^ D in rng psi & A c= C +^ D ) by A2, A13, A14, A15, FUNCT_1:def 5, ORDINAL2:50;
then C +^ D in sup (rng psi) by ORDINAL2:27;
hence A in sup (rng psi) by A16, ORDINAL1:22; :: thesis: verum

end;

hence x in sup (rng psi) by A9, A10, Th42; :: thesis: verum

end;

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