theorem Th6: :: ANPROJ_1:6

for V being RealLinearSpace
for u, v, w being Element of V st not v is zero & not w is zero & not are_Prop v,w holds
( v,w,u are_LinDep iff ex a, b being Real st u = (a * v) + (b * w) )