now :: thesis: for N being strict Subgroup of G st N = multMagma(# the carrier of (Ker g), the multF of (Ker g) #) holds

N is normal

hence
Ker g is normal
; :: thesis: verumN is normal

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

end;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