let V be RealLinearSpace; :: thesis: ( 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 ) implies OASpace V is OAffinSpace )

assume A1: 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 ) ; :: thesis:
then A2: ( ex a, b, c, d being Element of () st
( not a,b // c,d & not a,b // d,c ) & ( for a, b, c being Element of () ex d being Element of () st
( a,b // c,d & a,c // b,d & b <> d ) ) ) by Th23;
A3: for p, a, b, c being Element of () st p <> b & b,p // p,c holds
ex d being Element of () st
( a,p // p,d & a,b // c,d ) by ;
( ex a, b being Element of () st a <> b & ( for a, b, c, d, p, q, r, s being Element of () holds
( a,b // c,c & ( a,b // b,a implies a = b ) & ( a <> b & a,b // p,q & a,b // r,s implies p,q // r,s ) & ( a,b // c,d implies b,a // d,c ) & ( a,b // b,c implies a,b // a,c ) & ( not a,b // a,c or a,b // b,c or a,c // c,b ) ) ) ) by ;
hence OASpace V is OAffinSpace by ; :: thesis: verum