theorem :: CARD_FIN:23

for y being set
for F, Ch being Function st ( F is empty or union (rng F) is empty ) holds
Intersection (F,Ch,y) = union (rng F) by RELAT_1:38, ZFMISC_1:2;