theorem Th27: :: FUNCT_3:27

for A being set
for f being Function holds union ((" f) " A) c= f .: (union A)