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