let X be RealUnitarySpace; :: thesis: BoundedLinearFunctionals X = BoundedLinearFunctionals (RUSp2RNSp X)
set Y = RUSp2RNSp X;

now :: thesis: for x being object st x in BoundedLinearFunctionals X holds
x in BoundedLinearFunctionals (RUSp2RNSp X)

let x be object ; :: thesis: ( x in BoundedLinearFunctionals X implies x in BoundedLinearFunctionals (RUSp2RNSp X) )
assume x in BoundedLinearFunctionals X ; :: thesis: x in BoundedLinearFunctionals (RUSp2RNSp X)
then A1: x is Lipschitzian linear-Functional of X by Def10;
then x is linear-Functional of (RUSp2RNSp X) by LM6A;
then x is Lipschitzian linear-Functional of (RUSp2RNSp X) by A1, LM6B;
hence x in BoundedLinearFunctionals (RUSp2RNSp X) by DUALSP01:def 10; :: thesis: verum

end;

then A2: BoundedLinearFunctionals X c= BoundedLinearFunctionals (RUSp2RNSp X) ;

now :: thesis: for x being object st x in BoundedLinearFunctionals (RUSp2RNSp X) holds
x in BoundedLinearFunctionals X

let x be object ; :: thesis: ( x in BoundedLinearFunctionals (RUSp2RNSp X) implies x in BoundedLinearFunctionals X )
assume x in BoundedLinearFunctionals (RUSp2RNSp X) ; :: thesis: x in BoundedLinearFunctionals X
then x is Lipschitzian linear-Functional of (RUSp2RNSp X) by DUALSP01:def 10;
then x is Lipschitzian linear-Functional of X by LM6B, LM6A;
hence x in BoundedLinearFunctionals X by Def10; :: thesis: verum

end;

then BoundedLinearFunctionals (RUSp2RNSp X) c= BoundedLinearFunctionals X ;
hence BoundedLinearFunctionals X = BoundedLinearFunctionals (RUSp2RNSp X) by A2; :: thesis: verum