let p be prime Nat; :: thesis: for G being finite strict Group st G is p -group & expon (G,p) = 0 holds
G = (1). G
let G be finite strict Group; :: thesis: ( G is p -group & expon (G,p) = 0 implies G = (1). G )
assume ( G is p -group & expon (G,p) = 0 ) ; :: thesis: G = (1). G
then A1: card G = p |^ 0 by Def2
.= 1 by NEWTON:4 ;
card ((1). G) = 1 by GROUP_2:69;
hence G = (1). G by A1, GROUP_2:73; :: thesis: verum