let i be Integer; :: thesis: for G being addGroup
for g, h being Element of G st g + h = h + g holds
g + (i * h) = (i * h) + g
let G be addGroup; :: thesis: for g, h being Element of G st g + h = h + g holds
g + (i * h) = (i * h) + g
let g, h be Element of G; :: thesis: ( g + h = h + g implies g + (i * h) = (i * h) + g )
assume A1: g + h = h + g ; :: thesis: g + (i * h) = (i * h) + g
thus g + (i * h) = (1 * g) + (i * h) by Th25
.= (i * h) + (1 * g) by A1, Th38
.= (i * h) + g by Th25 ; :: thesis: verum