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 * a) * H = A * (a * H)
let a be Element of G; :: thesis: for A being Subset of G
for H being Subgroup of G holds (A * a) * H = A * (a * H)
let A be Subset of G; :: thesis: for H being Subgroup of G holds (A * a) * H = A * (a * H)
let H be Subgroup of G; :: thesis: (A * a) * H = A * (a * H)
thus (A * a) * H = A * ({a} * H) by GROUP_2:96
.= A * (a * H) ; :: thesis: verum