let X be RealNormSpace; :: thesis: the carrier of (DualSp X) = the carrier of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real))
A1: for x being object holds
( x in BoundedLinearFunctionals X iff x in BoundedLinearOperators (X,RNS_Real) )

proof

let x be object ; :: thesis: ( x in BoundedLinearFunctionals X iff x in BoundedLinearOperators (X,RNS_Real) )

hereby :: thesis: ( x in BoundedLinearOperators (X,RNS_Real) implies x in BoundedLinearFunctionals X )

assume x in BoundedLinearFunctionals X ; :: thesis: x in BoundedLinearOperators (X,RNS_Real)
then x is additive homogeneous Lipschitzian Functional of X by DUALSP01:def 10;
then x is additive homogeneous Lipschitzian Function of X,RNS_Real by LMN7;
hence x in BoundedLinearOperators (X,RNS_Real) by LOPBAN_1:def 9; :: thesis: verum

end;

assume x in BoundedLinearOperators (X,RNS_Real) ; :: thesis: x in BoundedLinearFunctionals X
then x is Lipschitzian LinearOperator of X,RNS_Real by LOPBAN_1:def 9;
then x is additive homogeneous Lipschitzian Functional of X by LMN7;
hence x in BoundedLinearFunctionals X by DUALSP01:def 10; :: thesis: verum

end;

R_NormSpace_of_BoundedLinearOperators (X,RNS_Real) = NORMSTR(# (BoundedLinearOperators (X,RNS_Real)),(Zero_ ((BoundedLinearOperators (X,RNS_Real)),(R_VectorSpace_of_LinearOperators (X,RNS_Real)))),(Add_ ((BoundedLinearOperators (X,RNS_Real)),(R_VectorSpace_of_LinearOperators (X,RNS_Real)))),(Mult_ ((BoundedLinearOperators (X,RNS_Real)),(R_VectorSpace_of_LinearOperators (X,RNS_Real)))),(BoundedLinearOperatorsNorm (X,RNS_Real)) #) by LOPBAN_1:def 14;
hence the carrier of (DualSp X) = the carrier of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real)) by A1, TARSKI:2; :: thesis: verum