for V being RealLinearSpace
for o, u, u2 being Element of V st o,u,u2 are_LinDep & not are_Prop o,u & not are_Prop o,u2 & not are_Prop u,u2 & o,u,u2 are_Prop_Vect holds
( ex a1, b1 being Real st
( b1 * u2 = o + (a1 * u) & a1 <> 0 & b1 <> 0 ) & ex a2, c2 being Real st
( u2 = (c2 * o) + (a2 * u) & c2 <> 0 & a2 <> 0 ) )