let R be Ring; :: thesis: 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 ) )
let n, i be Nat; :: thesis: ( 1 <= i & i <= n implies ( (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 ) ) )
set v = i _th_unit_vector (n,R);
assume AS: ( 1 <= i & i <= n ) ; :: thesis: ( (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 ) )
A: ( 1 <= i & i <= len (n |-> (0. R)) ) by AS, FINSEQ_2:132;
D: dom (i _th_unit_vector (n,R)) = Seg n by FINSEQ_2:124;
hence (i _th_unit_vector (n,R)) . i = (i _th_unit_vector (n,R)) /. i by AS, FINSEQ_1:1, PARTFUN1:def 6
.= 1. R by A, FINSEQ_7:8 ;
:: thesis: for j being Nat st 1 <= j & j <= n & j <> i holds
(i _th_unit_vector (n,R)) . j = 0. R

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

let j be Nat; :: thesis: ( 1 <= j & j <= n & j <> i implies (i _th_unit_vector (n,R)) . j = 0. R )
assume C: ( 1 <= j & j <= n & j <> i ) ; :: thesis: (i _th_unit_vector (n,R)) . j = 0. R
B: ( 1 <= j & j <= len (n |-> (0. R)) ) by C, FINSEQ_2:132;
E: dom (n |-> (0. R)) = Seg n by FINSEQ_2:124;
thus (i _th_unit_vector (n,R)) . j = (i _th_unit_vector (n,R)) /. j by D, C, FINSEQ_1:1, PARTFUN1:def 6
.= (n |-> (0. R)) /. j by C, B, FINSEQ_7:10
.= (n |-> (0. R)) . j by E, C, FINSEQ_1:1, PARTFUN1:def 6
.= ((Seg n) --> (0. R)) . j by FINSEQ_2:def 2
.= 0. R by C, FINSEQ_1:1, FUNCOP_1:7 ; :: thesis: verum

end;

hence for j being Nat st 1 <= j & j <= n & j <> i holds
(i _th_unit_vector (n,R)) . j = 0. R ; :: thesis: verum