theorem :: DUALSP01:8

for V being RealLinearSpace holds 0. (V *') = the carrier of V --> 0