let G be Group; :: thesis: for N being normal Subgroup of G
for x1, x2 being Element of G holds (x1 * N) * (x2 * N) = (x1 * x2) * N
let N be normal Subgroup of G; :: thesis: for x1, x2 being Element of G holds (x1 * N) * (x2 * N) = (x1 * x2) * N
let x1, x2 be Element of G; :: thesis: (x1 * N) * (x2 * N) = (x1 * x2) * N
(x1 * N) * (x2 * N) = ((x1 * N) * x2) * N by GROUP_2:10
.= (x1 * (N * x2)) * N by GROUP_2:29
.= (x1 * (x2 * N)) * N by GROUP_3:117
.= ((x1 * x2) * N) * N by GROUP_2:105
.= (x1 * x2) * (N * N) by GROUP_2:29 ;
hence (x1 * N) * (x2 * N) = (x1 * x2) * N by GROUP_2:76; :: thesis: verum