theorem Th9: :: SIN_COS:9

( 0c ExpSeq is absolutely_summable & Sum (0c ExpSeq) = 1r )