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