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 Th40
.= H * (1_ G) by GROUP_1:def 6
.= carr H by Th43 ;
(H * a) * (a ") = H * (a * (a ")) by Th40
.= H * (1_ G) by GROUP_1:def 6
.= carr H by Th43 ;
hence ( carr H c= (H * a) * (H * (a ")) & carr H c= (H * (a ")) * (H * a) ) by A1, Th145; :: thesis: verum