:: deftheorem defines FinUnion SETWISEO:def 5 :
for X being non empty set
for A being set
for B being Element of Fin X
for f being Function of X,(Fin A) holds FinUnion (B,f) = (FinUnion A) $$ (B,f);