reconsider G0 = G, F0 = F as RealLinearSpace ;
RLSStruct(# the carrier of [:G,F:], the ZeroF of [:G,F:], the addF of [:G,F:], the Mult of [:G,F:] #) = [:G0,F0:]
;
hence
( [:G,F:] is strict & [:G,F:] is reflexive & [:G,F:] is discerning & [:G,F:] is RealNormSpace-like & [:G,F:] is scalar-distributive & [:G,F:] is vector-distributive & [:G,F:] is scalar-associative & [:G,F:] is scalar-unital & [:G,F:] is Abelian & [:G,F:] is add-associative & [:G,F:] is right_zeroed & [:G,F:] is right_complementable )
by RSSPACE3:2; verum