:: deftheorem defines _th_unit_vector VECTSP13:def 8 :
for R being Ring
for n, i being Nat holds i _th_unit_vector (n,R) = Replace ((n |-> (0. R)),i,(1. R));