theorem :: CLASSES4:5

for X being FamUnion-closed set
for f being Function st dom f in X & rng f c= X holds
union (rng f) in X by CLASSES3:def 3;