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