theorem :: SETWISEO:59

for X being non empty set
for Y, Z being set
for f being Function of X,(Fin Y)
for g being Function of (Fin Y),(Fin Z) st g . ({}. Y) = {}. Z & ( for x, y being Element of Fin Y holds g . (x \/ y) = (g . x) \/ (g . y) ) holds
for B being Element of Fin X holds g . (FinUnion (B,f)) = FinUnion (B,(g * f))