let V be RealLinearSpace; :: thesis: for x being set holds
( x is Element of (OASpace V) iff x is VECTOR of V )
let x be set ; :: thesis: ( x is Element of (OASpace V) iff x is VECTOR of V )
OASpace V = AffinStruct(# the carrier of V,(DirPar V) #) by ANALOAF:def 4;
hence ( x is Element of (OASpace V) iff x is VECTOR of V ) ; :: thesis: verum