theorem :: SEQ_1:42

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