let x1, x2 be object ; :: thesis: rng <*x1,x2*> = {x1,x2}
thus rng <*x1,x2*> = (rng <*x1*>) \/ (rng <*x2*>) by FINSEQ_1:31
.= (rng <*x1*>) \/ {x2} by FINSEQ_1:38
.= {x1} \/ {x2} by FINSEQ_1:39
.= {x1,x2} by ENUMSET1:1 ; :: thesis: verum