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

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