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