let G be addGroup; :: thesis: for a, b being Element of G holds
( (a * b) * (- b) = a & (a * (- b)) * b = a )
let a, b be Element of G; :: thesis: ( (a * b) * (- b) = a & (a * (- b)) * b = a )
thus (a * b) * (- b) = a * (b + (- b)) by Th24
.= a * (0_ G) by Def5
.= a by Th19 ; :: thesis: (a * (- b)) * b = a
thus (a * (- b)) * b = a * ((- b) + b) by Th24
.= a * (0_ G) by Def5
.= a by Th19 ; :: thesis: verum