let X be RealUnitarySpace; :: thesis: X *' = (RUSp2RNSp X) *'
set Y = RUSp2RNSp X;
the carrier of (X *') = the carrier of ((RUSp2RNSp X) *') by LM10A;
hence X *' = (RUSp2RNSp X) *' ; :: thesis: verum