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 :: thesis: for x being object holds
( ( x in FinUnion (B,(singleton X)) implies x in B ) & ( x in B implies x in FinUnion (B,(singleton X)) ) )

let x be object ; :: 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 Th54;
hence x in B by Th52; :: thesis: verum

end;

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

end;

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