let G be Group; :: thesis: for a being Element of G
for H being Subgroup of G holds
( carr H,a * H are_equipotent & carr H,H * a are_equipotent )
let a be Element of G; :: thesis: for H being Subgroup of G holds
( carr H,a * H are_equipotent & carr H,H * a are_equipotent )
let H be Subgroup of G; :: thesis: ( carr H,a * H are_equipotent & carr H,H * a are_equipotent )
( carr H = (1_ G) * H & carr H = H * (1_ G) ) by Th37;
hence ( carr H,a * H are_equipotent & carr H,H * a are_equipotent ) by Th128, Th130; :: thesis: verum