for X being non empty set
for A being set
for f being Function of X,(Fin A)
for B being Element of Fin X
for x being set holds
( x in FinUnion (B,f) iff ex i being Element of X st
( i in B & x in f . i ) )