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 (H |^ a) by Th64;
then the carrier of H, the carrier of (H |^ a) are_equipotent by CARD_1:5;
hence ( H is finite iff H |^ a is finite ) by CARD_1:38; :: thesis: verum