let x be set ; :: thesis:
let V be RealLinearSpace; :: thesis:
let v be VECTOR of V; :: thesis:
thus ( x in Z_Lin {v} implies ex a being Integer st x = a * v ) :: thesis:

proof

assume x in Z_Lin {v} ; :: thesis:
then consider l being Linear_Combination of {v} such that
A1: ( x = Sum l & rng l c= INT ) ;
A2: Sum l = (l . v) * v by RLVECT_2:32;
ex f being Function st
( l = f & dom f = the carrier of V & rng f c= REAL ) by FUNCT_2:def 2;
then l . v in rng l by FUNCT_1:3;
hence ex a being Integer st x = a * v by A1, A2; :: thesis:

end;

given a0 being Integer such that A3: x = a0 * v ; :: thesis:
reconsider a = a0 as Element of REAL by XREAL_0:def 1;
consider f being Function of the carrier of V,REAL such that
A4: f . v = a and
A5: for z being VECTOR of V st z <> v holds
f . z = H₁(z) from FUNCT_2:sch 6();
reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;

A6: now :: thesis:

let z be VECTOR of V; :: thesis:
assume not z in {v} ; :: thesis:
then z <> v by TARSKI:def 1;
hence f . z = 0 by A5; :: thesis:

end;

then reconsider f = f as Linear_Combination of V by RLVECT_2:def 3;
Carrier f c= {v}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A7: x in Carrier f ; :: thesis:
then f . x <> 0 by RLVECT_2:19;
then x = v by A5, A7;
hence x in {v} by TARSKI:def 1; :: thesis:

end;

then reconsider f = f as Linear_Combination of {v} by RLVECT_2:def 6;
A8: Sum f = x by A3, A4, RLVECT_2:32;
rng f c= INT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A9: y in rng f ; :: thesis:
consider x being object such that
A10: ( x in the carrier of V & y = f . x ) by A9, FUNCT_2:11;
reconsider z = x as VECTOR of V by A10;

per cases ;

suppose not z in {v} ; :: thesis:

then f . z = 0 by A6;
hence y in INT by A10, NUMBERS:17; :: thesis:

end;

suppose z in {v} ; :: thesis:

then f . z = a0 by A4, TARSKI:def 1;
hence y in INT by A10, INT_1:def 2; :: thesis:

end;

end;

end;

hence x in Z_Lin {v} by A8; :: thesis: