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; :: thesis: verum