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

proof

assume x in v + (Z_Lin {w}) ; :: thesis: ex a being Integer st x = v + (a * w)
then consider u being VECTOR of V such that
A1: x = v + u and
A2: u in Z_Lin {w} ;
ex a being Integer st u = a * w by A2, Th16;
hence ex a being Integer st x = v + (a * w) by A1; :: thesis: verum

end;

given a0 being Integer such that A3: x = v + (a0 * w) ; :: thesis: x in v + (Z_Lin {w})
a0 * w in Z_Lin {w} by Th16;
hence x in v + (Z_Lin {w}) by A3; :: thesis: verum