let R be non degenerated Ring; :: thesis: 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 )
let n, i, j be Nat; :: thesis: ( 1 <= i & i <= n & 1 <= j & j <= n implies ( i _th_unit_vector (n,R) = j _th_unit_vector (n,R) iff i = j ) )
assume AS: ( 1 <= i & i <= n & 1 <= j & j <= n ) ; :: thesis: ( i _th_unit_vector (n,R) = j _th_unit_vector (n,R) iff i = j )

now :: thesis: ( i _th_unit_vector (n,R) = j _th_unit_vector (n,R) implies i = j )

assume A: i _th_unit_vector (n,R) = j _th_unit_vector (n,R) ; :: thesis: i = j

now :: thesis: not i <> j

assume i <> j ; :: thesis: contradiction
then 0. R = (j _th_unit_vector (n,R)) . j by A, AS, u1;
hence contradiction by AS, u1; :: thesis: verum

end;

hence i = j ; :: thesis: verum

end;

hence ( i _th_unit_vector (n,R) = j _th_unit_vector (n,R) iff i = j ) ; :: thesis: verum