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:1; :: thesis: verum