let G be addGroup; :: thesis: for a being Element of G
for H being Subgroup of G holds
( carr H c= (H + a) + (H + (- a)) & carr H c= (H + (- a)) + (H + a) )
let a be Element of G; :: thesis: for H being Subgroup of G holds
( carr H c= (H + a) + (H + (- a)) & carr H c= (H + (- a)) + (H + a) )
let H be Subgroup of G; :: thesis: ( carr H c= (H + a) + (H + (- a)) & carr H c= (H + (- a)) + (H + a) )
A1: (H + (- a)) + a = H + ((- a) + a) by ThB34
.= H + (0_ G) by Def5
.= carr H by Th37 ;
(H + a) + (- a) = H + (a + (- a)) by ThB34
.= H + (0_ G) by Def5
.= carr H by Th37 ;
hence ( carr H c= (H + a) + (H + (- a)) & carr H c= (H + (- a)) + (H + a) ) by A1, Th122; :: thesis: verum