let G be Group; :: thesis: for a, b being Element of G
for H being Subgroup of G holds H * a,H * b are_equipotent
let a, b be Element of G; :: thesis: for H being Subgroup of G holds H * a,H * b are_equipotent
let H be Subgroup of G; :: thesis: H * a,H * b are_equipotent
( H * a,b * H are_equipotent & b * H,H * b are_equipotent ) by Th129;
hence H * a,H * b are_equipotent by WELLORD2:15; :: thesis: verum