theorem u1: :: VECTSP13:23

for R being Ring
for n, i being Nat st 1 <= i & i <= n holds
( (i _th_unit_vector (n,R)) . i = 1. R & ( for j being Nat st 1 <= j & j <= n & j <> i holds
(i _th_unit_vector (n,R)) . j = 0. R ) )