theorem Th61: :: MESFUN18:61

for n being non zero Nat holds
( REAL-NS n = product ((Seg n) --> RNS_Real) & REAL n = the carrier of (product ((Seg n) --> RNS_Real)) & REAL n = product ((Seg n) --> REAL) )