let G be Group; :: thesis: for a being Element of G
for H being Subgroup of G holds (a |^ 2) * H c= (a * H) * (a * H)
let a be Element of G; :: thesis: for H being Subgroup of G holds (a |^ 2) * H c= (a * H) * (a * H)
let H be Subgroup of G; :: thesis: (a |^ 2) * H c= (a * H) * (a * H)
(a |^ 2) * H = (a * a) * H by GROUP_1:27;
hence (a |^ 2) * H c= (a * H) * (a * H) by Th116; :: thesis: verum