let G be Group; :: thesis: for a being Element of G
for H being Subgroup of G holds
( H is finite iff H |^ a is finite )
let a be Element of G; :: thesis: for H being Subgroup of G holds
( H is finite iff H |^ a is finite )
let H be Subgroup of G; :: thesis: ( H is finite iff H |^ a is finite )
( card H = card the carrier of H & card H = card (H |^ a) & card (H |^ a) = card the carrier of (H |^ a) ) by Th77;
then the carrier of H,the carrier of (H |^ a) are_equipotent by CARD_1:21;
then ( the carrier of H is finite iff the carrier of (H |^ a) is finite ) by CARD_1:68;
hence ( H is finite iff H |^ a is finite ) ; :: thesis: verum