let W be Universe; :: thesis: for a being Ordinal of W
for L being DOMAIN-Sequence of holds L . a c= Union L
let a be Ordinal of W; :: thesis: for L being DOMAIN-Sequence of holds L . a c= Union L
let L be DOMAIN-Sequence of ; :: thesis: L . a c= Union L
a in dom L by Th23;
then ( L . a in rng L & union (rng L) = Union L ) by CARD_3:def 4, FUNCT_1:def 5;
hence L . a c= Union L by ZFMISC_1:92; :: thesis: verum