theorem :: FUNCT_3:28

for A being set
for f being Function st A c= bool (dom f) & f is one-to-one holds
union ((" f) " A) = f .: (union A)