G . j in rng G by FUNCT_1:def 3;
hence G . j is RealNormSpace by Def10; :: thesis: verum