let x be set ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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) ) :: thesis: ( ex a, b being Integer st x = (a * w1) + (b * w2) implies x in Z_Lin {w1,w2} )

proof

assume A1: x in Z_Lin {w1,w2} ; :: thesis: ex a, b being Integer st x = (a * w1) + (b * w2)

now

per cases ( w1 = w2 or w1 <> w2 ) ;

suppose w1 = w2 ; :: thesis: ex a, b being Integer st x = (a * w1) + (b * w2)

then {w1,w2} = {w1} by ENUMSET1:69;
then consider a being Integer such that
A2: x = a * w1 by A1, R4Th11;
consider b being Integer such that
AA: b = 0 ;
x = (a * w1) + (0. V) by A2, RLVECT_1:10;
then x = (a * w1) + (b * w2) by RLVECT_1:23, AA;
hence ex a, b being Integer st x = (a * w1) + (b * w2) ; :: thesis: verum

end;

suppose A3: w1 <> w2 ; :: thesis: ex a, b being Integer st x = (a * w1) + (b * w2)

consider l being Linear_Combination of {w1,w2} such that
A4: ( x = Sum l & rng l c= INT ) by A1;
A5: x = ((l . w1) * w1) + ((l . w2) * w2) by A3, A4, RLVECT_2:51;
ex f being Function st
( l = f & dom f = the carrier of V & rng f c= REAL ) by FUNCT_2:def 2;
then ( l . w1 in rng l & l . w2 in rng l ) by FUNCT_1:12;
hence ex a, b being Integer st x = (a * w1) + (b * w2) by A4, A5; :: thesis: verum

end;

end;

end;

hence ex a, b being Integer st x = (a * w1) + (b * w2) ; :: thesis: verum

end;

given a0, b0 being Integer such that A5: x = (a0 * w1) + (b0 * w2) ; :: thesis: x in Z_Lin {w1,w2}
reconsider a = a0, b = b0 as Real by XREAL_0:def 1;

now

per cases ( w1 = w2 or w1 <> w2 ) ;

suppose A6: w1 = w2 ; :: thesis: x in Z_Lin {w1,w2}

then x = (a + b) * w1 by A5, RLVECT_1:def 9;
then x in Z_Lin {w1} by R4Th11;
hence x in Z_Lin {w1,w2} by A6, ENUMSET1:69; :: thesis: verum

end;

suppose A7: w1 <> w2 ; :: thesis: x in Z_Lin {w1,w2}

consider f being Function of the carrier of V,REAL such that
A8: ( f . w1 = a & f . w2 = b ) and
A9: for u being VECTOR of V st u <> w1 & u <> w2 holds
f . u = H₁(u) from FUNCT_2:sch 7(A7);
reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:11;

A90: now

let u be VECTOR of V; :: thesis: ( not u in {w1,w2} implies f . u = 0 )
assume not u in {w1,w2} ; :: thesis: f . u = 0
then ( u <> w1 & u <> w2 ) by TARSKI:def 2;
hence f . u = 0 by A9; :: thesis: verum

end;

then reconsider f = f as Linear_Combination of V by RLVECT_2:def 5;
Carrier f c= {w1,w2}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in {w1,w2} )
assume that
A10: x in Carrier f and
A11: not x in {w1,w2} ; :: thesis: contradiction
( x <> w1 & x <> w2 ) by A11, TARSKI:def 2;
then f . x = 0 by A9, A10;
hence contradiction by A10, RLVECT_2:28; :: thesis: verum

end;

then reconsider f = f as Linear_Combination of {w1,w2} by RLVECT_2:def 8;
A12: x = Sum f by A5, A7, A8, RLVECT_2:51;
rng f c= INT

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in INT )
assume AD: y in rng f ; :: thesis: y in INT
consider x being set such that
R1: ( x in the carrier of V & y = f . x ) by AD, FUNCT_2:17;
reconsider v = x as VECTOR of V by R1;

per cases ( not v in {w1,w2} or v in {w1,w2} ) ;

suppose not v in {w1,w2} ; :: thesis: y in INT

then f . v = 0 by A90;
hence y in INT by R1, NUMBERS:17, TARSKI:def 3; :: thesis: verum

end;

suppose v in {w1,w2} ; :: thesis: y in INT

then ( f . v = a0 or f . v = b0 ) by A8, TARSKI:def 2;
hence y in INT by R1, INT_1:def 2; :: thesis: verum

end;

end;

end;

hence x in Z_Lin {w1,w2} by A12; :: thesis: verum

end;

end;

end;

hence x in Z_Lin {w1,w2} ; :: thesis: verum