let x be set ; for V being RealLinearSpace
for v, w1, w2 being VECTOR of V holds
( x in v + (Z_Lin {w1,w2}) iff ex a, b being Integer st x = (v + (a * w1)) + (b * w2) )
let V be RealLinearSpace; for v, w1, w2 being VECTOR of V holds
( x in v + (Z_Lin {w1,w2}) iff ex a, b being Integer st x = (v + (a * w1)) + (b * w2) )
let v, w1, w2 be VECTOR of V; ( x in v + (Z_Lin {w1,w2}) iff ex a, b being Integer st x = (v + (a * w1)) + (b * w2) )
thus
( x in v + (Z_Lin {w1,w2}) implies ex a, b being Integer st x = (v + (a * w1)) + (b * w2) )
( ex a, b being Integer st x = (v + (a * w1)) + (b * w2) implies x in v + (Z_Lin {w1,w2}) )
given a, b being Integer such that A4:
x = (v + (a * w1)) + (b * w2)
; x in v + (Z_Lin {w1,w2})
(a * w1) + (b * w2) in Z_Lin {w1,w2}
by Th19;
then
v + ((a * w1) + (b * w2)) in v + (Z_Lin {w1,w2})
;
hence
x in v + (Z_Lin {w1,w2})
by A4, RLVECT_1:def 3; verum