theorem Th23: :: CARD_FIN:24

for F, Ch being Function
for y being object st F | (Ch " {y}) = (Ch " {y}) --> (union (rng F)) holds
Intersection (F,Ch,y) = union (rng F)