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