let X be RealNormSpace; :: thesis:
A1: for x being object holds
( x in BoundedLinearFunctionals X iff x in BoundedLinearOperators (X,RNS_Real) )

proof

let x be object ; :: thesis:

hereby :: thesis:

assume x in BoundedLinearFunctionals X ; :: thesis:
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:

end;

assume x in BoundedLinearOperators (X,RNS_Real) ; :: thesis:
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:

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: