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:31
.= {x} \/ (rng <*y*>) by FINSEQ_1:38
.= {x} \/ {y} by FINSEQ_1:38
.= {x,y} by ENUMSET1:1 ;
:: thesis: verum