let x1, x2, x3 be set ; :: thesis: rng <*x1,x2,x3*> = {x1,x2,x3}
thus rng <*x1,x2,x3*> = rng (<*x1*> ^ <*x2,x3*>) by FINSEQ_1:60
.= (rng <*x1*>) \/ (rng <*x2,x3*>) by FINSEQ_1:44
.= {x1} \/ (rng <*x2,x3*>) by FINSEQ_1:55
.= {x1} \/ {x2,x3} by Lm1
.= {x1,x2,x3} by ENUMSET1:42 ; :: thesis: verum