let x1, x2, x3 be object ; 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
; verum