theorem Th75A: :: DUALSP02:14

for X being RealNormSpace holds the carrier of (DualSp X) = the carrier of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real))