let X be RealUnitarySpace; :: thesis: DualSp X = DualSp (RUSp2RNSp X)
set Y = RUSp2RNSp X;
set X1 = BoundedLinearFunctionals X;
set Y1 = BoundedLinearFunctionals (RUSp2RNSp X);
A0: the carrier of (X *') = the carrier of ((RUSp2RNSp X) *') by LM10B;
A2: the ZeroF of (DualSp X) = 0. (X *') by RSSPACE:def 10
.= 0. ((RUSp2RNSp X) *') by LM10B
.= the ZeroF of (DualSp (RUSp2RNSp X)) by DUALSP01:17, RSSPACE:def 10 ;
A3: the addF of (DualSp X) = the addF of (X *') || (BoundedLinearFunctionals X) by RSSPACE:def 8
.= the addF of ((RUSp2RNSp X) *') || (BoundedLinearFunctionals (RUSp2RNSp X)) by LM6, A0
.= the addF of (DualSp (RUSp2RNSp X)) by DUALSP01:17, RSSPACE:def 8 ;
A4: the Mult of (DualSp X) = the Mult of (X *') | [:REAL,(BoundedLinearFunctionals X):] by RSSPACE:def 9
.= the Mult of ((RUSp2RNSp X) *') | [:REAL,(BoundedLinearFunctionals (RUSp2RNSp X)):] by LM6, A0
.= the Mult of (DualSp (RUSp2RNSp X)) by DUALSP01:17, RSSPACE:def 9 ;
the normF of (DualSp X) = the normF of (DualSp (RUSp2RNSp X)) by LM9;
hence DualSp X = DualSp (RUSp2RNSp X) by A2, A3, A4; :: thesis: verum