theorem Th16: :: ANALMETR:16

for V being RealLinearSpace holds the carrier of (Lambda (OASpace V)) = the carrier of V