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

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