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