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