theorem :: SEQ_1:56

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