:: deftheorem defines Base VECTSP13:def 9 :
for R being Ring
for n being Nat holds Base (R,n) = { (i _th_unit_vector (n,R)) where i is Nat : ( 1 <= i & i <= n ) } ;