let G be addGroup; :: thesis: for a being Element of G
for H being strict Subgroup of G holds
( (H * a) * (- a) = H & (H * (- a)) * a = H )
let a be Element of G; :: thesis: for H being strict Subgroup of G holds
( (H * a) * (- a) = H & (H * (- a)) * a = H )
let H be strict Subgroup of G; :: thesis: ( (H * a) * (- a) = H & (H * (- a)) * a = H )
thus (H * a) * (- a) = H * (a + (- a)) by Th60
.= H * (0_ G) by Def5
.= H by Th61 ; :: thesis: (H * (- a)) * a = H
thus (H * (- a)) * a = H * ((- a) + a) by Th60
.= H * (0_ G) by Def5
.= H by Th61 ; :: thesis: verum