let k, s be Element of NAT ; :: thesis: for G being finite Group
for a being Element of G st card (gr {(a |^ s)}) = card (gr {(a |^ k)}) & a |^ k in gr {(a |^ s)} holds
gr {(a |^ s)} = gr {(a |^ k)}
let G be finite Group; :: thesis: for a being Element of G st card (gr {(a |^ s)}) = card (gr {(a |^ k)}) & a |^ k in gr {(a |^ s)} holds
gr {(a |^ s)} = gr {(a |^ k)}
let a be Element of G; :: thesis: ( card (gr {(a |^ s)}) = card (gr {(a |^ k)}) & a |^ k in gr {(a |^ s)} implies gr {(a |^ s)} = gr {(a |^ k)} )
assume A1: card (gr {(a |^ s)}) = card (gr {(a |^ k)}) ; :: thesis: ( not a |^ k in gr {(a |^ s)} or gr {(a |^ s)} = gr {(a |^ k)} )
assume a |^ k in gr {(a |^ s)} ; :: thesis: gr {(a |^ s)} = gr {(a |^ k)}
then reconsider h = a |^ k as Element of (gr {(a |^ s)}) by STRUCT_0:def 5;
card (gr {h}) = card (gr {(a |^ s)}) by A1, Th3;
hence gr {(a |^ s)} = gr {h} by GROUP_2:73
.= gr {(a |^ k)} by Th3 ;
:: thesis: verum