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