for r being Complex
for seq being Complex_Sequence st r <> 0c & seq is non-zero holds
r (#) seq is non-zero