theorem :: GROUP_6:42

for G, H being strict Group holds Ker (1: (G,H)) = G