let a1, a2, a3, a4, a5, a6, a7 be object ; rng <*a1,a2,a3,a4,a5,a6,a7*> = {a1,a2,a3,a4,a5,a6,a7}
thus rng <*a1,a2,a3,a4,a5,a6,a7*> =
(rng <*a1,a2,a3,a4,a5*>) \/ (rng <*a6,a7*>)
by FINSEQ_1:31
.=
{a1,a2,a3,a4,a5} \/ (rng <*a6,a7*>)
by CIRCCMB3:14
.=
{a1,a2,a3,a4,a5} \/ {a6,a7}
by FINSEQ_2:127
.=
{a1,a2,a3,a4,a5,a6,a7}
by ENUMSET1:20
; verum