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