let i be Integer; :: thesis: for G being Group holds (1_ G) |^ i = 1_ G
let G be Group; :: thesis: (1_ G) |^ i = 1_ G
( (1_ G) |^ i = (1_ G) |^ (abs i) or ( (1_ G) |^ i = ((1_ G) |^ (abs i)) " & (1_ G) " = 1_ G ) ) by Def9, Th16;
hence (1_ G) |^ i = 1_ G by Lm4; :: thesis: verum