let G be Group; :: thesis: for a being Element of G

for H being Subgroup of G holds

( carr H c= (a * H) * ((a ") * H) & carr H c= ((a ") * H) * (a * H) )

let a be Element of G; :: thesis: for H being Subgroup of G holds

( carr H c= (a * H) * ((a ") * H) & carr H c= ((a ") * H) * (a * H) )

let H be Subgroup of G; :: thesis: ( carr H c= (a * H) * ((a ") * H) & carr H c= ((a ") * H) * (a * H) )

A1: ((a ") * a) * H = (1_ G) * H by GROUP_1:def 5

.= carr H by Th37 ;

(a * (a ")) * H = (1_ G) * H by GROUP_1:def 5

.= carr H by Th37 ;

hence ( carr H c= (a * H) * ((a ") * H) & carr H c= ((a ") * H) * (a * H) ) by A1, Th116; :: thesis: verum

for H being Subgroup of G holds

( carr H c= (a * H) * ((a ") * H) & carr H c= ((a ") * H) * (a * H) )

let a be Element of G; :: thesis: for H being Subgroup of G holds

( carr H c= (a * H) * ((a ") * H) & carr H c= ((a ") * H) * (a * H) )

let H be Subgroup of G; :: thesis: ( carr H c= (a * H) * ((a ") * H) & carr H c= ((a ") * H) * (a * H) )

A1: ((a ") * a) * H = (1_ G) * H by GROUP_1:def 5

.= carr H by Th37 ;

(a * (a ")) * H = (1_ G) * H by GROUP_1:def 5

.= carr H by Th37 ;

hence ( carr H c= (a * H) * ((a ") * H) & carr H c= ((a ") * H) * (a * H) ) by A1, Th116; :: thesis: verum