let G be Group; :: thesis: for a being Element of G
for A being Subset of G
for H being Subgroup of G holds (H * a) * A = H * (a * A)
let a be Element of G; :: thesis: for A being Subset of G
for H being Subgroup of G holds (H * a) * A = H * (a * A)
let A be Subset of G; :: thesis: for H being Subgroup of G holds (H * a) * A = H * (a * A)
let H be Subgroup of G; :: thesis: (H * a) * A = H * (a * A)
thus (H * a) * A = (H * {a}) * A
.= H * (a * A) by GROUP_2:118 ; :: thesis: verum