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

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