thus Seg 7 = {1,2,3,4,5,6} \/ {(6 + 1)} by Th4, FINSEQ_1:9
.= {1,2,3,4,5,6,7} by ENUMSET1:21 ; :: thesis: verum