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