let S be non empty finite set ; :: thesis: Union (canFS S) = union S
now :: thesis: for x being object st x in union S holds
x in union (rng (canFS S))
let x be object ; :: thesis: ( x in union S implies x in union (rng (canFS S)) )
assume x in union S ; :: thesis: x in union (rng (canFS S))
then consider A being set such that
A2: ( x in A & A in S ) by TARSKI:def 4;
A in rng (canFS S) by A2, DIST_2:3;
hence x in union (rng (canFS S)) by A2, TARSKI:def 4; :: thesis: verum
end;
then union S c= union (rng (canFS S)) ;
hence Union (canFS S) = union S by ZFMISC_1:77; :: thesis: verum