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
( not u is zero & not v is zero & not are_Prop u,v & not u1 is zero & not v1 is zero & not are_Prop u1,v1 & not u,v,u1 are_LinDep & not u1,v1,u are_LinDep )