let G be addGroup; :: 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 = (0_ G) + H & carr H = H + (0_ G) ) by Th37;
hence ( carr H,a + H are_equipotent & carr H,H + a are_equipotent ) by Th128, Th130; :: thesis: verum