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:10
.= (a * (N1 * b)) * N2 by GROUP_2:29
.= (a * (b * N1)) * N2 by GROUP_3:117
.= ((a * b) * N1) * N2 by GROUP_2:105
.= (a * b) * (N1 * N2) by GROUP_4:45 ;
hence (a * N1) * (b * N2) = (a * b) * N by A1; :: thesis: verum