for G being Group
for a being Element of G
for H being Subgroup of G holds H * (a |^ 2) c= (H * a) * (H * a)