theorem ConstantProduct: :: RVSUM_3:8

for f being constant non empty real-valued FinSequence holds Product f = (the_value_of f) |^ (len f)