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

( 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