:: deftheorem defines ProductREAL SRINGS_5:def 1 :
for n being Nat holds ProductREAL n = (Seg n) --> REAL;