theorem Th20: :: ANALMETR:20

for V being RealLinearSpace
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)