theorem Th26: :: ANALOAF:26

for V being RealLinearSpace st 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 ) holds
OASpace V is OAffinSpace