theorem Th16: :: FUNCT_3:16

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