let G be Group; :: thesis: for a being Element of G
for H1, H2 being Subgroup of G holds (a * H1) * H2 = a * (H1 * H2)
let a be Element 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 * ((carr H1) * H2) by GROUP_2:96
.= a * (H1 * H2) ; :: thesis: verum