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