theorem :: SETWISEO:50

for X being non empty set
for A being set
for f being Function of X,(Fin A)
for B1, B2 being Element of Fin X holds FinUnion ((B1 \/ B2),f) = (FinUnion (B1,f)) \/ (FinUnion (B2,f))