for r being Real
for seq being Real_Sequence st r <> 0 & seq is non-zero holds
r (#) seq is non-zero