theorem :: SETWISEO:51

for X, Y being non empty set
for A being set
for B being Element of Fin X
for f being Function of X,Y
for g being Function of Y,(Fin A) holds FinUnion ((f .: B),g) = FinUnion (B,(g * f))