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

proof

assume x in Z_Lin {v} ; :: thesis: ex a being Integer st x = a * v
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: verum

end;

given a0 being Integer such that A3: x = a0 * v ; :: thesis: x in Z_Lin {v}
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: for z being VECTOR of V st not z in {v} holds
f . z = 0

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

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: ( not x in Carrier f or x in {v} )
assume A7: x in Carrier f ; :: thesis: x in {v}
then f . x <> 0 by RLVECT_2:19;
then x = v by A5, A7;
hence x in {v} by TARSKI:def 1; :: thesis: verum

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: ( not y in rng f or y in INT )
assume A9: y in rng f ; :: thesis: y in INT
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 ( not z in {v} or z in {v} ) ;

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

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

end;

suppose z in {v} ; :: thesis: y in INT

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

end;

end;

end;

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