reconsider X = RLSp2RVSp V as VectSp of F_Real ;
RVSp2RLSp (X *') is RealLinearSpace
;
hence
( ex b1 being strict RealLinearSpace ex X being VectSp of F_Real st
( X = RLSp2RVSp V & b1 = RVSp2RLSp (X *') ) & ( for b1, b2 being strict RealLinearSpace st ex X being VectSp of F_Real st
( X = RLSp2RVSp V & b1 = RVSp2RLSp (X *') ) & ex X being VectSp of F_Real st
( X = RLSp2RVSp V & b2 = RVSp2RLSp (X *') ) holds
b1 = b2 ) )
; verum