let X be non empty set ; :: thesis: for B being Element of Fin X holds FinUnion B,(singleton X) = B
let B be Element of Fin X; :: thesis: FinUnion B,(singleton X) = B

now

let x be set ; :: thesis: ( ( x in FinUnion B,(singleton X) implies x in B ) & ( x in B implies x in FinUnion B,(singleton X) ) )
thus ( x in FinUnion B,(singleton X) implies x in B ) :: thesis: ( x in B implies x in FinUnion B,(singleton X) )

proof

assume x in FinUnion B,(singleton X) ; :: thesis: x in B
then ex i being Element of X st
( i in B & x in (singleton X) . i ) by Th70;
hence x in B by Th68; :: thesis: verum

end;

assume A1: x in B ; :: thesis: x in FinUnion B,(singleton X)
then reconsider x9 = x as Element of X by Th14;
x in (singleton X) . x9 by Th68;
hence x in FinUnion B,(singleton X) by A1, Th70; :: thesis: verum

end;

hence FinUnion B,(singleton X) = B by TARSKI:2; :: thesis: verum