let x be set ; for V being RealLinearSpace
for w1, w2 being VECTOR of V holds
( x in Z_Lin {w1,w2} iff ex a, b being Integer st x = (a * w1) + (b * w2) )
let V be RealLinearSpace; for w1, w2 being VECTOR of V holds
( x in Z_Lin {w1,w2} iff ex a, b being Integer st x = (a * w1) + (b * w2) )
let w1, w2 be VECTOR of V; ( x in Z_Lin {w1,w2} iff ex a, b being Integer st x = (a * w1) + (b * w2) )
thus
( x in Z_Lin {w1,w2} implies ex a, b being Integer st x = (a * w1) + (b * w2) )
( ex a, b being Integer st x = (a * w1) + (b * w2) implies x in Z_Lin {w1,w2} )
given a0, b0 being Integer such that A7:
x = (a0 * w1) + (b0 * w2)
; x in Z_Lin {w1,w2}
reconsider a = a0, b = b0 as Element of REAL by XREAL_0:def 1;
hence
x in Z_Lin {w1,w2}
; verum