:: deftheorem defines RN_Base EUCLID_7:def 13 :
for n being Nat holds RN_Base n = { (Base_FinSeq (n,i)) where i is Element of NAT : ( 1 <= i & i <= n ) } ;