let G be Group; :: 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 Th34
.= H * (1_ G) by GROUP_1:def 5
.= carr H by Th37 ;
(H * a) * (a ") = H * (a * (a ")) by Th34
.= H * (1_ G) by GROUP_1:def 5
.= carr H by Th37 ;
hence ( carr H c= (H * a) * (H * (a ")) & carr H c= (H * (a ")) * (H * a) ) by A1, Th122; :: thesis: verum