theorem :: CATALAN2:46

for seq1, seq2, seq3 being Real_Sequence holds seq1 (##) (seq2 + seq3) = (seq1 (##) seq2) + (seq1 (##) seq3)