theorem :: ANALMETR:19

for V being RealLinearSpace
for w, y being VECTOR of V holds
( the carrier of (AMSpace (V,w,y)) = the carrier of V & the CONGR of (AMSpace (V,w,y)) = lambda (DirPar V) & the orthogonality of (AMSpace (V,w,y)) = Orthogonality (V,w,y) ) ;