let x, y be set ; :: thesis: rng <*x,y*> = {x,y}
thus rng <*x,y*> = (rng <*x*>) \/ (rng <*y*>) by FINSEQ_1:31
.= {x} \/ (rng <*y*>) by FINSEQ_1:38
.= {x} \/ {y} by FINSEQ_1:38
.= {x,y} by ENUMSET1:1 ; :: thesis: verum