theorem :: RVSUM_4:55

for n being Nat
for f1, f2 being b₁ -element complex-valued XFinSequence holds XProduct (f1 (#) f2) = (XProduct f1) * (XProduct f2)