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₁( 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₁(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