for G being Group
for g being Element of G
for H being Subgroup of G
for h being Element of H st h = g holds
h " = g "