now

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

end;

hence Ker g is normal by Def10; :: thesis: verum