let G be Group; :: thesis: for a being Element of G
for H being Subgroup of G holds
( card H = card (a * H) & card H = card (H * a) )
let a be Element of G; :: thesis: for H being Subgroup of G holds
( card H = card (a * H) & card H = card (H * a) )
let H be Subgroup of G; :: thesis: ( card H = card (a * H) & card H = card (H * a) )
carr H,a * H are_equipotent by Th154;
hence card H = card (a * H) by CARD_1:21; :: thesis: card H = card (H * a)
carr H,H * a are_equipotent by Th154;
hence card H = card (H * a) by CARD_1:21; :: thesis: verum