reconsider G9 = G, H9 = H as Group ;
let N be strict Subgroup of G; :: thesis: ( N = multMagma(# the carrier of (Ker g), the multF of (Ker g) #) implies N is normal )
reconsider g9 = g as Homomorphism of G9,H9 ;
A1: the carrier of (Ker g9) = { a where a is Element of G : g . a = 1_ H } by GROUP_6:def 9;
assume N = multMagma(# the carrier of (Ker g), the multF of (Ker g) #) ; :: thesis: N is normal
then the carrier of (Ker g9) = the carrier of N by A1, Def21;
hence N is normal by GROUP_2:59; :: thesis: verum