let x, y, z be set ; :: thesis: rng <*x,y,z*> = {x,y,z}
<*x,y,z*> = <*x,y*> ^ <*z*> by FINSEQ_1:60;
hence rng <*x,y,z*> = (rng <*x,y*>) \/ (rng <*z*>) by FINSEQ_1:44
.= {x,y} \/ (rng <*z*>) by Lm1
.= {x,y} \/ {z} by FINSEQ_1:55
.= {x,y,z} by ENUMSET1:43 ;
:: thesis: verum