let G be finite Group; for a being Element of G
for n, p, s being Element of NAT st card (gr {a}) = n & n = p * s holds
ord (a |^ p) = s
let a be Element of G; for n, p, s being Element of NAT st card (gr {a}) = n & n = p * s holds
ord (a |^ p) = s
let n, p, s be Element of NAT ; ( card (gr {a}) = n & n = p * s implies ord (a |^ p) = s )
assume AS1:
( card (gr {a}) = n & n = p * s )
; ord (a |^ p) = s
reconsider a0 = a as Element of (gr {a}) by GR_CY_2:2, STRUCT_0:def 5;
A0:
gr {a0} = gr {a}
by GR_CY_2:3;
ord (a0 |^ p) =
card (gr {(a0 |^ p)})
by GR_CY_1:7
.=
card (gr {(a |^ p)})
by GROUP_4:2, GR_CY_2:3
.=
ord (a |^ p)
by GR_CY_1:7
;
hence
ord (a |^ p) = s
by A0, AS1, GR_CY_2:8; verum