let x, y, z be set ; :: thesis: rng <*x,y,z*> = {x,y,z}
thus rng <*x,y,z*> = (rng <*x,y*>) \/ (rng <*z*>) by FINSEQ_1:31
.= {x,y} \/ (rng <*z*>) by Lm1
.= {x,y} \/ {z} by FINSEQ_1:38
.= {x,y,z} by ENUMSET1:3 ; :: thesis: verum