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:29;
then consider a being Integer such that
A2: x = a * w1 by A1, Th16;
consider b being Integer such that
A3: b = 0 ;
x = (a * w1) + (0. V) by A2, RLVECT_1:4;
then x = (a * w1) + (b * w2) by A3, RLVECT_1:10;
hence ex a, b being Integer st x = (a * w1) + (b * w2) ; :: thesis: verum

end;

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

consider l being Linear_Combination of {w1,w2} such that
A5: ( x = Sum l & rng l c= INT ) by A1;
A6: x = ((l . w1) * w1) + ((l . w2) * w2) by A4, A5, RLVECT_2:33;
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:3;
hence ex a, b being Integer st x = (a * w1) + (b * w2) by A5, A6; :: 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 A7: 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 A8: w1 = w2 ; :: thesis: x in Z_Lin {w1,w2}

then x = (a + b) * w1 by A7, RLVECT_1:def 6;
then x in Z_Lin {w1} by Th16;
hence x in Z_Lin {w1,w2} by A8, ENUMSET1:29; :: thesis: verum

end;

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

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

A12: 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 A11; :: thesis: verum

end;

then reconsider f = f as Linear_Combination of V by RLVECT_2:def 3;
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
A13: x in Carrier f and
A14: not x in {w1,w2} ; :: thesis: contradiction
( x <> w1 & x <> w2 ) by A14, TARSKI:def 2;
then f . x = 0 by A11, A13;
hence contradiction by A13, RLVECT_2:19; :: thesis: verum

end;

then reconsider f = f as Linear_Combination of {w1,w2} by RLVECT_2:def 6;
A15: x = Sum f by A7, A9, A10, RLVECT_2:33;
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 A16: y in rng f ; :: thesis: y in INT
consider x being set such that
A17: ( x in the carrier of V & y = f . x ) by A16, FUNCT_2:11;
reconsider v = x as VECTOR of V by A17;

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 A12;
hence y in INT by A17, 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 A10, TARSKI:def 2;
hence y in INT by A17, INT_1:def 2; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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