theorem Th1: :: DUALSP01:5

for V being RealLinearSpace
for x being object holds
( x in the carrier of (V *') iff x is linear-Functional of V )