let G, H be strict Group; :: thesis: Ker (1: G,H) = G

now

let a be Element of G; :: thesis: a in Ker (1: G,H)
(1: G,H) . a = 1_ H by Def8;
hence a in Ker (1: G,H) by Th50; :: thesis: verum

end;

hence Ker (1: G,H) = G by GROUP_2:71; :: thesis: verum