theorem Th45: :: SETWISEO:48

for X being non empty set
for A being set
for f being Function of X,(Fin A)
for i being Element of X
for B being Element of Fin X holds FinUnion ((B \/ {.i.}),f) = (FinUnion (B,f)) \/ (f . i)