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