let G be addGroup; :: 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;
hence ( H is finite iff H * a is finite ) ; :: thesis: verum