:: deftheorem defines REAL EUCLID:def 1 :
for n being Nat holds REAL n = n -tuples_on REAL;