G . j in rng G by FUNCT_1:def 5;
hence G . j is RealLinearSpace by Def3; :: thesis: verum