let i be Integer; :: thesis: for G being addGroup holds i * (0_ G) = 0_ G
let G be addGroup; :: thesis: i * (0_ G) = 0_ G
( i * (0_ G) = |.i.| * (0_ G) or ( i * (0_ G) = - (|.i.| * (0_ G)) & - (0_ G) = 0_ G ) ) by Def8, Th8;
hence i * (0_ G) = 0_ G by Lm4; :: thesis: verum