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

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