for seq, seq1 being Real_Sequence holds
( ( seq is non-zero & seq1 is non-zero ) iff seq (#) seq1 is non-zero )