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