theorem Th48: :: CATALAN2:48

for seq1, seq2 being Real_Sequence
for n being Nat ex Fr being XFinSequence of REAL st
( (Partial_Sums (seq1 (##) seq2)) . n = Sum Fr & dom Fr = n + 1 & ( for i being Nat st i in n + 1 holds
Fr . i = (seq1 . i) * ((Partial_Sums seq2) . (n -' i)) ) )