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

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