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