theorem Th5: :: ANPROJ_2:5

for V being RealLinearSpace
for u, v, u1, v1 being Element of V st ( for a, b, a1, b1 being Real st (((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1) = 0. V holds
( a = 0 & b = 0 & a1 = 0 & b1 = 0 ) ) holds
for y being Element of V holds
( y is zero or not u,v,y are_LinDep or not u1,v1,y are_LinDep )