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