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

now :: thesis: for a being Element of G holds a in Ker (1: (G,H))

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

end;

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