let x be set ; :: thesis: for V being RealLinearSpace
for v, w1, w2, w3 being VECTOR of V holds
( x in v + (Lin {w1,w2,w3}) iff ex a, b, c being Real st x = ((v + (a * w1)) + (b * w2)) + (c * w3) )
let V be RealLinearSpace; :: thesis: for v, w1, w2, w3 being VECTOR of V holds
( x in v + (Lin {w1,w2,w3}) iff ex a, b, c being Real st x = ((v + (a * w1)) + (b * w2)) + (c * w3) )
let v, w1, w2, w3 be VECTOR of V; :: thesis: ( x in v + (Lin {w1,w2,w3}) iff ex a, b, c being Real st x = ((v + (a * w1)) + (b * w2)) + (c * w3) )
thus ( x in v + (Lin {w1,w2,w3}) implies ex a, b, c being Real st x = ((v + (a * w1)) + (b * w2)) + (c * w3) ) :: thesis: ( ex a, b, c being Real st x = ((v + (a * w1)) + (b * w2)) + (c * w3) implies x in v + (Lin {w1,w2,w3}) )

proof

assume x in v + (Lin {w1,w2,w3}) ; :: thesis: ex a, b, c being Real st x = ((v + (a * w1)) + (b * w2)) + (c * w3)
then consider u being VECTOR of V such that
A1: u in Lin {w1,w2,w3} and
A2: x = v + u by RLSUB_1:63;
consider a, b, c being Real such that
A3: u = ((a * w1) + (b * w2)) + (c * w3) by A1, Th14;
take a ; :: thesis: ex b, c being Real st x = ((v + (a * w1)) + (b * w2)) + (c * w3)
take b ; :: thesis: ex c being Real st x = ((v + (a * w1)) + (b * w2)) + (c * w3)
take c ; :: thesis: x = ((v + (a * w1)) + (b * w2)) + (c * w3)
x = (v + ((a * w1) + (b * w2))) + (c * w3) by A2, A3, RLVECT_1:def 3;
hence x = ((v + (a * w1)) + (b * w2)) + (c * w3) by RLVECT_1:def 3; :: thesis: verum

end;

given a, b, c being Real such that A4: x = ((v + (a * w1)) + (b * w2)) + (c * w3) ; :: thesis: x in v + (Lin {w1,w2,w3})
((a * w1) + (b * w2)) + (c * w3) in Lin {w1,w2,w3} by Th14;
then v + (((a * w1) + (b * w2)) + (c * w3)) in v + (Lin {w1,w2,w3}) by RLSUB_1:63;
then (v + ((a * w1) + (b * w2))) + (c * w3) in v + (Lin {w1,w2,w3}) by RLVECT_1:def 3;
hence x in v + (Lin {w1,w2,w3}) by A4, RLVECT_1:def 3; :: thesis: verum