let V be RealLinearSpace; :: thesis: the CONGR of (Lambda (OASpace V)) = lambda (DirPar 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 CONGR of (Lambda (OASpace V)) = lambda (DirPar V) by A1; :: thesis: verum