let V be Z_Module; :: thesis: for u being Vector of V ex l being Linear_Combination of V st

( l . u = 1 & ( for v being Vector of V st v <> u holds

l . v = 0 ) )

let u be Element of V; :: thesis: ex l being Linear_Combination of V st

( l . u = 1 & ( for v being Vector of V st v <> u holds

l . v = 0 ) )

reconsider i0 = 0 as Element of INT by INT_1:def 2;

deffunc H_{1}( Element of V) -> Element of INT = i0;

reconsider i1 = 1 as Element of INT by INT_1:def 2;

ex f being Function of the carrier of V,INT st

( f . u = i1 & ( for v being Element of V st v <> u holds

f . v = H_{1}(v) ) )
from FUNCT_2:sch 6();

then consider f being Function of the carrier of V,INT such that

A1: f . u = 1 and

A2: for v being Element of V st v <> u holds

f . v = 0 ;

for v being Element of V st not v in {u} holds

v <> u by TARSKI:def 1;

then A3: for v being Element of V st not v in {u} holds

f . v = 0. INT.Ring by A2;

reconsider f = f as Element of Funcs ( the carrier of V, the carrier of INT.Ring) by FUNCT_2:8;

reconsider f = f as Linear_Combination of V by A3, VECTSP_6:def 1;

take f ; :: thesis: ( f . u = 1 & ( for v being Vector of V st v <> u holds

f . v = 0 ) )

thus ( f . u = 1 & ( for v being Vector of V st v <> u holds

f . v = 0 ) ) by A1, A2; :: thesis: verum

( l . u = 1 & ( for v being Vector of V st v <> u holds

l . v = 0 ) )

let u be Element of V; :: thesis: ex l being Linear_Combination of V st

( l . u = 1 & ( for v being Vector of V st v <> u holds

l . v = 0 ) )

reconsider i0 = 0 as Element of INT by INT_1:def 2;

deffunc H

reconsider i1 = 1 as Element of INT by INT_1:def 2;

ex f being Function of the carrier of V,INT st

( f . u = i1 & ( for v being Element of V st v <> u holds

f . v = H

then consider f being Function of the carrier of V,INT such that

A1: f . u = 1 and

A2: for v being Element of V st v <> u holds

f . v = 0 ;

for v being Element of V st not v in {u} holds

v <> u by TARSKI:def 1;

then A3: for v being Element of V st not v in {u} holds

f . v = 0. INT.Ring by A2;

reconsider f = f as Element of Funcs ( the carrier of V, the carrier of INT.Ring) by FUNCT_2:8;

reconsider f = f as Linear_Combination of V by A3, VECTSP_6:def 1;

take f ; :: thesis: ( f . u = 1 & ( for v being Vector of V st v <> u holds

f . v = 0 ) )

thus ( f . u = 1 & ( for v being Vector of V st v <> u holds

f . v = 0 ) ) by A1, A2; :: thesis: verum