theorem Th7: :: SRINGS_5:8

for n being Nat holds product ((Seg n) --> REAL) = REAL n