theorem :: ANALMETR:18

for V being RealLinearSpace
for u, u1, v, v1 being VECTOR of V
for p, p1, q, q1 being Element of (Lambda (OASpace V)) st p = u & q = v & p1 = u1 & q1 = v1 holds
( p,q // p1,q1 iff ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) )