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