let x, y be set ; :: thesis: rng <*x,y*> = {x,y}
<*x,y*> = <*x*> ^ <*y*> by FINSEQ_1:def 9;
hence rng <*x,y*> = (rng <*x*>) \/ (rng <*y*>) by FINSEQ_1:44
.= {x} \/ (rng <*y*>) by FINSEQ_1:55
.= {x} \/ {y} by FINSEQ_1:55
.= {x,y} by ENUMSET1:41 ;
:: thesis: verum