theorem :: SETWISEO:58

for X being non empty set
for B being Element of Fin X holds FinUnion (B,(singleton X)) = B