let G be Group; :: thesis: for a being Element of G
for H being finite Subgroup of G ex B, C being finite set st
( B = a * H & C = H * a & card H = card B & card H = card C )
let a be Element of G; :: thesis: for H being finite Subgroup of G ex B, C being finite set st
( B = a * H & C = H * a & card H = card B & card H = card C )
let H be finite Subgroup of G; :: thesis: ex B, C being finite set st
( B = a * H & C = H * a & card H = card B & card H = card C )
reconsider B = a * H, C = H * a as finite set by Th131, CARD_1:38;
take B ; :: thesis: ex C being finite set st
( B = a * H & C = H * a & card H = card B & card H = card C )
take C ; :: thesis: ( B = a * H & C = H * a & card H = card B & card H = card C )
( carr H,a * H are_equipotent & carr H,H * a are_equipotent ) by Th131;
hence ( B = a * H & C = H * a & card H = card B & card H = card C ) by CARD_1:5; :: thesis: verum