g . i in rng g by FUNCT_1:def 3;
hence g . i is AbGroup by Def11; :: thesis: verum