let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V st Gen w,y holds
OASpace V is OAffinSpace
let w, y be VECTOR of V; :: thesis: ( Gen w,y implies OASpace V is OAffinSpace )
assume Gen w,y ; :: thesis: OASpace V is OAffinSpace
then for a1, a2 being Real st (a1 * w) + (a2 * y) = 0. V holds
( a1 = 0 & a2 = 0 ) by ANALMETR:def 1;
hence OASpace V is OAffinSpace by ANALOAF:26; :: thesis: verum