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