let fi be Ordinal-Sequence; :: thesis: for W being Universe st dom fi in W & rng fi c= W holds
sup fi in W
let W be Universe; :: thesis: ( dom fi in W & rng fi c= W implies sup fi in W )
assume A1: ( dom fi in W & rng fi c= W ) ; :: thesis: sup fi in W
( rng fi = fi .: (dom fi) & W is Tarski ) by RELAT_1:146;
then ( card (rng fi) c= card (dom fi) & card (dom fi) in card W ) by A1, CARD_2:3, CLASSES2:1;
then card (rng fi) in card W by ORDINAL1:22;
then rng fi in W by A1, CLASSES1:2;
then A2: union (rng fi) in W by CLASSES2:65;
consider A being Ordinal such that
A3: rng fi c= A by ORDINAL2:def 8;
for x being set st x in rng fi holds
x is Ordinal by A3;
then reconsider B = union (rng fi) as Ordinal by ORDINAL1:35;
A4: succ B in W by A2, CLASSES2:6;
sup fi c= succ B

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in sup fi or x in succ B )
assume A5: x in sup fi ; :: thesis: x in succ B
then reconsider A = x as Ordinal ;
consider C being Ordinal such that
A6: ( C in rng fi & A c= C ) by A5, ORDINAL2:29;
C c= union (rng fi) by A6, ZFMISC_1:92;
then A c= B by A6, XBOOLE_1:1;
hence x in succ B by ORDINAL1:34; :: thesis: verum

end;

hence sup fi in W by A4, CLASSES1:def 1; :: thesis: verum