let V be RealLinearSpace; :: thesis: 0. (V *') = the carrier of V --> 0
consider Y being VectSp of F_Real such that
AS1: ( Y = RLSp2RVSp V & V *' = RVSp2RLSp (Y *') ) by def2;
0. (V *') = 0. (Y *') by AS1
.= 0Functional Y by HAHNBAN1:def 10
.= ([#] Y) --> (0. F_Real) by HAHNBAN1:def 7 ;
hence 0. (V *') = the carrier of V --> 0 by AS1; :: thesis: verum