for n being Nat
for f being complex-valued XFinSequence st n in dom f holds
(XProduct (f | n)) * (f . n) = XProduct (f | (n + 1))