let G be addGroup; :: thesis: for a, b being Element of G
for i being Integer holds (i * a) * b = i * (a * b)
let a, b be Element of G; :: thesis: for i being Integer holds (i * a) * b = i * (a * b)
let i be Integer; :: thesis: (i * a) * b = i * (a * b)

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

suppose i >= 0 ; :: thesis: (i * a) * b = i * (a * b)

then i = |.i.| by ABSVALUE:def 1;
hence (i * a) * b = i * (a * b) by Lm4; :: thesis: verum

end;

suppose A1: i < 0 ; :: thesis: (i * a) * b = i * (a * b)

hence (i * a) * b = (- (|.i.| * a)) * b by Th29
.= - ((|.i.| * a) * b) by Th26
.= - (|.i.| * (a * b)) by Lm4
.= i * (a * b) by A1, Th29 ;
:: thesis: verum

end;

end;