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