let G be Group; :: thesis: for N being normal Subgroup of G holds 1_ (G ./. N) = carr N
let N be normal Subgroup of G; :: thesis: 1_ (G ./. N) = carr N
reconsider e = carr N as Element of (G ./. N) by GROUP_2:135;

now :: thesis: for h being Element of (G ./. N) holds
( h * e = h & e * h = h )

let h be Element of (G ./. N); :: thesis: ( h * e = h & e * h = h )
consider a being Element of G such that
A1: h = a * N and
A2: h = N * a by Th13;
thus h * e = (a * N) * N by A1, Def3
.= a * (N * N) by GROUP_4:45
.= h by A1, GROUP_2:76 ; :: thesis: e * h = h
thus e * h = N * (N * a) by A2, Def3
.= (N * N) * a by GROUP_4:46
.= h by A2, GROUP_2:76 ; :: thesis: verum

end;

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