theorem :: SRINGS_5:7

for n being Nat holds ProductREAL n = (Seg n) --> the carrier of R^1 ;