for G being Group
for h being Element of G holds h |^ 2 = h * h