theorem :: SEQ_1:50

for seq, seq1, seq9, seq19 being Real_Sequence st seq is non-zero & seq9 is non-zero holds
( (seq1 /" seq) + (seq19 /" seq9) = ((seq1 (#) seq9) + (seq19 (#) seq)) /" (seq (#) seq9) & (seq1 /" seq) - (seq19 /" seq9) = ((seq1 (#) seq9) - (seq19 (#) seq)) /" (seq (#) seq9) )