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

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

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

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

end;

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

A3: (|.i.| * g) + (|.j.| * h) = (|.j.| * h) + (|.i.| * g) by A1, Lm10;
( i * g = |.i.| * g & j * h = - (|.j.| * h) ) by A2, Def8;
hence (i * g) + (j * h) = (j * h) + (i * g) by A3, Th19; :: thesis: verum

end;

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

A5: (|.i.| * g) + (|.j.| * h) = (|.j.| * h) + (|.i.| * g) by A1, Lm10;
( i * g = - (|.i.| * g) & j * h = |.j.| * h ) by A4, Def8;
hence (i * g) + (j * h) = (j * h) + (i * g) by A5, Th19; :: thesis: verum

end;

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

then A6: ( i * g = - (|.i.| * g) & j * h = - (|.j.| * h) ) by Def8;
hence (i * g) + (j * h) = - ((|.j.| * h) + (|.i.| * g)) by Th16
.= - ((|.i.| * g) + (|.j.| * h)) by A1, Lm10
.= (j * h) + (i * g) by A6, Th16 ;
:: thesis: verum

end;

end;