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