let a1, a2, a3, a4, a5, a6, a7, a8, a9, a10 be object ; :: thesis: rng <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> = {a1,a2,a3,a4,a5,a6,a7,a8,a9,a10}
thus rng <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> = (rng <*a1,a2,a3,a4,a5,a6,a7,a8,a9*>) \/ (rng <*a10*>) by FINSEQ_1:31
.= {a1,a2,a3,a4,a5,a6,a7,a8,a9} \/ (rng <*a10*>) by Th2
.= {a1,a2,a3,a4,a5,a6,a7,a8,a9} \/ {a10} by FINSEQ_1:38
.= {a1,a2,a3,a4,a5,a6,a7,a8,a9,a10} by ENUMSET1:85 ; :: thesis: verum