let G be Group; :: thesis: for N being normal Subgroup of G holds multMagma(# the carrier of N, the multF of N #) is strict normal Subgroup of G
let N be normal Subgroup of G; :: thesis: multMagma(# the carrier of N, the multF of N #) is strict normal Subgroup of G
reconsider N0 = multMagma(# the carrier of N, the multF of N #) as strict Subgroup of G by Th1;
for g being Element of G holds N0 |^ g = N0

proof

let g be Element of G; :: thesis: N0 |^ g = N0
B2: N |^ g = multMagma(# the carrier of N, the multF of N #) by GROUP_3:def 13;
carr N = carr N0 ;
then the carrier of (N0 |^ g) = (carr N) |^ g by GROUP_3:def 6
.= the carrier of N0 by B2, GROUP_3:def 6 ;
hence N0 |^ g = N0 by GROUP_2:59; :: thesis: verum

end;

hence multMagma(# the carrier of N, the multF of N #) is strict normal Subgroup of G by GROUP_3:def 13; :: thesis: verum