let p be prime Nat; :: thesis: for G being finite strict Group st G is p -group & expon (G,p) = 0 holds
G is p -commutative-group
let G be finite strict Group; :: thesis: ( G is p -group & expon (G,p) = 0 implies G is p -commutative-group )
assume A1: ( G is p -group & expon (G,p) = 0 ) ; :: thesis: G is p -commutative-group
then G = (1). G by Th24;
hence G is p -commutative-group by A1; :: thesis: verum