theorem :: PAPDESAF:5

for V being RealLinearSpace
for OAS being OAffinSpace st OAS = OASpace V holds
ex u, v being VECTOR of V st
for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 )