let O be set ; :: thesis: for G being GroupWithOperators of O
for N being normal StableSubgroup of G holds multMagma(# the carrier of N, the multF of N #) is strict normal Subgroup of G
let G be GroupWithOperators of O; :: thesis: for N being normal StableSubgroup of G holds multMagma(# the carrier of N, the multF of N #) is strict normal Subgroup of G
let N be normal StableSubgroup of G; :: thesis: multMagma(# the carrier of N, the multF of N #) is strict normal Subgroup of G
set H = multMagma(# the carrier of N, the multF of N #);
reconsider H = multMagma(# the carrier of N, the multF of N #) as non empty multMagma ;
reconsider H = H as non empty Group-like multMagma ;
N is Subgroup of G by Def7;
then ( the carrier of H c= the carrier of G & the multF of H = the multF of G || the carrier of H ) by GROUP_2:def 5;
then reconsider H = H as Subgroup of G by GROUP_2:def 5;
H is normal by Def10;
hence multMagma(# the carrier of N, the multF of N #) is strict normal Subgroup of G ; :: thesis: verum