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

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