for r being Real
for seq being Real_Sequence holds abs (r (#) seq) = |.r.| (#) (abs seq)