let L be T-Sequence; :: thesis: ( dom L is limit_ordinal & ( for A being Ordinal st A in dom L holds
L . A = Rank A ) implies Rank (dom L) = Union L )
assume that
A1: dom L is limit_ordinal and
A2: for A being Ordinal st A in dom L holds
L . A = Rank A ; :: thesis: Rank (dom L) = Union L
A3: union (rng L) = Union L by CARD_3:def 4;

now

assume A4: dom L <> {} ; :: thesis: ( Rank (dom L) c= Union L & Union L c= Rank (dom L) )
thus Rank (dom L) c= Union L :: thesis: Union L c= Rank (dom L)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Rank (dom L) or x in Union L )
assume x in Rank (dom L) ; :: thesis: x in Union L
then consider A being Ordinal such that
A5: ( A in dom L & x in Rank A ) by A1, A4, CLASSES1:35;
L . A = Rank A by A2, A5;
then Rank A in rng L by A5, FUNCT_1:def 5;
hence x in Union L by A3, A5, TARSKI:def 4; :: thesis: verum

end;

thus Union L c= Rank (dom L) :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Union L or x in Rank (dom L) )
assume x in Union L ; :: thesis: x in Rank (dom L)
then consider X being set such that
A6: ( x in X & X in rng L ) by A3, TARSKI:def 4;
consider y being set such that
A7: ( y in dom L & X = L . y ) by A6, FUNCT_1:def 5;
reconsider y = y as Ordinal by A7;
X = Rank y by A2, A7;
hence x in Rank (dom L) by A1, A6, A7, CLASSES1:35; :: thesis: verum

end;

end;

hence Rank (dom L) = Union L by A3, CLASSES1:33, RELAT_1:65, XBOOLE_0:def 10, ZFMISC_1:2; :: thesis: verum