theorem Th1: :: RANDOM_3:1

for B being non empty set
for f being Function holds f " (union B) = union { (f " Y) where Y is Element of B : verum }