theorem :: SRINGS_5:9

for n being Nat holds product (ProductREAL n) = REAL n by Th7;