for n being Nat
for f being Complex_Sequence holds (XProduct (f | n)) * (f . n) = XProduct (f | (n + 1))