g . i in rng g by FUNCT_1:def 3;
hence g . i is non empty addLoopStr by DefAA; :: thesis: verum