theorem XPF: :: RVSUM_4:57

for f being complex-valued XFinSequence holds Product (XFS2FS f) = XProduct f