theorem :: COMSEQ_2:3

for s being Complex_Sequence st s is non-zero holds
s *' is non-zero