dom f = A by Th19;
then A1: f . a in rng f by FUNCT_1:def 3;
rng f c= H₃(G) by Th19;
hence f . a is Element of G by A1; :: thesis: verum