let G be Group; :: thesis: for A being Subset of G
for H1, H2 being Subgroup of G holds (H1 * H2) * A = H1 * (H2 * A)
let A be Subset of G; :: thesis: for H1, H2 being Subgroup of G holds (H1 * H2) * A = H1 * (H2 * A)
let H1, H2 be Subgroup of G; :: thesis: (H1 * H2) * A = H1 * (H2 * A)
thus (H1 * H2) * A = (H1 * (carr H2)) * A
.= H1 * (H2 * A) by GROUP_2:98 ; :: thesis: verum