Sum <*1*> = 1 ;
hence Sum (Sgm {1}) = 1 by FINSEQ_3:44; :: thesis: verum