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

set Y = RUSp2RNSp X;

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

set Y = RUSp2RNSp X;

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

x in LinearFunctionals (RUSp2RNSp X)

then A1:
LinearFunctionals X c= LinearFunctionals (RUSp2RNSp X)
;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;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

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

x in LinearFunctionals X

then
LinearFunctionals (RUSp2RNSp X) c= LinearFunctionals X
;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;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

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