theorem PFO: :: RVSUM_4:51

for f being empty XFinSequence holds XProduct f = 1