for V being RealLinearSpace
for p, q being Element of V
for a1, b1, a2, b2 being Real st not are_Prop p,q & (a1 * p) + (b1 * q) = (a2 * p) + (b2 * q) & not p is zero & not q is zero holds
( a1 = a2 & b1 = b2 )