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

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