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

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