theorem Th47: :: CATALAN2:47

for seq1, seq2 being Real_Sequence holds (seq1 (##) seq2) . 0 = (seq1 . 0) * (seq2 . 0)