let G be addGroup; :: thesis: for a being Element of G
for A being Subset of G holds
( (A * a) * (- a) = A & (A * (- a)) * a = A )
let a be Element of G; :: thesis: for A being Subset of G holds
( (A * a) * (- a) = A & (A * (- a)) * a = A )
let A be Subset of G; :: thesis: ( (A * a) * (- a) = A & (A * (- a)) * a = A )
thus (A * a) * (- a) = A * (a + (- a)) by Th47
.= A * (0_ G) by Def5
.= A by ThB52 ; :: thesis: (A * (- a)) * a = A
thus (A * (- a)) * a = A * ((- a) + a) by Th47
.= A * (0_ G) by Def5
.= A by ThB52 ; :: thesis: verum