let V be RealLinearSpace; :: thesis: the carrier of (Lambda (OASpace V)) = the carrier of V
( Lambda (OASpace V) = AffinStruct(# the carrier of (OASpace V),(lambda the CONGR of (OASpace V)) #) & OASpace V = AffinStruct(# the carrier of V,(DirPar V) #) ) by ANALOAF:def 4, DIRAF:def 2;
hence the carrier of (Lambda (OASpace V)) = the carrier of V ; :: thesis: verum