:: deftheorem defines RAT SRINGS_5:def 2 :
for n being Nat holds RAT n = n -tuples_on RAT;