let G be Group; :: thesis: for a, b being Element of G
for H being Subgroup of G holds (H |^ a) |^ b = H |^ (a * b)
let a, b be Element of G; :: thesis: for H being Subgroup of G holds (H |^ a) |^ b = H |^ (a * b)
let H be Subgroup of G; :: thesis: (H |^ a) |^ b = H |^ (a * b)
the carrier of ((H |^ a) |^ b) = (carr (H |^ a)) |^ b by Def6
.= ((carr H) |^ a) |^ b by Def6
.= (carr H) |^ (a * b) by Th47
.= the carrier of (H |^ (a * b)) by Def6 ;
hence (H |^ a) |^ b = H |^ (a * b) by GROUP_2:59; :: thesis: verum