theorem :: RVSUM_4:55
for n being Nat
for f1, f2 being b1 -element complex-valued XFinSequence holds XProduct (f1 (#) f2) = (XProduct f1) * (XProduct f2)