theorem Th17: :: ANALMETR:17

for V being RealLinearSpace holds the CONGR of (Lambda (OASpace V)) = lambda (DirPar V)