theorem :: SEQ_1:25

for r being Real
for seq, seq1 being Real_Sequence holds r (#) (seq1 /" seq) = (r (#) seq1) /" seq