theorem :: RLVECT_4:13

for x being set
for V being RealLinearSpace
for v, w1, w2 being VECTOR of V holds
( x in v + (Lin {w1,w2}) iff ex a, b being Real st x = (v + (a * w1)) + (b * w2) )