theorem Th13: :: FUNCT_3:13

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