{} c= Seg 0 ;
hence Sgm {} = {} by FINSEQ_1:72; :: thesis: verum