let X be RealNormSpace; :: thesis: DualSp X is RealNormSpace
RLSStruct(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))) #) is RealLinearSpace ;
hence DualSp X is RealNormSpace by RSSPACE3:2; :: thesis: verum