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) |^ |.i.| or ( (1_ G) |^ i = ((1_ G) |^ |.i.|) " & (1_ G) " = 1_ G ) ) by Def8, Th8;
hence (1_ G) |^ i = 1_ G by Lm4; :: thesis: verum