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

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