theorem u2: :: VECTSP13:24

for R being non degenerated Ring
for n, i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n holds
( i _th_unit_vector (n,R) = j _th_unit_vector (n,R) iff i = j )