let G be Group; :: thesis: for N, N1, N2 being normal Subgroup of G
for a, b being Element of G st the carrier of N = N1 * N2 holds
(a * N1) * (b * N2) = (a * b) * N
let N, N1, N2 be normal Subgroup of G; :: thesis: for a, b being Element of G st the carrier of N = N1 * N2 holds
(a * N1) * (b * N2) = (a * b) * N
let a, b be Element of G; :: thesis: ( the carrier of N = N1 * N2 implies (a * N1) * (b * N2) = (a * b) * N )
assume A1: the carrier of N = N1 * N2 ; :: thesis: (a * N1) * (b * N2) = (a * b) * N
(a * N1) * (b * N2) = ((a * N1) * b) * N2 by GROUP_2:14
.= (a * (N1 * b)) * N2 by GROUP_2:35
.= (a * (b * N1)) * N2 by GROUP_3:140
.= ((a * b) * N1) * N2 by GROUP_2:127
.= (a * b) * (N1 * N2) by GROUP_4:60 ;
hence (a * N1) * (b * N2) = (a * b) * N by A1; :: thesis: verum