theorem :: GROUP_1:25

for G being Group
for h being Element of G holds h |^ 0 = 1_ G by Def7;