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