let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V holds AffinStruct(# the carrier of (AMSpace (V,w,y)), the CONGR of (AMSpace (V,w,y)) #) = Lambda (OASpace V)
let w, y be VECTOR of V; :: thesis: AffinStruct(# the carrier of (AMSpace (V,w,y)), the CONGR of (AMSpace (V,w,y)) #) = Lambda (OASpace V)
set Y = OASpace V;
the carrier of (Lambda (OASpace V)) = the carrier of V by Th16;
hence AffinStruct(# the carrier of (AMSpace (V,w,y)), the CONGR of (AMSpace (V,w,y)) #) = Lambda (OASpace V) by Th17; :: thesis: verum