let V be RealUnitarySpace; :: thesis: for v, w1, w2 being VECTOR of V
for x being set holds
( x in v + (Lin {w1,w2}) iff ex a, b being Real st x = (v + (a * w1)) + (b * w2) )
let v, w1, w2 be VECTOR of V; :: thesis: for x being set holds
( x in v + (Lin {w1,w2}) iff ex a, b being Real st x = (v + (a * w1)) + (b * w2) )
let x be set ; :: thesis: ( x in v + (Lin {w1,w2}) iff ex a, b being Real st x = (v + (a * w1)) + (b * w2) )
thus ( x in v + (Lin {w1,w2}) implies ex a, b being Real st x = (v + (a * w1)) + (b * w2) ) :: thesis: ( ex a, b being Real st x = (v + (a * w1)) + (b * w2) implies x in v + (Lin {w1,w2}) )
proof
assume x in v + (Lin {w1,w2}) ; :: thesis: ex a, b being Real st x = (v + (a * w1)) + (b * w2)
then consider u being VECTOR of V such that
A1: u in Lin {w1,w2} and
A2: x = v + u by RUSUB_2:63;
consider a, b being Real such that
A3: u = (a * w1) + (b * w2) by A1, Th32;
take a ; :: thesis: ex b being Real st x = (v + (a * w1)) + (b * w2)
take b ; :: thesis: x = (v + (a * w1)) + (b * w2)
thus x = (v + (a * w1)) + (b * w2) by A2, A3, RLVECT_1:def 3; :: thesis: verum
end;
given a, b being Real such that A4: x = (v + (a * w1)) + (b * w2) ; :: thesis: x in v + (Lin {w1,w2})
(a * w1) + (b * w2) in Lin {w1,w2} by Th32;
then v + ((a * w1) + (b * w2)) in v + (Lin {w1,w2}) by RUSUB_2:63;
hence x in v + (Lin {w1,w2}) by A4, RLVECT_1:def 3; :: thesis: verum