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