for seq being Real_Sequence
for Ns being V43() sequence of NAT holds
( (- seq) * Ns = - (seq * Ns) & (abs seq) * Ns = abs (seq * Ns) )