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