let R be Ring; :: thesis: for n being Nat
for v being Element of n -tuples_on the carrier of R
for a being Element of R
for i being Nat st 1 <= i & i <= n holds
( (a * (i _th_unit_vector (n,R))) . i = a & ( for j being Nat st j <> i & 1 <= j & j <= n holds
(a * (j _th_unit_vector (n,R))) . i = 0. R ) )
let n be Nat; :: thesis: for v being Element of n -tuples_on the carrier of R
for a being Element of R
for i being Nat st 1 <= i & i <= n holds
( (a * (i _th_unit_vector (n,R))) . i = a & ( for j being Nat st j <> i & 1 <= j & j <= n holds
(a * (j _th_unit_vector (n,R))) . i = 0. R ) )
let v be Element of n -tuples_on the carrier of R; :: thesis: for a being Element of R
for i being Nat st 1 <= i & i <= n holds
( (a * (i _th_unit_vector (n,R))) . i = a & ( for j being Nat st j <> i & 1 <= j & j <= n holds
(a * (j _th_unit_vector (n,R))) . i = 0. R ) )
let a be Element of R; :: thesis: for i being Nat st 1 <= i & i <= n holds
( (a * (i _th_unit_vector (n,R))) . i = a & ( for j being Nat st j <> i & 1 <= j & j <= n holds
(a * (j _th_unit_vector (n,R))) . i = 0. R ) )
let i be Nat; :: thesis: ( 1 <= i & i <= n implies ( (a * (i _th_unit_vector (n,R))) . i = a & ( for j being Nat st j <> i & 1 <= j & j <= n holds
(a * (j _th_unit_vector (n,R))) . i = 0. R ) ) )
assume AS: ( 1 <= i & i <= n ) ; :: thesis: ( (a * (i _th_unit_vector (n,R))) . i = a & ( for j being Nat st j <> i & 1 <= j & j <= n holds
(a * (j _th_unit_vector (n,R))) . i = 0. R ) )
then B: (i _th_unit_vector (n,R)) . i = 1. R by u1;
i in Seg n by AS;
hence (a * (i _th_unit_vector (n,R))) . i = a * (1. R) by B, FVSUM_1:51
.= a ;
:: thesis: for j being Nat st j <> i & 1 <= j & j <= n holds
(a * (j _th_unit_vector (n,R))) . i = 0. R

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

let j be Nat; :: thesis: ( j <> i & 1 <= j & j <= n implies (a * (j _th_unit_vector (n,R))) . i = 0. R )
assume ( j <> i & 1 <= j & j <= n ) ; :: thesis: (a * (j _th_unit_vector (n,R))) . i = 0. R
then D: (j _th_unit_vector (n,R)) . i = 0. R by AS, u1;
i in Seg n by AS;
hence (a * (j _th_unit_vector (n,R))) . i = a * (0. R) by D, FVSUM_1:51
.= 0. R ;
:: thesis: verum

end;

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