theorem :: CARD_FIN:25

for y being set
for F, Ch being Function st not union (rng F) is empty & Intersection (F,Ch,y) = union (rng F) holds
F | (Ch " {y}) = (Ch " {y}) --> (union (rng F))