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

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

let x be object ; :: thesis: ( x in LinearFunctionals X implies x in LinearFunctionals (RUSp2RNSp X) )
assume x in LinearFunctionals X ; :: thesis: x in LinearFunctionals (RUSp2RNSp X)
then x is linear-Functional of X by DUALSP01:def 6;
then x is linear-Functional of (RUSp2RNSp X) by LM6A;
hence x in LinearFunctionals (RUSp2RNSp X) by DUALSP01:def 6; :: thesis: verum

end;

then A1: LinearFunctionals X c= LinearFunctionals (RUSp2RNSp X) ;

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

let x be object ; :: thesis: ( x in LinearFunctionals (RUSp2RNSp X) implies x in LinearFunctionals X )
assume x in LinearFunctionals (RUSp2RNSp X) ; :: thesis: x in LinearFunctionals X
then x is linear-Functional of (RUSp2RNSp X) by DUALSP01:def 6;
then x is linear-Functional of X by LM6A;
hence x in LinearFunctionals X by DUALSP01:def 6; :: thesis: verum

end;

then LinearFunctionals (RUSp2RNSp X) c= LinearFunctionals X ;
hence LinearFunctionals X = LinearFunctionals (RUSp2RNSp X) by A1; :: thesis: verum