groupp_1.miz



    begin

    reserve G for Group,

a,b for Element of G,

m,n for Nat,

p for prime Nat;

    theorem :: GROUPP_1:1

    

     Th1: (for r be Nat holds n <> (p |^ r)) implies ex s be Element of NAT st s is prime & s divides n & s <> p

    proof

      assume

       A1: for r be Nat holds n <> (p |^ r);

      per cases ;

        suppose

         A2: n = 0 ;

        per cases ;

          suppose

           A3: p = 2;

          take s = 3;

          thus s is prime by PEPIN: 41;

          thus s divides n by A2, INT_2: 12;

          thus s <> p by A3;

        end;

          suppose

           A4: p <> 2;

          take s = 2;

          thus s is prime by INT_2: 28;

          thus s divides n by A2, INT_2: 12;

          thus s <> p by A4;

        end;

      end;

        suppose

         A5: n <> 0 ;

        

         A6: p > 1 by INT_2:def 4;

        reconsider r1 = (p |-count n) as Element of NAT ;

        

         A7: (p |^ r1) divides n by A5, A6, NAT_3:def 7;

        

         A8: not (p |^ (r1 + 1)) divides n by A5, A6, NAT_3:def 7;

        consider s1 be Nat such that

         A9: n = ((p |^ r1) * s1) by A7, NAT_D:def 3;

        s1 >= 2

        proof

          assume not s1 >= 2;

          then s1 < (1 + 1);

          then s1 <= 1 by NAT_1: 13;

          then s1 = 0 or s1 = 1 by NAT_1: 25;

          hence contradiction by A5, A1, A9;

        end;

        then

        consider s be Element of NAT such that

         A10: s is prime and

         A11: s divides s1 by INT_2: 31;

        

         A12: s1 divides n by A9, NAT_D:def 3;

        take s;

        s <> p

        proof

          assume s = p;

          then

          consider s2 be Nat such that

           A13: s1 = (p * s2) by A11, NAT_D:def 3;

          n = (((p |^ r1) * p) * s2) by A9, A13

          .= ((p |^ (r1 + 1)) * s2) by NEWTON: 6;

          hence contradiction by A8, NAT_D:def 3;

        end;

        hence thesis by A10, A11, A12, NAT_D: 4;

      end;

    end;

    theorem :: GROUPP_1:2

    

     Th2: for n,m be Nat holds n divides (p |^ m) implies ex r be Nat st n = (p |^ r) & r <= m

    proof

      let n,m be Nat;

      assume

       A1: n divides (p |^ m);

      n > 0

      proof

        assume n <= 0 ;

        then n = 0 ;

        hence contradiction by A1, INT_2: 3;

      end;

      then n in ( NatDivisors (p |^ m)) by A1, MOEBIUS1: 39;

      then n in { (p |^ k) where k be Element of NAT : k <= m } by NAT_5: 19;

      then

      consider r be Element of NAT such that

       A2: n = (p |^ r) & r <= m;

      take r;

      thus thesis by A2;

    end;

    theorem :: GROUPP_1:3

    

     Th3: (a |^ n) = ( 1_ G) implies ((a " ) |^ n) = ( 1_ G)

    proof

      assume (a |^ n) = ( 1_ G);

      

      then ((a " ) |^ n) = (( 1_ G) " ) by GROUP_1: 37

      .= ( 1_ G) by GROUP_1: 8;

      hence thesis;

    end;

    theorem :: GROUPP_1:4

    

     Th4: ((a " ) |^ n) = ( 1_ G) implies (a |^ n) = ( 1_ G)

    proof

      ((a " ) " ) = a;

      hence thesis by Th3;

    end;

    theorem :: GROUPP_1:5

    

     Th5: ( ord (a " )) = ( ord a)

    proof

      (a |^ ( ord a)) = ( 1_ G) by GROUP_1: 41;

      then ((a " ) |^ ( ord a)) = ( 1_ G) by Th3;

      then

       A1: ( ord (a " )) divides ( ord a) by GROUP_1: 44;

      ((a " ) |^ ( ord (a " ))) = ( 1_ G) by GROUP_1: 41;

      then (a |^ ( ord (a " ))) = ( 1_ G) by Th4;

      then ( ord a) divides ( ord (a " )) by GROUP_1: 44;

      hence thesis by A1, NAT_D: 5;

    end;

    theorem :: GROUPP_1:6

    

     Th6: ( ord (a |^ b)) = ( ord a)

    proof

      ((a |^ b) |^ ( ord a)) = ((a |^ ( ord a)) |^ b) by GROUP_3: 27

      .= (( 1_ G) |^ b) by GROUP_1: 41

      .= ( 1_ G) by GROUP_3: 17;

      then

       A1: ( ord (a |^ b)) divides ( ord a) by GROUP_1: 44;

      ((a |^ ( ord (a |^ b))) |^ b) = ((a |^ b) |^ ( ord (a |^ b))) by GROUP_3: 27

      .= ( 1_ G) by GROUP_1: 41;

      then ( ord a) divides ( ord (a |^ b)) by GROUP_1: 44, GROUP_3: 18;

      hence thesis by A1, NAT_D: 5;

    end;

    theorem :: GROUPP_1:7

    

     Th7: for G be Group, N be Subgroup of G holds for a,b be Element of G holds N is normal & b in N implies for n holds ex g be Element of G st g in N & ((a * b) |^ n) = ((a |^ n) * g)

    proof

      let G be Group;

      let N be Subgroup of G;

      let a,b be Element of G;

      assume

       A1: N is normal & b in N;

      defpred P[ Nat] means for n holds ex g be Element of G st g in N & ((a * b) |^ $1) = ((a |^ $1) * g);

      

       A2: ((a * b) |^ 0 ) = ( 1_ G) by GROUP_1: 25;

      ((a |^ 0 ) * ( 1_ G)) = (( 1_ G) * ( 1_ G)) by GROUP_1: 25

      .= ( 1_ G) by GROUP_1:def 4;

      then

       A3: P[ 0 ] by A2, GROUP_2: 46;

       A4:

      now

        let n;

        assume P[n];

        then

        consider g1 be Element of G such that

         A5: g1 in N & ((a * b) |^ n) = ((a |^ n) * g1);

        

         A6: ((a * b) |^ (n + 1)) = (((a |^ n) * g1) * (a * b)) by A5, GROUP_1: 34

        .= ((a |^ n) * (g1 * (a * b))) by GROUP_1:def 3

        .= ((a |^ n) * ((g1 * a) * b)) by GROUP_1:def 3;

        (a * N) = (N * a) by A1, GROUP_3: 117;

        then (g1 * a) in (a * N) by A5, GROUP_2: 104;

        then

        consider g2 be Element of G such that

         A7: (g1 * a) = (a * g2) & g2 in N by GROUP_2: 103;

        ((g1 * a) * b) = (a * (g2 * b)) by A7, GROUP_1:def 3;

        

        then ((a |^ n) * ((g1 * a) * b)) = (((a |^ n) * a) * (g2 * b)) by GROUP_1:def 3

        .= ((a |^ (n + 1)) * (g2 * b)) by GROUP_1: 34;

        hence P[(n + 1)] by A1, A6, A7, GROUP_2: 50;

      end;

      for n holds P[n] from NAT_1:sch 2( A3, A4);

      hence thesis;

    end;

    theorem :: GROUPP_1:8

    

     Th8: for G be Group, N be normal Subgroup of G, a be Element of G, S be Element of (G ./. N) holds S = (a * N) implies for n holds (S |^ n) = ((a |^ n) * N)

    proof

      let G be Group;

      let N be normal Subgroup of G;

      let a be Element of G;

      let S be Element of (G ./. N);

      assume

       A1: S = (a * N);

      defpred P[ Nat] means for n holds (S |^ $1) = ((a |^ $1) * N);

      

       A2: (S |^ 0 ) = ( 1_ (G ./. N)) by GROUP_1: 25;

      ((a |^ 0 ) * N) = (( 1_ G) * N) by GROUP_1: 25

      .= ( carr N) by GROUP_2: 109;

      then

       A3: P[ 0 ] by A2, GROUP_6: 24;

       A4:

      now

        let n;

        assume

         A5: P[n];

        (S |^ (n + 1)) = ((S |^ n) * S) by GROUP_1: 34

        .= (( @ (S |^ n)) * ( @ S)) by GROUP_6:def 3

        .= (((a |^ n) * N) * (a * N)) by A1, A5

        .= (((a |^ n) * a) * N) by GROUP_11: 1

        .= ((a |^ (n + 1)) * N) by GROUP_1: 34;

        hence P[(n + 1)];

      end;

      for n holds P[n] from NAT_1:sch 2( A3, A4);

      hence thesis;

    end;

    theorem :: GROUPP_1:9

    

     Th9: for G be Group, H be Subgroup of G, a,b be Element of G holds (a * H) = (b * H) implies ex h be Element of G st a = (b * h) & h in H by GROUP_2: 108, GROUP_2: 103;

    theorem :: GROUPP_1:10

    

     Th10: for G be finite Group, N be normal Subgroup of G holds N is Subgroup of ( center G) & (G ./. N) is cyclic implies G is commutative

    proof

      let G be finite Group;

      let N be normal Subgroup of G;

      assume that

       A1: N is Subgroup of ( center G) and

       A2: (G ./. N) is cyclic;

      reconsider I = (G ./. N) as finite Group;

      consider S be Element of I such that

       A3: for T be Element of I holds ex n be Nat st T = (S |^ n) by A2, GR_CY_1: 18;

      consider a1 be Element of G such that

       A4: S = (a1 * N) & S = (N * a1) by GROUP_6: 21;

      for a,b be Element of G holds (a * b) = (b * a)

      proof

        let a,b be Element of G;

        

         A5: (a * N) is Element of I & (b * N) is Element of I by GROUP_6: 22;

        then

        consider r1 be Nat such that

         A6: (a * N) = (S |^ r1) by A3;

        (a * N) = ((a1 |^ r1) * N) by A4, Th8, A6;

        then

        consider c1 be Element of G such that

         A7: a = ((a1 |^ r1) * c1) & c1 in N by Th9;

        

         A8: c1 in ( center G) by A1, A7, GROUP_2: 40;

        consider r2 be Nat such that

         A9: (b * N) = (S |^ r2) by A3, A5;

        (b * N) = ((a1 |^ r2) * N) by A4, Th8, A9;

        then

        consider c2 be Element of G such that

         A10: b = ((a1 |^ r2) * c2) & c2 in N by Th9;

        

         A11: c2 in ( center G) by A1, A10, GROUP_2: 40;

        (a * b) = ((a1 |^ r1) * (c1 * ((a1 |^ r2) * c2))) by A7, A10, GROUP_1:def 3

        .= ((a1 |^ r1) * (((a1 |^ r2) * c2) * c1)) by A8, GROUP_5: 77

        .= ((a1 |^ r1) * ((a1 |^ r2) * (c2 * c1))) by GROUP_1:def 3

        .= (((a1 |^ r1) * (a1 |^ r2)) * (c2 * c1)) by GROUP_1:def 3

        .= ((a1 |^ (r1 + r2)) * (c2 * c1)) by GROUP_1: 33

        .= (((a1 |^ r2) * (a1 |^ r1)) * (c2 * c1)) by GROUP_1: 33

        .= ((a1 |^ r2) * ((a1 |^ r1) * (c2 * c1))) by GROUP_1:def 3

        .= ((a1 |^ r2) * (((a1 |^ r1) * c2) * c1)) by GROUP_1:def 3

        .= ((a1 |^ r2) * ((c2 * (a1 |^ r1)) * c1)) by A11, GROUP_5: 77

        .= ((a1 |^ r2) * (c2 * ((a1 |^ r1) * c1))) by GROUP_1:def 3

        .= (b * a) by A7, A10, GROUP_1:def 3;

        hence thesis;

      end;

      hence thesis by GROUP_1:def 12;

    end;

    theorem :: GROUPP_1:11

    for G be finite Group, N be normal Subgroup of G holds N = ( center G) & (G ./. N) is cyclic implies G is commutative

    proof

      let G be finite Group;

      let N be normal Subgroup of G;

      assume

       A1: N = ( center G) & (G ./. N) is cyclic;

      then N is Subgroup of ( center G) by GROUP_2: 54;

      hence thesis by A1, Th10;

    end;

    theorem :: GROUPP_1:12

    for G be finite Group, H be Subgroup of G holds ( card H) <> ( card G) implies ex a be Element of G st not a in H

    proof

      let G be finite Group;

      let H be Subgroup of G;

      assume

       A1: ( card H) <> ( card G);

      assume not ex a be Element of G st not a in H;

      then the multMagma of H = the multMagma of G by GROUP_2: 62;

      hence contradiction by A1;

    end;

    definition

      let p be Nat;

      let G be Group;

      let a be Element of G;

      :: GROUPP_1:def1

      attr a is p -power means

      : Def1: ex r be Nat st ( ord a) = (p |^ r);

    end

    theorem :: GROUPP_1:13

    

     Th13: ( 1_ G) is m -power

    proof

      

       A1: ( ord ( 1_ G)) = 1 by GROUP_1: 42;

      (m |^ 0 ) = 1 by NEWTON: 4;

      hence thesis by A1;

    end;

    registration

      let G, m;

      cluster m -power for Element of G;

      existence

      proof

        take ( 1_ G);

        thus thesis by Th13;

      end;

    end

    registration

      let p, G;

      let a be p -power Element of G;

      cluster (a " ) -> p -power;

      coherence

      proof

        consider n be Nat such that

         A1: ( ord a) = (p |^ n) by Def1;

        ( ord (a " )) = (p |^ n) by A1, Th5;

        hence thesis;

      end;

    end

    theorem :: GROUPP_1:14

    (a |^ b) is p -power implies a is p -power

    proof

      assume (a |^ b) is p -power;

      then

      consider r be Nat such that

       A1: ( ord (a |^ b)) = (p |^ r);

      ( ord a) = (p |^ r) by A1, Th6;

      hence thesis;

    end;

    registration

      let p, G, b;

      let a be p -power Element of G;

      cluster (a |^ b) -> p -power;

      coherence

      proof

        consider n be Nat such that

         A1: ( ord a) = (p |^ n) by Def1;

        ( ord (a |^ b)) = (p |^ n) by A1, Th6;

        hence thesis;

      end;

    end

    registration

      let p;

      let G be commutative Group, a,b be p -power Element of G;

      cluster (a * b) -> p -power;

      coherence

      proof

        consider n be Nat such that

         A1: ( ord a) = (p |^ n) by Def1;

        consider m be Nat such that

         A2: ( ord b) = (p |^ m) by Def1;

        

         A3: (a |^ (p |^ (n + m))) = (a |^ ((p |^ n) * (p |^ m))) by NEWTON: 8

        .= ((a |^ (p |^ n)) |^ (p |^ m)) by GROUP_1: 35

        .= (( 1_ G) |^ (p |^ m)) by A1, GROUP_1: 41

        .= ( 1_ G) by GROUP_1: 31;

        (b |^ (p |^ (n + m))) = (b |^ ((p |^ m) * (p |^ n))) by NEWTON: 8

        .= ((b |^ (p |^ m)) |^ (p |^ n)) by GROUP_1: 35

        .= (( 1_ G) |^ (p |^ n)) by A2, GROUP_1: 41

        .= ( 1_ G) by GROUP_1: 31;

        

        then ((a * b) |^ (p |^ (n + m))) = (( 1_ G) * ( 1_ G)) by A3, GROUP_1: 48

        .= ( 1_ G) by GROUP_1:def 4;

        then

        consider r be Nat such that

         A4: ( ord (a * b)) = (p |^ r) & r <= (n + m) by Th2, GROUP_1: 44;

        take r;

        thus thesis by A4;

      end;

    end

    registration

      let p;

      let G be finitep -group Group;

      cluster -> p -power for Element of G;

      coherence

      proof

        let a be Element of G;

        consider m be Nat such that

         A1: ( card G) = (p |^ m) by GROUP_10:def 17;

        ex r be Nat st ( ord a) = (p |^ r) & r <= m by A1, Th2, GR_CY_1: 8;

        hence thesis;

      end;

    end

    theorem :: GROUPP_1:15

    

     Th15: for G be finite Group, H be Subgroup of G holds for a be Element of G st H is p -group & a in H holds a is p -power

    proof

      let G be finite Group;

      let H be Subgroup of G;

      let a be Element of G;

      assume that

       A1: H is p -group and

       A2: a in H;

      a is Element of H by A2;

      then

      consider b be Element of H such that

       A3: b = a;

      consider r be Nat such that

       A4: ( ord b) = (p |^ r) by A1, Def1;

      ( ord a) = (p |^ r) by A3, A4, GROUP_8: 5;

      hence thesis;

    end;

    registration

      let p;

      let G be finitep -group Group;

      cluster -> p -group for Subgroup of G;

      coherence

      proof

        let H be Subgroup of G;

        consider m be Nat such that

         A1: ( card G) = (p |^ m) by GROUP_10:def 17;

        ex r be Nat st ( card H) = (p |^ r) & r <= m by A1, Th2, GROUP_2: 148;

        hence thesis;

      end;

    end

    theorem :: GROUPP_1:16

    

     Th16: ( (1). G) is p -group

    proof

      take 0 ;

      

      thus ( card ( (1). G)) = 1 by GROUP_2: 69

      .= (p |^ 0 ) by NEWTON: 4;

    end;

    registration

      let p;

      let G be Group;

      cluster p -group for Subgroup of G;

      existence

      proof

        take ( (1). G);

        thus thesis by Th16;

      end;

    end

    registration

      let p;

      let G be finite Group, G1 be p -group Subgroup of G, G2 be Subgroup of G;

      cluster (G1 /\ G2) -> p -group;

      coherence

      proof

        reconsider H1 = (G1 /\ G2) as Subgroup of G1 by GROUP_2: 88;

        H1 is p -group;

        hence thesis;

      end;

      cluster (G2 /\ G1) -> p -group;

      coherence ;

    end

    theorem :: GROUPP_1:17

    

     Th17: for G be finite Group st for a be Element of G holds a is p -power holds G is p -group

    proof

      let G be finite Group;

      assume

       A1: for a be Element of G holds a is p -power;

      assume not G is p -group;

      then for r be Nat holds ( card G) <> (p |^ r);

      then

      consider s be Element of NAT such that

       A2: s is prime & s divides ( card G) and

       A3: s <> p by Th1;

      consider b be Element of G such that

       A4: ( ord b) = s by A2, GROUP_10: 11;

      b is p -power by A1;

      then ex r1 be Nat st ( ord b) = (p |^ r1);

      hence contradiction by A2, A4, A3, NAT_3: 6;

    end;

    registration

      let p;

      let G be finitep -group Group, N be normal Subgroup of G;

      cluster (G ./. N) -> p -group;

      coherence

      proof

        consider r be Nat such that

         A1: ( card G) = (p |^ r) by GROUP_10:def 17;

        

         A2: ( card G) = (( card N) * ( index N)) by GROUP_2: 147;

        

         A3: ( card (G ./. N)) = ( index N) by GROUP_6: 27;

        reconsider n = ( card (G ./. N)) as Nat;

        n divides (p |^ r) by A1, A2, A3, NAT_D:def 3;

        then ex r1 be Nat st n = (p |^ r1) & r1 <= r by Th2;

        hence thesis;

      end;

    end

    theorem :: GROUPP_1:18

    for G be finite Group, N be normal Subgroup of G st N is p -group & (G ./. N) is p -group holds G is p -group

    proof

      let G be finite Group;

      let N be normal Subgroup of G;

      assume that

       A1: N is p -group and

       A2: (G ./. N) is p -group;

      consider r1 be Nat such that

       A3: ( card N) = (p |^ r1) by A1;

      consider r2 be Nat such that

       A4: ( card (G ./. N)) = (p |^ r2) by A2;

      ( card (G ./. N)) = ( index N) by GROUP_6: 27;

      

      then ( card G) = ((p |^ r1) * (p |^ r2)) by A3, A4, GROUP_2: 147

      .= (p |^ (r1 + r2)) by NEWTON: 8;

      hence thesis;

    end;

    theorem :: GROUPP_1:19

    

     Th19: for G be finite commutative Group, H,H1,H2 be Subgroup of G st H1 is p -group & H2 is p -group & the carrier of H = (H1 * H2) holds H is p -group

    proof

      let G be finite commutative Group;

      let H,H1,H2 be Subgroup of G;

      assume that

       A1: H1 is p -group & H2 is p -group and

       A2: the carrier of H = (H1 * H2);

      for a be Element of H holds a is p -power

      proof

        let a be Element of H;

        a in (H1 * H2) by A2;

        then

        consider b1,b2 be Element of G such that

         A3: a = (b1 * b2) & b1 in H1 & b2 in H2 by GROUP_11: 6;

        b1 is p -power & b2 is p -power by A1, A3, Th15;

        then

        consider r be Nat such that

         A4: ( ord (b1 * b2)) = (p |^ r) by Def1;

        ( ord a) = (p |^ r) by A3, A4, GROUP_8: 5;

        hence thesis;

      end;

      hence thesis by Th17;

    end;

    theorem :: GROUPP_1:20

    

     Th20: for G be finite Group, H,N be Subgroup of G holds N is normal Subgroup of G & H is p -group & N is p -group implies ex P be strict Subgroup of G st the carrier of P = (H * N) & P is p -group

    proof

      let G be finite Group;

      let H,N be Subgroup of G;

      assume that

       A1: N is normal Subgroup of G and

       A2: H is p -group & N is p -group;

      (H * N) = (N * H) by A1, GROUP_5: 8;

      then

      consider P be strict Subgroup of G such that

       A3: the carrier of P = (H * N) by GROUP_2: 78;

      

       A4: for a be Element of P holds a is p -power

      proof

        let a be Element of P;

        a in (H * N) by A3;

        then

        consider b,c be Element of G such that

         A5: a = (b * c) & b in H & c in N by GROUP_11: 6;

        b is p -power by A5, A2, Th15;

        then

        consider n be Nat such that

         A6: ( ord b) = (p |^ n);

        

         A7: (b |^ (p |^ n)) = ( 1_ G) by A6, GROUP_1: 41;

        consider d be Element of G such that

         A8: d in N & ((b * c) |^ (p |^ n)) = ((b |^ (p |^ n)) * d) by A1, A5, Th7;

        d is p -power by A2, A8, Th15;

        then

        consider m be Nat such that

         A9: ( ord d) = (p |^ m);

        

         A10: (d |^ (p |^ m)) = ( 1_ G) by A9, GROUP_1: 41;

        

         A11: (a |^ (p |^ (n + m))) = ((b * c) |^ (p |^ (n + m))) by A5, GROUP_8: 4

        .= ((b * c) |^ ((p |^ n) * (p |^ m))) by NEWTON: 8

        .= (((b * c) |^ (p |^ n)) |^ (p |^ m)) by GROUP_1: 35

        .= ( 1_ G) by A7, A8, A10, GROUP_1:def 4;

        reconsider a1 = a as Element of G by GROUP_2: 42;

        (a1 |^ (p |^ (n + m))) = ( 1_ G) by A11, GROUP_8: 4;

        then

        consider r be Nat such that

         A12: ( ord a1) = (p |^ r) & r <= (n + m) by Th2, GROUP_1: 44;

        ( ord a) = (p |^ r) by A12, GROUP_8: 5;

        hence thesis;

      end;

      take P;

      thus thesis by A3, A4, Th17;

    end;

    theorem :: GROUPP_1:21

    

     Th21: for G be finite Group, N1,N2 be normal Subgroup of G holds N1 is p -group & N2 is p -group implies ex N be strict normal Subgroup of G st the carrier of N = (N1 * N2) & N is p -group

    proof

      let G be finite Group;

      let N1,N2 be normal Subgroup of G;

      assume N1 is p -group & N2 is p -group;

      then

      consider N be strict Subgroup of G such that

       A1: the carrier of N = (N1 * N2) & N is p -group by Th20;

      for x,y be Element of G st y in N holds ((x * y) * (x " )) in N

      proof

        let x,y be Element of G;

        assume y in N;

        then y in the carrier of N;

        then

        consider a,b be Element of G such that

         A2: y = (a * b) & a in N1 & b in N2 by A1, GROUP_11: 6;

        

         A3: ((x * y) * (x " )) = (((x * a) * b) * (x " )) by A2, GROUP_1:def 3

        .= ((x * a) * (b * (x " ))) by GROUP_1:def 3

        .= (((x * a) * ( 1_ G)) * (b * (x " ))) by GROUP_1:def 4

        .= (((x * a) * ((x " ) * x)) * (b * (x " ))) by GROUP_1:def 5

        .= ((((x * a) * (x " )) * x) * (b * (x " ))) by GROUP_1:def 3

        .= (((x * a) * (x " )) * (x * (b * (x " )))) by GROUP_1:def 3

        .= (((x * a) * (x " )) * ((x * b) * (x " ))) by GROUP_1:def 3;

        ((x * a) * (x " )) in N1 & ((x * b) * (x " )) in N2 by A2, GROUP_11: 4;

        then ((x * y) * (x " )) in (N1 * N2) by A3, GROUP_11: 6;

        hence thesis by A1;

      end;

      then N is normal Subgroup of G by GROUP_11: 5;

      hence thesis by A1;

    end;

    registration

      let p;

      let G be p -group finite Group, H be finite Group, g be Homomorphism of G, H;

      cluster ( Image g) -> p -group;

      coherence

      proof

        for h be Element of ( Image g) holds h is p -power

        proof

          let h be Element of ( Image g);

          h in ( Image g);

          then

          consider a be Element of G such that

           A1: h = (g . a) by GROUP_6: 45;

          consider n be Nat such that

           A2: ( ord a) = (p |^ n) by Def1;

          

           A3: (g . (a |^ (p |^ n))) = ((g . a) |^ (p |^ n)) by GROUP_6: 37

          .= (h |^ (p |^ n)) by A1, GROUP_8: 4;

          

           A4: (g . (a |^ (p |^ n))) = (g . ( 1_ G)) by A2, GROUP_1: 41

          .= ( 1_ H) by GROUP_6: 31;

          reconsider h1 = h as Element of H by GROUP_2: 42;

          (h1 |^ (p |^ n)) = ( 1_ H) by A3, A4, GROUP_8: 4;

          then

          consider r be Nat such that

           A5: ( ord h1) = (p |^ r) & r <= n by Th2, GROUP_1: 44;

          ( ord h) = (p |^ r) by A5, GROUP_8: 5;

          hence thesis;

        end;

        hence thesis by Th17;

      end;

    end

    theorem :: GROUPP_1:22

    

     Th22: for G,H be strict Group holds (G,H) are_isomorphic & G is p -group implies H is p -group by GROUP_6: 73;

    definition

      let p be prime Nat;

      let G be Group;

      :: GROUPP_1:def2

      func expon (G,p) -> Nat means

      : Def2: ( card G) = (p |^ it );

      existence by A1;

      uniqueness

      proof

        let a,b be Nat such that

         A2: ( card G) = (p |^ a) and

         A3: ( card G) = (p |^ b);

        p > 1 by INT_2:def 4;

        hence thesis by A2, A3, PEPIN: 30;

      end;

    end

    definition

      let p be prime Nat;

      let G be Group;

      :: original: expon

      redefine

      func expon (G,p) -> Element of NAT ;

      coherence by ORDINAL1:def 12;

    end

    theorem :: GROUPP_1:23

    for G be finite Group, H be Subgroup of G st G is p -group holds ( expon (H,p)) <= ( expon (G,p))

    proof

      let G be finite Group;

      let H be Subgroup of G;

      assume

       A1: G is p -group;

      then ( card G) = (p |^ ( expon (G,p))) by Def2;

      then ex r be Nat st ( card H) = (p |^ r) & r <= ( expon (G,p)) by Th2, GROUP_2: 148;

      hence thesis by A1, Def2;

    end;

    theorem :: GROUPP_1:24

    

     Th24: for G be strict finite Group st G is p -group & ( expon (G,p)) = 0 holds G = ( (1). G)

    proof

      let G be strict finite Group;

      assume G is p -group & ( expon (G,p)) = 0 ;

      

      then

       A1: ( card G) = (p |^ 0 ) by Def2

      .= 1 by NEWTON: 4;

      ( card ( (1). G)) = 1 by GROUP_2: 69;

      hence thesis by A1, GROUP_2: 73;

    end;

    theorem :: GROUPP_1:25

    

     Th25: for G be strict finite Group holds G is p -group & ( expon (G,p)) = 1 implies G is cyclic

    proof

      let G be strict finite Group;

      assume G is p -group & ( expon (G,p)) = 1;

      

      then ( card G) = (p |^ 1) by Def2

      .= p;

      hence thesis by GR_CY_1: 21;

    end;

    theorem :: GROUPP_1:26

    for G be finite Group, p be prime Nat holds for a be Element of G holds G is p -group & ( expon (G,p)) = 2 & ( ord a) = (p |^ 2) implies G is commutative

    proof

      let G be finite Group;

      let p be prime Nat;

      let a be Element of G;

      assume that

       A1: G is p -group & ( expon (G,p)) = 2 and

       A2: ( ord a) = (p |^ 2);

      ( card G) = (p |^ 2) by A1, Def2;

      then G is cyclic by A2, GR_CY_1: 19;

      hence thesis;

    end;

    begin

    definition

      let p be Nat;

      let G be Group;

      :: GROUPP_1:def3

      attr G is p -commutative-group-like means

      : Def3: for a,b be Element of G holds ((a * b) |^ p) = ((a |^ p) * (b |^ p));

    end

    definition

      let p be Nat;

      let G be Group;

      :: GROUPP_1:def4

      attr G is p -commutative-group means G is p -groupp -commutative-group-like;

    end

    registration

      let p be Nat;

      cluster p -commutative-group -> p -groupp -commutative-group-like for Group;

      coherence ;

      cluster p -groupp -commutative-group-like -> p -commutative-group for Group;

      coherence ;

    end

    theorem :: GROUPP_1:27

    

     Th27: ( (1). G) is p -commutative-group-like

    proof

      let a,b be Element of ( (1). G);

      

       A1: the carrier of ( (1). G) = {( 1_ G)} by GROUP_2:def 7;

      

      hence ((a * b) |^ p) = ( 1_ G) by TARSKI:def 1

      .= ((a |^ p) * (b |^ p)) by A1, TARSKI:def 1;

    end;

    registration

      let p;

      cluster p -commutative-group finite cyclic commutative for Group;

      existence

      proof

        take ( (1). the Group);

        ( (1). the Group) is p -commutative-group-likep -group by Th16, Th27;

        hence thesis;

      end;

    end

    registration

      let p;

      let G be p -commutative-group-like finite Group;

      cluster -> p -commutative-group-like for Subgroup of G;

      coherence

      proof

        let H be Subgroup of G;

        let a,b be Element of H;

        reconsider a2 = a, b2 = b as Element of G by GROUP_2: 42;

        

         A1: (a * b) = (a2 * b2) by GROUP_8: 2;

        

         A2: (a |^ p) = (a2 |^ p) & (b |^ p) = (b2 |^ p) by GROUP_8: 4;

        

        thus ((a * b) |^ p) = ((a2 * b2) |^ p) by A1, GROUP_8: 4

        .= ((a2 |^ p) * (b2 |^ p)) by Def3

        .= ((a |^ p) * (b |^ p)) by A2, GROUP_8: 2;

      end;

    end

    registration

      let p;

      cluster p -group finite commutative -> p -commutative-group for Group;

      coherence

      proof

        let G be Group such that

         A1: G is p -group finite commutative;

        for a,b be Element of G holds ((a * b) |^ p) = ((a |^ p) * (b |^ p)) by A1, GROUP_1: 48;

        then G is p -commutative-group-like;

        hence thesis by A1;

      end;

    end

    theorem :: GROUPP_1:28

    for G be strict finite Group st ( card G) = p holds G is p -commutative-group

    proof

      let G be strict finite Group;

      assume

       A1: ( card G) = p;

      p = (p |^ 1);

      then

       A2: G is p -group by A1;

      G is cyclic Group by A1, GR_CY_1: 21;

      hence thesis by A2;

    end;

    registration

      let p, G;

      cluster p -commutative-group finite for Subgroup of G;

      existence

      proof

        take ( (1). G);

        ( (1). G) is p -commutative-group-likep -group by Th16, Th27;

        hence thesis;

      end;

    end

    registration

      let p;

      let G be finite Group, H1 be p -commutative-group-like Subgroup of G, H2 be Subgroup of G;

      cluster (H1 /\ H2) -> p -commutative-group-like;

      coherence

      proof

        reconsider H = (H1 /\ H2) as Subgroup of H1 by GROUP_2: 88;

        H is p -commutative-group-like;

        hence thesis;

      end;

      cluster (H2 /\ H1) -> p -commutative-group-like;

      coherence ;

    end

    registration

      let p;

      let G be finitep -commutative-group-like Group, N be normal Subgroup of G;

      cluster (G ./. N) -> p -commutative-group-like;

      coherence

      proof

        let S,T be Element of (G ./. N);

        consider a be Element of G such that

         A1: S = (a * N) & S = (N * a) by GROUP_6: 21;

        consider b be Element of G such that

         A2: T = (b * N) & T = (N * b) by GROUP_6: 21;

        

         A3: (S * T) = (( @ S) * ( @ T)) by GROUP_6: 19

        .= ((a * b) * N) by A1, A2, GROUP_11: 1;

        set c = (a * b);

        

         A4: ((S * T) |^ p) = ((c |^ p) * N) by A3, Th8

        .= (((a |^ p) * (b |^ p)) * N) by Def3

        .= (((a |^ p) * N) * ((b |^ p) * N)) by GROUP_11: 1;

        

         A5: (S |^ p) = ((a |^ p) * N) by A1, Th8;

        (T |^ p) = ((b |^ p) * N) by A2, Th8;

        hence thesis by A4, A5, GROUP_6:def 3;

      end;

    end

    theorem :: GROUPP_1:29

    for G be finite Group, a,b be Element of G st G is p -commutative-group-like holds for n holds ((a * b) |^ (p |^ n)) = ((a |^ (p |^ n)) * (b |^ (p |^ n)))

    proof

      let G be finite Group;

      let a,b be Element of G;

      assume

       A1: G is p -commutative-group-like;

      defpred P[ Nat] means for n holds ((a * b) |^ (p |^ $1)) = ((a |^ (p |^ $1)) * (b |^ (p |^ $1)));

      

       A2: ((a * b) |^ (p |^ 0 )) = ((a * b) |^ 1) by NEWTON: 4

      .= (a * b) by GROUP_1: 26;

      ((a |^ (p |^ 0 )) * (b |^ (p |^ 0 ))) = ((a |^ 1) * (b |^ (p |^ 0 ))) by NEWTON: 4

      .= (a * (b |^ (p |^ 0 ))) by GROUP_1: 26

      .= (a * (b |^ 1)) by NEWTON: 4

      .= (a * b) by GROUP_1: 26;

      then

       A3: P[ 0 ] by A2;

       A4:

      now

        let n;

        assume

         A5: P[n];

        set a1 = (a |^ (p |^ n)), b1 = (b |^ (p |^ n));

        ((a * b) |^ (p |^ (n + 1))) = ((a * b) |^ ((p |^ n) * p)) by NEWTON: 6

        .= (((a * b) |^ (p |^ n)) |^ p) by GROUP_1: 35

        .= (((a |^ (p |^ n)) * (b |^ (p |^ n))) |^ p) by A5

        .= ((a1 |^ p) * (b1 |^ p)) by A1

        .= ((a |^ ((p |^ n) * p)) * ((b |^ (p |^ n)) |^ p)) by GROUP_1: 35

        .= ((a |^ ((p |^ n) * p)) * (b |^ ((p |^ n) * p))) by GROUP_1: 35

        .= ((a |^ (p |^ (n + 1))) * (b |^ ((p |^ n) * p))) by NEWTON: 6

        .= ((a |^ (p |^ (n + 1))) * (b |^ (p |^ (n + 1)))) by NEWTON: 6;

        hence P[(n + 1)];

      end;

      for n holds P[n] from NAT_1:sch 2( A3, A4);

      hence thesis;

    end;

    theorem :: GROUPP_1:30

    for G be finite commutative Group, H,H1,H2 be Subgroup of G st H1 is p -commutative-group & H2 is p -commutative-group & the carrier of H = (H1 * H2) holds H is p -commutative-group

    proof

      let G be finite commutative Group;

      let H,H1,H2 be Subgroup of G;

      assume that

       A1: H1 is p -commutative-group & H2 is p -commutative-group and

       A2: the carrier of H = (H1 * H2);

      H is p -group by A1, A2, Th19;

      hence thesis;

    end;

    theorem :: GROUPP_1:31

    for G be finite Group, H be Subgroup of G, N be strict normal Subgroup of G holds N is Subgroup of ( center G) & H is p -commutative-group & N is p -commutative-group implies ex P be strict Subgroup of G st the carrier of P = (H * N) & P is p -commutative-group

    proof

      let G be finite Group;

      let H be Subgroup of G;

      let N be strict normal Subgroup of G;

      assume that

       A1: N is Subgroup of ( center G) and

       A2: H is p -commutative-group & N is p -commutative-group;

      consider P be strict Subgroup of G such that

       A3: the carrier of P = (H * N) & P is p -group by A2, Th20;

      set P1 = P;

      for a,b be Element of P holds ((a * b) |^ p) = ((a |^ p) * (b |^ p))

      proof

        let a,b be Element of P;

        

         A4: a in (H * N) & b in (H * N) by A3;

        then

        consider a1,a2 be Element of G such that

         A5: a = (a1 * a2) & a1 in H & a2 in N by GROUP_11: 6;

        

         A6: a2 in ( center G) by A1, A5, GROUP_2: 40;

        consider b1,b2 be Element of G such that

         A7: b = (b1 * b2) & b1 in H & b2 in N by A4, GROUP_11: 6;

        

         A8: b2 in ( center G) by A1, A7, GROUP_2: 40;

        then (a2 * b2) in ( center G) & (b2 * a2) in ( center G) by A6, GROUP_2: 50;

        then

         A9: ((a1 * b1) * (b2 * a2)) = ((b2 * a2) * (a1 * b1)) by GROUP_5: 77;

        reconsider c1 = a1, d1 = b1 as Element of H by A5, A7;

        

         A10: (a1 |^ p) = (c1 |^ p) & (b1 |^ p) = (d1 |^ p) by GROUP_4: 2;

        (a1 * b1) = (c1 * d1) by GROUP_2: 43;

        

        then

         A11: ((a1 * b1) |^ p) = ((c1 * d1) |^ p) by GROUP_8: 4

        .= ((c1 |^ p) * (d1 |^ p)) by A2, Def3

        .= ((a1 |^ p) * (b1 |^ p)) by A10, GROUP_2: 43;

        reconsider c2 = a2, d2 = b2 as Element of N by A5, A7;

        

         A12: (a2 |^ p) = (c2 |^ p) & (b2 |^ p) = (d2 |^ p) by GROUP_4: 2;

        (b2 * a2) = (d2 * c2) by GROUP_2: 43;

        

        then

         A13: ((b2 * a2) |^ p) = ((d2 * c2) |^ p) by GROUP_8: 4

        .= ((d2 |^ p) * (c2 |^ p)) by A2, Def3

        .= ((b2 |^ p) * (a2 |^ p)) by A12, GROUP_2: 43;

        

         A14: (a2 |^ p) in ( center G) by A6, GROUP_4: 4;

        

         A15: (a1 * a2) = (a2 * a1) by A6, GROUP_5: 77;

        

         A16: (b1 * b2) = (b2 * b1) by A8, GROUP_5: 77;

        (a * b) = ((a1 * a2) * (b1 * b2)) by A5, A7, GROUP_2: 43;

        

        then

         A17: ((a * b) |^ p) = (((a1 * a2) * (b1 * b2)) |^ p) by GROUP_8: 4

        .= ((a1 * (a2 * (b1 * b2))) |^ p) by GROUP_1:def 3

        .= ((a1 * ((b1 * b2) * a2)) |^ p) by A6, GROUP_5: 77

        .= ((a1 * (b1 * (b2 * a2))) |^ p) by GROUP_1:def 3

        .= (((a1 * b1) * (b2 * a2)) |^ p) by GROUP_1:def 3

        .= (((a1 * b1) |^ p) * ((b2 * a2) |^ p)) by A9, GROUP_1: 38

        .= (((a1 |^ p) * (b1 |^ p)) * ((a2 |^ p) * (b2 |^ p))) by A11, A13, A14, GROUP_5: 77

        .= ((a1 |^ p) * ((b1 |^ p) * ((a2 |^ p) * (b2 |^ p)))) by GROUP_1:def 3

        .= ((a1 |^ p) * (((b1 |^ p) * (a2 |^ p)) * (b2 |^ p))) by GROUP_1:def 3

        .= ((a1 |^ p) * (((a2 |^ p) * (b1 |^ p)) * (b2 |^ p))) by A14, GROUP_5: 77

        .= (((a1 |^ p) * ((a2 |^ p) * (b1 |^ p))) * (b2 |^ p)) by GROUP_1:def 3

        .= ((((a1 |^ p) * (a2 |^ p)) * (b1 |^ p)) * (b2 |^ p)) by GROUP_1:def 3

        .= (((a1 |^ p) * (a2 |^ p)) * ((b1 |^ p) * (b2 |^ p))) by GROUP_1:def 3

        .= (((a1 * a2) |^ p) * ((b1 |^ p) * (b2 |^ p))) by A15, GROUP_1: 38

        .= (((a1 * a2) |^ p) * ((b1 * b2) |^ p)) by A16, GROUP_1: 38;

        

         A18: (a |^ p) = ((a1 * a2) |^ p) by A5, GROUP_4: 2;

        (b |^ p) = ((b1 * b2) |^ p) by A7, GROUP_4: 2;

        hence thesis by A17, A18, GROUP_2: 43;

      end;

      then P1 is p -commutative-group-like;

      hence thesis by A3;

    end;

    theorem :: GROUPP_1:32

    for G be finite Group, N1,N2 be normal Subgroup of G holds N2 is Subgroup of ( center G) & N1 is p -commutative-group & N2 is p -commutative-group implies ex N be strict normal Subgroup of G st the carrier of N = (N1 * N2) & N is p -commutative-group

    proof

      let G be finite Group;

      let N1,N2 be normal Subgroup of G;

      assume that

       A1: N2 is Subgroup of ( center G) and

       A2: N1 is p -commutative-group & N2 is p -commutative-group;

      consider N be strict normal Subgroup of G such that

       A3: the carrier of N = (N1 * N2) & N is p -group by A2, Th21;

      for a,b be Element of N holds ((a * b) |^ p) = ((a |^ p) * (b |^ p))

      proof

        let a,b be Element of N;

        

         A4: a in (N1 * N2) & b in (N1 * N2) by A3;

        then

        consider a1,a2 be Element of G such that

         A5: a = (a1 * a2) & a1 in N1 & a2 in N2 by GROUP_11: 6;

        

         A6: a2 in ( center G) by A1, A5, GROUP_2: 40;

        consider b1,b2 be Element of G such that

         A7: b = (b1 * b2) & b1 in N1 & b2 in N2 by A4, GROUP_11: 6;

        

         A8: b2 in ( center G) by A1, A7, GROUP_2: 40;

        then (a2 * b2) in ( center G) & (b2 * a2) in ( center G) by A6, GROUP_2: 50;

        then

         A9: ((a1 * b1) * (b2 * a2)) = ((b2 * a2) * (a1 * b1)) by GROUP_5: 77;

        reconsider c1 = a1, d1 = b1 as Element of N1 by A5, A7;

        

         A10: (a1 |^ p) = (c1 |^ p) & (b1 |^ p) = (d1 |^ p) by GROUP_4: 2;

        (a1 * b1) = (c1 * d1) by GROUP_2: 43;

        

        then

         A11: ((a1 * b1) |^ p) = ((c1 * d1) |^ p) by GROUP_8: 4

        .= ((c1 |^ p) * (d1 |^ p)) by A2, Def3

        .= ((a1 |^ p) * (b1 |^ p)) by A10, GROUP_2: 43;

        reconsider c2 = a2, d2 = b2 as Element of N2 by A5, A7;

        

         A12: (a2 |^ p) = (c2 |^ p) & (b2 |^ p) = (d2 |^ p) by GROUP_4: 2;

        (b2 * a2) = (d2 * c2) by GROUP_2: 43;

        

        then

         A13: ((b2 * a2) |^ p) = ((d2 * c2) |^ p) by GROUP_8: 4

        .= ((d2 |^ p) * (c2 |^ p)) by A2, Def3

        .= ((b2 |^ p) * (a2 |^ p)) by A12, GROUP_2: 43;

        

         A14: (a2 |^ p) in ( center G) by A6, GROUP_4: 4;

        

         A15: (a1 * a2) = (a2 * a1) by A6, GROUP_5: 77;

        

         A16: (b1 * b2) = (b2 * b1) by A8, GROUP_5: 77;

        (a * b) = ((a1 * a2) * (b1 * b2)) by A5, A7, GROUP_2: 43;

        

        then

         A17: ((a * b) |^ p) = (((a1 * a2) * (b1 * b2)) |^ p) by GROUP_8: 4

        .= ((a1 * (a2 * (b1 * b2))) |^ p) by GROUP_1:def 3

        .= ((a1 * ((b1 * b2) * a2)) |^ p) by A6, GROUP_5: 77

        .= ((a1 * (b1 * (b2 * a2))) |^ p) by GROUP_1:def 3

        .= (((a1 * b1) * (b2 * a2)) |^ p) by GROUP_1:def 3

        .= (((a1 * b1) |^ p) * ((b2 * a2) |^ p)) by A9, GROUP_1: 38

        .= (((a1 |^ p) * (b1 |^ p)) * ((a2 |^ p) * (b2 |^ p))) by A11, A13, A14, GROUP_5: 77

        .= ((a1 |^ p) * ((b1 |^ p) * ((a2 |^ p) * (b2 |^ p)))) by GROUP_1:def 3

        .= ((a1 |^ p) * (((b1 |^ p) * (a2 |^ p)) * (b2 |^ p))) by GROUP_1:def 3

        .= ((a1 |^ p) * (((a2 |^ p) * (b1 |^ p)) * (b2 |^ p))) by A14, GROUP_5: 77

        .= (((a1 |^ p) * ((a2 |^ p) * (b1 |^ p))) * (b2 |^ p)) by GROUP_1:def 3

        .= ((((a1 |^ p) * (a2 |^ p)) * (b1 |^ p)) * (b2 |^ p)) by GROUP_1:def 3

        .= (((a1 |^ p) * (a2 |^ p)) * ((b1 |^ p) * (b2 |^ p))) by GROUP_1:def 3

        .= (((a1 * a2) |^ p) * ((b1 |^ p) * (b2 |^ p))) by A15, GROUP_1: 38

        .= (((a1 * a2) |^ p) * ((b1 * b2) |^ p)) by A16, GROUP_1: 38;

        

         A18: (a |^ p) = ((a1 * a2) |^ p) by A5, GROUP_4: 2;

        (b |^ p) = ((b1 * b2) |^ p) by A7, GROUP_4: 2;

        hence thesis by A17, A18, GROUP_2: 43;

      end;

      then N is p -commutative-group-like;

      hence thesis by A3;

    end;

    theorem :: GROUPP_1:33

    

     Th33: for G,H be Group holds (G,H) are_isomorphic & G is p -commutative-group-like implies H is p -commutative-group-like

    proof

      let G,H be Group;

      assume that

       A1: (G,H) are_isomorphic and

       A2: G is p -commutative-group-like;

      let h1,h2 be Element of H;

      consider h be Homomorphism of G, H such that

       A3: h is bijective by A1;

      consider a be Element of G such that

       A4: (h . a) = h1 by A3, GROUP_6: 58;

      consider b be Element of G such that

       A5: (h . b) = h2 by A3, GROUP_6: 58;

      (h1 * h2) = (h . (a * b)) by A4, A5, GROUP_6:def 6;

      

      then ((h1 * h2) |^ p) = (h . ((a * b) |^ p)) by GROUP_6: 37

      .= (h . ((a |^ p) * (b |^ p))) by A2

      .= ((h . (a |^ p)) * (h . (b |^ p))) by GROUP_6:def 6

      .= (((h . a) |^ p) * (h . (b |^ p))) by GROUP_6: 37

      .= ((h1 |^ p) * (h2 |^ p)) by A4, A5, GROUP_6: 37;

      hence thesis;

    end;

    theorem :: GROUPP_1:34

    for G,H be strict Group holds (G,H) are_isomorphic & G is p -commutative-group implies H is p -commutative-group by Th22, Th33;

    registration

      let p;

      let G be p -commutative-group-like finite Group, H be finite Group;

      let g be Homomorphism of G, H;

      cluster ( Image g) -> p -commutative-group-like;

      coherence

      proof

        let g1,g2 be Element of ( Image g);

        reconsider h1 = g1, h2 = g2 as Element of H by GROUP_2: 42;

        g1 in ( Image g);

        then

        consider a be Element of G such that

         A1: g1 = (g . a) by GROUP_6: 45;

        g2 in ( Image g);

        then

        consider b be Element of G such that

         A2: g2 = (g . b) by GROUP_6: 45;

        (g1 * g2) = (h1 * h2) by GROUP_2: 43

        .= (g . (a * b)) by A1, A2, GROUP_6:def 6;

        

        then

         A3: ((g1 * g2) |^ p) = ((g . (a * b)) |^ p) by GROUP_8: 4

        .= (g . ((a * b) |^ p)) by GROUP_6: 37

        .= (g . ((a |^ p) * (b |^ p))) by Def3

        .= ((g . (a |^ p)) * (g . (b |^ p))) by GROUP_6:def 6

        .= (((g . a) |^ p) * (g . (b |^ p))) by GROUP_6: 37

        .= ((h1 |^ p) * (h2 |^ p)) by A1, A2, GROUP_6: 37;

        (h1 |^ p) = (g1 |^ p) & (h2 |^ p) = (g2 |^ p) by GROUP_8: 4;

        hence thesis by A3, GROUP_2: 43;

      end;

    end

    theorem :: GROUPP_1:35

    for G be strict finite Group st G is p -group & ( expon (G,p)) = 0 holds G is p -commutative-group

    proof

      let G be strict finite Group;

      assume

       A1: G is p -group & ( expon (G,p)) = 0 ;

      then G = ( (1). G) by Th24;

      hence thesis by A1;

    end;

    theorem :: GROUPP_1:36

    for G be strict finite Group st G is p -group & ( expon (G,p)) = 1 holds G is p -commutative-group

    proof

      let G be strict finite Group;

      assume

       A1: G is p -group & ( expon (G,p)) = 1;

      then G is cyclic by Th25;

      hence thesis by A1;

    end;