let O be set ; :: thesis: for G being GroupWithOperators of O

for N being normal StableSubgroup of G holds 1_ (G ./. N) = carr N

let G be GroupWithOperators of O; :: thesis: for N being normal StableSubgroup of G holds 1_ (G ./. N) = carr N

let N be normal StableSubgroup of G; :: thesis: 1_ (G ./. N) = carr N

reconsider N9 = multMagma(# the carrier of N, the multF of N #) as normal Subgroup of G by Lm6;

1_ (G ./. N9) = carr N9 by GROUP_6:24;

hence 1_ (G ./. N) = carr N by Lm34; :: thesis: verum

for N being normal StableSubgroup of G holds 1_ (G ./. N) = carr N

let G be GroupWithOperators of O; :: thesis: for N being normal StableSubgroup of G holds 1_ (G ./. N) = carr N

let N be normal StableSubgroup of G; :: thesis: 1_ (G ./. N) = carr N

reconsider N9 = multMagma(# the carrier of N, the multF of N #) as normal Subgroup of G by Lm6;

1_ (G ./. N9) = carr N9 by GROUP_6:24;

hence 1_ (G ./. N) = carr N by Lm34; :: thesis: verum