:: deftheorem Def4 defines (##) CATALAN2:def 4 :
for seq1, seq2, b₃ being Real_Sequence holds
( b₃ = seq1 (##) seq2 iff for k being Nat ex Fr being XFinSequence of REAL st
( dom Fr = k + 1 & ( for n being Nat st n in k + 1 holds
Fr . n = (seq1 . n) * (seq2 . (k -' n)) ) & Sum Fr = b₃ . k ) );