let i be Integer; :: thesis: for G being addGroup
for g, h being Element of G st g + h = h + g holds
i * (g + h) = (i * g) + (i * h)
let G be addGroup; :: thesis: for g, h being Element of G st g + h = h + g holds
i * (g + h) = (i * g) + (i * h)
let g, h be Element of G; :: thesis: ( g + h = h + g implies i * (g + h) = (i * g) + (i * h) )
assume A1: g + h = h + g ; :: thesis: i * (g + h) = (i * g) + (i * h)

per cases ( i >= 0 or i < 0 ) ;

suppose A2: i >= 0 ; :: thesis: i * (g + h) = (i * g) + (i * h)

then A3: i * h = |.i.| * h by Def8;
( i * (g + h) = |.i.| * (g + h) & i * g = |.i.| * g ) by A2, Def8;
hence i * (g + h) = (i * g) + (i * h) by A1, A3, Lm11; :: thesis: verum

end;

suppose A4: i < 0 ; :: thesis: i * (g + h) = (i * g) + (i * h)

hence i * (g + h) = - (|.i.| * (h + g)) by A1, Def8
.= - ((|.i.| * h) + (|.i.| * g)) by A1, Lm11
.= (- (|.i.| * g)) + (- (|.i.| * h)) by Th16
.= (i * g) + (- (|.i.| * h)) by A4, Def8
.= (i * g) + (i * h) by A4, Def8 ;
:: thesis: verum

end;

end;