group_5.miz



    begin

    reserve x,y for set,

k,n for Nat,

i for Integer,

G for Group,

a,b,c,d,e for Element of G,

A,B,C,D for Subset of G,

H,H1,H2,H3,H4 for Subgroup of G,

N1,N2 for normal Subgroup of G,

F,F1,F2 for FinSequence of the carrier of G,

I,I1,I2 for FinSequence of INT ;

    theorem :: GROUP_5:1

    

     Th1: x in ( (1). G) iff x = ( 1_ G)

    proof

      thus x in ( (1). G) implies x = ( 1_ G)

      proof

        assume x in ( (1). G);

        then x in the carrier of ( (1). G) by STRUCT_0:def 5;

        then x in {( 1_ G)} by GROUP_2:def 7;

        hence thesis by TARSKI:def 1;

      end;

      thus thesis by GROUP_2: 46;

    end;

    theorem :: GROUP_5:2

    a in H & b in H implies (a |^ b) in H

    proof

      assume a in H & b in H;

      then (b " ) in H & (a * b) in H by GROUP_2: 50, GROUP_2: 51;

      then ((b " ) * (a * b)) in H by GROUP_2: 50;

      hence thesis by GROUP_1:def 3;

    end;

    theorem :: GROUP_5:3

    

     Th3: for N be strict normal Subgroup of G holds a in N implies (a |^ b) in N

    proof

      let N be strict normal Subgroup of G;

      assume a in N;

      then (a |^ b) in (N |^ b) by GROUP_3: 58;

      hence thesis by GROUP_3:def 13;

    end;

    theorem :: GROUP_5:4

    

     Th4: x in (H1 * H2) iff ex a, b st x = (a * b) & a in H1 & b in H2

    proof

      thus x in (H1 * H2) implies ex a, b st x = (a * b) & a in H1 & b in H2

      proof

        assume x in (H1 * H2);

        then x in (( carr H1) * H2);

        then

        consider a, b such that

         A1: x = (a * b) and

         A2: a in ( carr H1) and

         A3: b in H2 by GROUP_2: 94;

        a in H1 by A2, STRUCT_0:def 5;

        hence thesis by A1, A3;

      end;

      given a, b such that

       A4: x = (a * b) & a in H1 and

       A5: b in H2;

      b in ( carr H2) by A5, STRUCT_0:def 5;

      then x in (H1 * ( carr H2)) by A4, GROUP_2: 95;

      hence thesis;

    end;

    theorem :: GROUP_5:5

    

     Th5: (H1 * H2) = (H2 * H1) implies (x in (H1 "\/" H2) iff ex a, b st x = (a * b) & a in H1 & b in H2)

    proof

      assume

       A1: (H1 * H2) = (H2 * H1);

      thus x in (H1 "\/" H2) implies ex a, b st x = (a * b) & a in H1 & b in H2

      proof

        assume x in (H1 "\/" H2);

        then x in the carrier of (H1 "\/" H2) by STRUCT_0:def 5;

        then x in (H1 * H2) by A1, GROUP_4: 51;

        hence thesis by Th4;

      end;

      given a, b such that

       A2: x = (a * b) & a in H1 & b in H2;

      x in (H1 * H2) by A2, Th4;

      then x in the carrier of (H1 "\/" H2) by A1, GROUP_4: 51;

      hence thesis by STRUCT_0:def 5;

    end;

    theorem :: GROUP_5:6

    G is commutative Group implies (x in (H1 "\/" H2) iff ex a, b st x = (a * b) & a in H1 & b in H2)

    proof

      assume G is commutative Group;

      then (H1 * H2) = (H2 * H1) by GROUP_2: 25;

      hence thesis by Th5;

    end;

    theorem :: GROUP_5:7

    

     Th7: for N1,N2 be strict normal Subgroup of G holds x in (N1 "\/" N2) iff ex a, b st x = (a * b) & a in N1 & b in N2

    proof

      let N1,N2 be strict normal Subgroup of G;

      (N1 * N2) = (N2 * N1) by GROUP_3: 125;

      hence thesis by Th5;

    end;

    theorem :: GROUP_5:8

    for N be normal Subgroup of G holds (H * N) = (N * H)

    proof

      let N be normal Subgroup of G;

      

      thus (H * N) = (( carr H) * N)

      .= (N * ( carr H)) by GROUP_3: 120

      .= (N * H);

    end;

    definition

      let G, F, a;

      :: GROUP_5:def1

      func F |^ a -> FinSequence of the carrier of G means

      : Def1: ( len it ) = ( len F) & for k be Nat st k in ( dom F) holds (it . k) = ((F /. k) |^ a);

      existence

      proof

        deffunc F( Nat) = ((F /. $1) |^ a);

        consider F1 such that

         A1: ( len F1) = ( len F) & for k be Nat st k in ( dom F1) holds (F1 . k) = F(k) from FINSEQ_2:sch 1;

        ( dom F1) = ( dom F) by A1, FINSEQ_3: 29;

        hence thesis by A1;

      end;

      correctness

      proof

        let F1, F2;

        assume that

         A2: ( len F1) = ( len F) and

         A3: for k be Nat st k in ( dom F) holds (F1 . k) = ((F /. k) |^ a) and

         A4: ( len F2) = ( len F) and

         A5: for k be Nat st k in ( dom F) holds (F2 . k) = ((F /. k) |^ a);

        

         A6: ( dom F1) = ( Seg ( len F)) by A2, FINSEQ_1:def 3;

        now

          let k be Nat;

          assume k in ( dom F1);

          then

           A7: k in ( dom F) by A6, FINSEQ_1:def 3;

          

          hence (F1 . k) = ((F /. k) |^ a) by A3

          .= (F2 . k) by A5, A7;

        end;

        hence thesis by A2, A4, FINSEQ_2: 9;

      end;

    end

    theorem :: GROUP_5:9

    

     Th9: ((F1 |^ a) ^ (F2 |^ a)) = ((F1 ^ F2) |^ a)

    proof

       A1:

      now

        let k;

        assume k in ( dom (F1 |^ a));

        then k in ( Seg ( len (F1 |^ a))) by FINSEQ_1:def 3;

        then k in ( Seg ( len F1)) by Def1;

        then

         A2: k in ( dom F1) by FINSEQ_1:def 3;

        then

         A3: (F1 /. k) = ((F1 ^ F2) /. k) & k in ( dom (F1 ^ F2)) by FINSEQ_3: 22, FINSEQ_4: 68;

        

        thus ((F1 |^ a) . k) = ((F1 /. k) |^ a) by A2, Def1

        .= (((F1 ^ F2) |^ a) . k) by A3, Def1;

      end;

       A4:

      now

        let k;

        assume

         A5: k in ( dom (F2 |^ a));

        ( len F2) = ( len (F2 |^ a)) by Def1;

        then

         A6: k in ( dom F2) by A5, FINSEQ_3: 29;

        then (( len F1) + k) in ( dom (F1 ^ F2)) by FINSEQ_1: 28;

        then (( len (F1 |^ a)) + k) in ( dom (F1 ^ F2)) by Def1;

        

        hence (((F1 ^ F2) |^ a) . (( len (F1 |^ a)) + k)) = (((F1 ^ F2) /. (( len (F1 |^ a)) + k)) |^ a) by Def1

        .= (((F1 ^ F2) /. (( len F1) + k)) |^ a) by Def1

        .= ((F2 /. k) |^ a) by A6, FINSEQ_4: 69

        .= ((F2 |^ a) . k) by A6, Def1;

      end;

      (( len (F1 |^ a)) + ( len (F2 |^ a))) = (( len F1) + ( len (F2 |^ a))) by Def1

      .= (( len F1) + ( len F2)) by Def1

      .= ( len (F1 ^ F2)) by FINSEQ_1: 22

      .= ( len ((F1 ^ F2) |^ a)) by Def1;

      hence thesis by A1, A4, FINSEQ_3: 38;

    end;

    theorem :: GROUP_5:10

    

     Th10: (( <*> the carrier of G) |^ a) = {}

    proof

      ( len (( <*> the carrier of G) |^ a)) = ( len ( <*> the carrier of G)) by Def1

      .= 0 ;

      hence thesis;

    end;

    theorem :: GROUP_5:11

    

     Th11: ( <*a*> |^ b) = <*(a |^ b)*>

    proof

       A1:

      now

        let k be Nat;

        assume k in ( dom <*a*>);

        then k in {1} by FINSEQ_1: 2, FINSEQ_1: 38;

        then

         A2: k = 1 by TARSKI:def 1;

        

        hence ( <*(a |^ b)*> . k) = (a |^ b) by FINSEQ_1: 40

        .= (( <*a*> /. k) |^ b) by A2, FINSEQ_4: 16;

      end;

      ( len <*(a |^ b)*>) = 1 by FINSEQ_1: 40

      .= ( len <*a*>) by FINSEQ_1: 39;

      hence thesis by A1, Def1;

    end;

    theorem :: GROUP_5:12

    

     Th12: ( <*a, b*> |^ c) = <*(a |^ c), (b |^ c)*>

    proof

      

      thus ( <*a, b*> |^ c) = (( <*a*> ^ <*b*>) |^ c) by FINSEQ_1:def 9

      .= (( <*a*> |^ c) ^ ( <*b*> |^ c)) by Th9

      .= ( <*(a |^ c)*> ^ ( <*b*> |^ c)) by Th11

      .= ( <*(a |^ c)*> ^ <*(b |^ c)*>) by Th11

      .= <*(a |^ c), (b |^ c)*> by FINSEQ_1:def 9;

    end;

    theorem :: GROUP_5:13

    ( <*a, b, c*> |^ d) = <*(a |^ d), (b |^ d), (c |^ d)*>

    proof

      

      thus ( <*a, b, c*> |^ d) = (( <*a*> ^ <*b, c*>) |^ d) by FINSEQ_1: 43

      .= (( <*a*> |^ d) ^ ( <*b, c*> |^ d)) by Th9

      .= (( <*a*> |^ d) ^ <*(b |^ d), (c |^ d)*>) by Th12

      .= ( <*(a |^ d)*> ^ <*(b |^ d), (c |^ d)*>) by Th11

      .= <*(a |^ d), (b |^ d), (c |^ d)*> by FINSEQ_1: 43;

    end;

    theorem :: GROUP_5:14

    

     Th14: ( Product (F |^ a)) = (( Product F) |^ a)

    proof

      defpred P[ FinSequence of the carrier of G] means ( Product ($1 |^ a)) = (( Product $1) |^ a);

       A1:

      now

        let F, b;

        assume

         A2: P[F];

        ( Product ((F ^ <*b*>) |^ a)) = ( Product ((F |^ a) ^ ( <*b*> |^ a))) by Th9

        .= ((( Product F) |^ a) * ( Product ( <*b*> |^ a))) by A2, GROUP_4: 5

        .= ((( Product F) |^ a) * ( Product <*(b |^ a)*>)) by Th11

        .= ((( Product F) |^ a) * (b |^ a)) by FINSOP_1: 11

        .= ((( Product F) * b) |^ a) by GROUP_3: 23

        .= (( Product (F ^ <*b*>)) |^ a) by GROUP_4: 6;

        hence P[(F ^ <*b*>)];

      end;

      

       A3: P[( <*> the carrier of G)]

      proof

        set p = ( <*> the carrier of G);

        

        thus ( Product (p |^ a)) = ( Product p) by Th10

        .= ( 1_ G) by GROUP_4: 8

        .= (( 1_ G) |^ a) by GROUP_3: 17

        .= (( Product p) |^ a) by GROUP_4: 8;

      end;

      for F holds P[F] from FINSEQ_2:sch 2( A3, A1);

      hence thesis;

    end;

    theorem :: GROUP_5:15

    

     Th15: ((F |^ a) |^ I) = ((F |^ I) |^ a)

    proof

      ( len (F |^ I)) = ( len F) by GROUP_4:def 3;

      then

       A1: ( dom (F |^ I)) = ( dom F) by FINSEQ_3: 29;

      

       A2: ( len (F |^ a)) = ( len F) by Def1;

      then

       A3: ( dom (F |^ a)) = ( dom F) by FINSEQ_3: 29;

      

       A4: ( len ((F |^ a) |^ I)) = ( len (F |^ a)) by GROUP_4:def 3;

      then

       A5: ( dom ((F |^ a) |^ I)) = ( Seg ( len F)) by A2, FINSEQ_1:def 3;

       A6:

      now

        let k be Nat;

        assume k in ( dom ((F |^ a) |^ I));

        then

         A7: k in ( dom F) by A5, FINSEQ_1:def 3;

        then

         A8: ((F |^ a) /. k) = ((F |^ a) . k) by A3, PARTFUN1:def 6;

        

         A9: ((F |^ I) /. k) = ((F |^ I) . k) by A1, A7, PARTFUN1:def 6;

        

        thus (((F |^ a) |^ I) . k) = (((F |^ a) /. k) |^ ( @ (I /. k))) by A3, A7, GROUP_4:def 3

        .= (((F /. k) |^ a) |^ ( @ (I /. k))) by A7, A8, Def1

        .= (((F /. k) |^ ( @ (I /. k))) |^ a) by GROUP_3: 28

        .= (((F |^ I) /. k) |^ a) by A7, A9, GROUP_4:def 3

        .= (((F |^ I) |^ a) . k) by A1, A7, Def1;

      end;

      ( len ((F |^ I) |^ a)) = ( len (F |^ I)) by Def1

      .= ( len F) by GROUP_4:def 3;

      hence thesis by A2, A4, A6, FINSEQ_2: 9;

    end;

    begin

    definition

      let G, a, b;

      :: GROUP_5:def2

      func [.a,b.] -> Element of G equals ((((a " ) * (b " )) * a) * b);

      correctness ;

    end

    theorem :: GROUP_5:16

    

     Th16: [.a, b.] = ((((a " ) * (b " )) * a) * b) & [.a, b.] = (((a " ) * ((b " ) * a)) * b) & [.a, b.] = ((a " ) * (((b " ) * a) * b)) & [.a, b.] = ((a " ) * ((b " ) * (a * b))) & [.a, b.] = (((a " ) * (b " )) * (a * b))

    proof

      thus [.a, b.] = ((((a " ) * (b " )) * a) * b);

      thus [.a, b.] = (((a " ) * ((b " ) * a)) * b) by GROUP_1:def 3;

      hence [.a, b.] = ((a " ) * (((b " ) * a) * b)) by GROUP_1:def 3;

      hence [.a, b.] = ((a " ) * ((b " ) * (a * b))) by GROUP_1:def 3;

      thus thesis by GROUP_1:def 3;

    end;

    theorem :: GROUP_5:17

    

     Th17: [.a, b.] = (((b * a) " ) * (a * b))

    proof

      

      thus [.a, b.] = (((a " ) * (b " )) * (a * b)) by Th16

      .= (((b * a) " ) * (a * b)) by GROUP_1: 17;

    end;

    theorem :: GROUP_5:18

     [.a, b.] = (((b " ) |^ a) * b) & [.a, b.] = ((a " ) * (a |^ b)) by Th16;

    theorem :: GROUP_5:19

    

     Th19: [.( 1_ G), a.] = ( 1_ G) & [.a, ( 1_ G).] = ( 1_ G)

    proof

      

      thus [.( 1_ G), a.] = (((( 1_ G) " ) * (a " )) * a) by GROUP_1:def 4

      .= ((( 1_ G) * (a " )) * a) by GROUP_1: 8

      .= ((a " ) * a) by GROUP_1:def 4

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

      

      thus [.a, ( 1_ G).] = (((a " ) * (( 1_ G) " )) * a) by GROUP_1:def 4

      .= (((a " ) * ( 1_ G)) * a) by GROUP_1: 8

      .= ((a " ) * a) by GROUP_1:def 4

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

    end;

    theorem :: GROUP_5:20

    

     Th20: [.a, a.] = ( 1_ G)

    proof

      

      thus [.a, a.] = (((a * a) " ) * (a * a)) by Th17

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

    end;

    theorem :: GROUP_5:21

     [.a, (a " ).] = ( 1_ G) & [.(a " ), a.] = ( 1_ G)

    proof

      

      thus [.a, (a " ).] = (((a " ) * ((a " ) " )) * (a * (a " ))) by Th16

      .= (( 1_ G) * (a * (a " ))) by GROUP_1:def 5

      .= (a * (a " )) by GROUP_1:def 4

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

      

      thus [.(a " ), a.] = ((((a " ) " ) * (a " )) * ((a " ) * a)) by Th16

      .= ((((a " ) " ) * (a " )) * ( 1_ G)) by GROUP_1:def 5

      .= (((a " ) " ) * (a " )) by GROUP_1:def 4

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

    end;

    theorem :: GROUP_5:22

    

     Th22: ( [.a, b.] " ) = [.b, a.]

    proof

      

      thus ( [.a, b.] " ) = ((((a " ) * (b " )) * (a * b)) " ) by Th16

      .= (((a * b) " ) * (((a " ) * (b " )) " )) by GROUP_1: 17

      .= (((b " ) * (a " )) * (((a " ) * (b " )) " )) by GROUP_1: 17

      .= (((b " ) * (a " )) * (((b " ) " ) * ((a " ) " ))) by GROUP_1: 17

      .= (((b " ) * (a " )) * (((b " ) " ) * a))

      .= (((b " ) * (a " )) * (b * a))

      .= [.b, a.] by Th16;

    end;

    theorem :: GROUP_5:23

    

     Th23: ( [.a, b.] |^ c) = [.(a |^ c), (b |^ c).]

    proof

      

      thus ( [.a, b.] |^ c) = (((c " ) * (((((a " ) * ( 1_ G)) * (b " )) * a) * b)) * c) by GROUP_1:def 4

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

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

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

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

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

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

      .= ((((a " ) |^ c) * ((c " ) * ((b " ) * (a * b)))) * c) by GROUP_1:def 3

      .= ((((a |^ c) " ) * ((c " ) * ((b " ) * (a * b)))) * c) by GROUP_3: 26

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

      .= ((((a |^ c) " ) * ((c " ) * (((b " ) * (c * (c " ))) * (a * b)))) * c) by GROUP_1:def 5

      .= ((((a |^ c) " ) * ((c " ) * ((b " ) * ((c * (c " )) * (a * b))))) * c) by GROUP_1:def 3

      .= ((((a |^ c) " ) * (((c " ) * (b " )) * ((c * (c " )) * (a * b)))) * c) by GROUP_1:def 3

      .= ((((a |^ c) " ) * (((c " ) * (b " )) * (c * ((c " ) * (a * b))))) * c) by GROUP_1:def 3

      .= ((((a |^ c) " ) * (((b " ) |^ c) * ((c " ) * (a * b)))) * c) by GROUP_1:def 3

      .= ((((a |^ c) " ) * (((b |^ c) " ) * ((c " ) * (a * b)))) * c) by GROUP_3: 26

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

      .= ((((a |^ c) " ) * (((b |^ c) " ) * ((c " ) * ((a * (c * (c " ))) * b)))) * c) by GROUP_1:def 5

      .= ((((a |^ c) " ) * (((b |^ c) " ) * ((c " ) * (a * ((c * (c " )) * b))))) * c) by GROUP_1:def 3

      .= ((((a |^ c) " ) * (((b |^ c) " ) * (((c " ) * a) * ((c * (c " )) * b)))) * c) by GROUP_1:def 3

      .= ((((a |^ c) " ) * (((b |^ c) " ) * (((c " ) * a) * (c * ((c " ) * b))))) * c) by GROUP_1:def 3

      .= ((((a |^ c) " ) * (((b |^ c) " ) * ((a |^ c) * ((c " ) * b)))) * c) by GROUP_1:def 3

      .= (((a |^ c) " ) * ((((b |^ c) " ) * ((a |^ c) * ((c " ) * b))) * c)) by GROUP_1:def 3

      .= (((a |^ c) " ) * (((b |^ c) " ) * (((a |^ c) * ((c " ) * b)) * c))) by GROUP_1:def 3

      .= (((a |^ c) " ) * (((b |^ c) " ) * ((a |^ c) * (b |^ c)))) by GROUP_1:def 3

      .= [.(a |^ c), (b |^ c).] by Th16;

    end;

    theorem :: GROUP_5:24

     [.a, b.] = ((((a " ) |^ 2) * ((a * (b " )) |^ 2)) * (b |^ 2))

    proof

      

      thus [.a, b.] = (((a " ) * (b " )) * (a * b)) by Th16

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

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

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

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

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

      .= (((((a " ) |^ 2) * a) * (b " )) * ((a * ((b " ) * b)) * b)) by GROUP_1: 27

      .= (((((a " ) |^ 2) * a) * (b " )) * (a * (((b " ) * b) * b))) by GROUP_1:def 3

      .= (((((a " ) |^ 2) * a) * (b " )) * (a * ((b " ) * (b * b)))) by GROUP_1:def 3

      .= (((((a " ) |^ 2) * a) * (b " )) * (a * ((b " ) * (b |^ 2)))) by GROUP_1: 27

      .= ((((a " ) |^ 2) * (a * (b " ))) * (a * ((b " ) * (b |^ 2)))) by GROUP_1:def 3

      .= (((a " ) |^ 2) * ((a * (b " )) * (a * ((b " ) * (b |^ 2))))) by GROUP_1:def 3

      .= (((a " ) |^ 2) * ((a * (b " )) * ((a * (b " )) * (b |^ 2)))) by GROUP_1:def 3

      .= (((a " ) |^ 2) * (((a * (b " )) * (a * (b " ))) * (b |^ 2))) by GROUP_1:def 3

      .= ((((a " ) |^ 2) * ((a * (b " )) * (a * (b " )))) * (b |^ 2)) by GROUP_1:def 3

      .= ((((a " ) |^ 2) * ((a * (b " )) |^ 2)) * (b |^ 2)) by GROUP_1: 27;

    end;

    theorem :: GROUP_5:25

    

     Th25: [.(a * b), c.] = (( [.a, c.] |^ b) * [.b, c.])

    proof

      

      thus [.(a * b), c.] = ((((a * b) " ) * (c " )) * ((a * b) * c)) by Th16

      .= ((((b " ) * (a " )) * (c " )) * ((a * b) * c)) by GROUP_1: 17

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

      .= (( [.a, c.] |^ b) * (((b " ) * (c " )) * (b * c))) by Th16

      .= (( [.a, c.] |^ b) * [.b, c.]) by Th16;

    end;

    theorem :: GROUP_5:26

     [.a, (b * c).] = ( [.a, c.] * ( [.a, b.] |^ c))

    proof

      

      thus [.a, (b * c).] = (((a " ) * ((b * c) " )) * (a * (b * c))) by Th16

      .= (((a " ) * ((c " ) * (b " ))) * (a * (b * c))) by GROUP_1: 17

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

      .= ( [.a, c.] * (((c " ) * (((a " ) * (b " )) * (a * b))) * c)) by Th16

      .= ( [.a, c.] * ( [.a, b.] |^ c)) by Th16;

    end;

    theorem :: GROUP_5:27

    

     Th27: [.(a " ), b.] = ( [.b, a.] |^ (a " ))

    proof

      

      thus [.(a " ), b.] = (((a " ) " ) * ((b " ) * ((a " ) * b))) by Th16

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

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

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

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

      .= ( [.b, a.] |^ (a " )) by Th16;

    end;

    theorem :: GROUP_5:28

    

     Th28: [.a, (b " ).] = ( [.b, a.] |^ (b " ))

    proof

      

      thus [.a, (b " ).] = ((((a " ) * b) * a) * (b " ))

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

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

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

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

      .= ( [.b, a.] |^ (b " )) by Th16;

    end;

    theorem :: GROUP_5:29

     [.(a " ), (b " ).] = ( [.a, b.] |^ ((a * b) " )) & [.(a " ), (b " ).] = ( [.a, b.] |^ ((b * a) " ))

    proof

      

      thus [.(a " ), (b " ).] = ( [.(b " ), a.] |^ (a " )) by Th27

      .= (( [.a, b.] |^ (b " )) |^ (a " )) by Th27

      .= ( [.a, b.] |^ ((b " ) * (a " ))) by GROUP_3: 24

      .= ( [.a, b.] |^ ((a * b) " )) by GROUP_1: 17;

      

      thus [.(a " ), (b " ).] = ( [.b, (a " ).] |^ (b " )) by Th28

      .= (( [.a, b.] |^ (a " )) |^ (b " )) by Th28

      .= ( [.a, b.] |^ ((a " ) * (b " ))) by GROUP_3: 24

      .= ( [.a, b.] |^ ((b * a) " )) by GROUP_1: 17;

    end;

    theorem :: GROUP_5:30

     [.a, (b |^ (a " )).] = [.b, (a " ).]

    proof

      

      thus [.a, (b |^ (a " )).] = ((((a " ) * ((b " ) |^ (a " ))) * a) * (b |^ (a " ))) by GROUP_3: 26

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

      .= ((((b " ) * (a " )) * a) * (b |^ (a " ))) by GROUP_3: 1

      .= ((b " ) * ((((a " ) " ) * b) * (a " ))) by GROUP_3: 1

      .= [.b, (a " ).] by Th16;

    end;

    theorem :: GROUP_5:31

     [.(a |^ (b " )), b.] = [.(b " ), a.]

    proof

      

      thus [.(a |^ (b " )), b.] = (((((a " ) |^ (b " )) * (b " )) * (a |^ (b " ))) * b) by GROUP_3: 26

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

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

      .= ((((a " ) |^ (b " )) * (a * (b " ))) * b) by GROUP_3: 1

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

      .= [.(b " ), a.] by GROUP_3: 1;

    end;

    theorem :: GROUP_5:32

     [.(a |^ n), b.] = ((a |^ ( - n)) * ((a |^ b) |^ n))

    proof

      

      thus [.(a |^ n), b.] = (((a |^ n) " ) * (((b " ) * (a |^ n)) * b)) by Th16

      .= ((a |^ ( - n)) * ((a |^ n) |^ b)) by GROUP_1: 36

      .= ((a |^ ( - n)) * ((a |^ b) |^ n)) by GROUP_3: 27;

    end;

    theorem :: GROUP_5:33

     [.a, (b |^ n).] = (((b |^ a) |^ ( - n)) * (b |^ n))

    proof

      

      thus [.a, (b |^ n).] = (((b |^ ( - n)) |^ a) * (b |^ n)) by GROUP_1: 36

      .= (((b |^ a) |^ ( - n)) * (b |^ n)) by GROUP_3: 28;

    end;

    theorem :: GROUP_5:34

     [.(a |^ i), b.] = ((a |^ ( - i)) * ((a |^ b) |^ i))

    proof

      

      thus [.(a |^ i), b.] = (((a |^ i) " ) * (((b " ) * (a |^ i)) * b)) by Th16

      .= ((a |^ ( - i)) * ((a |^ i) |^ b)) by GROUP_1: 36

      .= ((a |^ ( - i)) * ((a |^ b) |^ i)) by GROUP_3: 28;

    end;

    theorem :: GROUP_5:35

     [.a, (b |^ i).] = (((b |^ a) |^ ( - i)) * (b |^ i))

    proof

      

      thus [.a, (b |^ i).] = (((b |^ ( - i)) |^ a) * (b |^ i)) by GROUP_1: 36

      .= (((b |^ a) |^ ( - i)) * (b |^ i)) by GROUP_3: 28;

    end;

    theorem :: GROUP_5:36

    

     Th36: [.a, b.] = ( 1_ G) iff (a * b) = (b * a)

    proof

      thus [.a, b.] = ( 1_ G) implies (a * b) = (b * a)

      proof

        assume [.a, b.] = ( 1_ G);

        then (((b * a) " ) * (a * b)) = ( 1_ G) by Th17;

        then (a * b) = (((b * a) " ) " ) by GROUP_1: 12;

        hence thesis;

      end;

      assume (a * b) = (b * a);

      then

       A1: ((b * a) " ) = ((b " ) * (a " )) by GROUP_1: 18;

       [.a, b.] = (((b * a) " ) * (a * b)) by Th17;

      

      hence [.a, b.] = ((((b " ) * (a " )) * a) * b) by A1, GROUP_1:def 3

      .= ((b " ) * b) by GROUP_3: 1

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

    end;

    

     Lm1: for G be commutative Group holds for a,b be Element of G holds (a * b) = (b * a);

    theorem :: GROUP_5:37

    G is commutative Group iff for a, b holds [.a, b.] = ( 1_ G)

    proof

      thus G is commutative Group implies for a, b holds [.a, b.] = ( 1_ G)

      proof

        assume

         A1: G is commutative Group;

        let a, b;

        (a * b) = (b * a) by A1, Lm1;

        hence thesis by Th36;

      end;

      assume

       A2: for a, b holds [.a, b.] = ( 1_ G);

      G is commutative

      proof

        let a, b;

         [.a, b.] = ( 1_ G) by A2;

        hence thesis by Th36;

      end;

      hence thesis;

    end;

    theorem :: GROUP_5:38

    

     Th38: a in H & b in H implies [.a, b.] in H

    proof

      assume

       A1: a in H & b in H;

      then (a " ) in H & (b " ) in H by GROUP_2: 51;

      then

       A2: ((a " ) * (b " )) in H by GROUP_2: 50;

      (a * b) in H by A1, GROUP_2: 50;

      then (((a " ) * (b " )) * (a * b)) in H by A2, GROUP_2: 50;

      hence thesis by Th16;

    end;

    definition

      let G, a, b, c;

      :: GROUP_5:def3

      func [.a,b,c.] -> Element of G equals [. [.a, b.], c.];

      correctness ;

    end

    theorem :: GROUP_5:39

     [.a, b, ( 1_ G).] = ( 1_ G) & [.a, ( 1_ G), b.] = ( 1_ G) & [.( 1_ G), a, b.] = ( 1_ G)

    proof

      thus [.a, b, ( 1_ G).] = ( 1_ G) by Th19;

      

      thus [.a, ( 1_ G), b.] = [.( 1_ G), b.] by Th19

      .= ( 1_ G) by Th19;

      

      thus [.( 1_ G), a, b.] = [.( 1_ G), b.] by Th19

      .= ( 1_ G) by Th19;

    end;

    theorem :: GROUP_5:40

     [.a, a, b.] = ( 1_ G)

    proof

      

      thus [.a, a, b.] = [.( 1_ G), b.] by Th20

      .= ( 1_ G) by Th19;

    end;

    theorem :: GROUP_5:41

     [.a, b, a.] = [.(a |^ b), a.]

    proof

      

      thus [.a, b, a.] = ((( [.b, a.] * (a " )) * [.a, b.]) * a) by Th22

      .= ((((a " ) |^ b) * ((((a " ) * (b " )) * a) * b)) * a) by GROUP_3: 1

      .= ((((a |^ b) " ) * ((((a " ) * (b " )) * a) * b)) * a) by GROUP_3: 26

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

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

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

      .= [.(a |^ b), a.] by Th16;

    end;

    theorem :: GROUP_5:42

     [.b, a, a.] = (( [.b, (a " ).] * [.b, a.]) |^ a)

    proof

      

      thus [.b, a, a.] = ((( [.a, b.] * (a " )) * [.b, a.]) * a) by Th22

      .= (((((a " ) * ((b " ) * (a * b))) * (a " )) * [.b, a.]) * a) by Th16

      .= (((((a " ) * ((b " ) * (((a " ) " ) * b))) * (a " )) * [.b, a.]) * a)

      .= ((((a " ) * (((b " ) * (((a " ) " ) * b)) * (a " ))) * [.b, a.]) * a) by GROUP_1:def 3

      .= ((((a " ) * [.b, (a " ).]) * [.b, a.]) * a) by Th16

      .= (( [.b, (a " ).] * [.b, a.]) |^ a) by GROUP_1:def 3;

    end;

    theorem :: GROUP_5:43

     [.a, b, (b |^ a).] = [.b, [.b, a.].]

    proof

      

      thus [.a, b, (b |^ a).] = ((( [.b, a.] * ((b |^ a) " )) * [.a, b.]) * (b |^ a)) by Th22

      .= (((((((b " ) * (a " )) * b) * a) * ((b " ) |^ a)) * [.a, b.]) * (b |^ a)) by GROUP_3: 26

      .= (((((((b " ) * (a " )) * b) * a) * ((a " ) * ((b " ) * a))) * [.a, b.]) * (b |^ a)) by GROUP_1:def 3

      .= ((((((((b " ) * (a " )) * b) * a) * (a " )) * ((b " ) * a)) * [.a, b.]) * (b |^ a)) by GROUP_1:def 3

      .= ((((((b " ) * (a " )) * b) * ((b " ) * a)) * [.a, b.]) * (b |^ a)) by GROUP_3: 1

      .= (((((b " ) * (a " )) * (b * ((b " ) * a))) * [.a, b.]) * (b |^ a)) by GROUP_1:def 3

      .= (((((b " ) * (a " )) * a) * [.a, b.]) * (b |^ a)) by GROUP_3: 1

      .= (((b " ) * ((((a " ) * (b " )) * a) * b)) * (b |^ a)) by GROUP_3: 1

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

      .= ((((b " ) * [.a, b.]) * (b * (b " ))) * (((a " ) * b) * a)) by GROUP_1:def 5

      .= (((b " ) * [.a, b.]) * ((b * (b " )) * (((a " ) * b) * a))) by GROUP_1:def 3

      .= (((b " ) * [.a, b.]) * (b * ((b " ) * (((a " ) * b) * a)))) by GROUP_1:def 3

      .= (((b " ) * [.a, b.]) * (b * [.b, a.])) by Th16

      .= (((b " ) * ( [.b, a.] " )) * (b * [.b, a.])) by Th22

      .= [.b, [.b, a.].] by Th16;

    end;

    theorem :: GROUP_5:44

     [.(a * b), c.] = (( [.a, c.] * [.a, c, b.]) * [.b, c.])

    proof

      (( [.a, c.] * [.a, c, b.]) * [.b, c.]) = ((((((a " ) * (c " )) * a) * c) * ((( [.c, a.] * (b " )) * [.a, c.]) * b)) * [.b, c.]) by Th22

      .= ((((((a " ) * (c " )) * a) * c) * ((((((c " ) * (a " )) * (c * a)) * (b " )) * [.a, c.]) * b)) * [.b, c.]) by Th16

      .= ((((((a " ) * (c " )) * a) * c) * ((((((a * c) " ) * (c * a)) * (b " )) * [.a, c.]) * b)) * [.b, c.]) by GROUP_1: 17

      .= (((((a " ) * (c " )) * (a * c)) * ((((((a * c) " ) * (c * a)) * (b " )) * [.a, c.]) * b)) * [.b, c.]) by GROUP_1:def 3

      .= ((((a " ) * (c " )) * ((a * c) * ((((((a * c) " ) * (c * a)) * (b " )) * [.a, c.]) * b))) * [.b, c.]) by GROUP_1:def 3

      .= ((((a " ) * (c " )) * ((a * c) * (((((a * c) " ) * (c * a)) * (b " )) * ( [.a, c.] * b)))) * [.b, c.]) by GROUP_1:def 3

      .= ((((a " ) * (c " )) * ((a * c) * ((((a * c) " ) * (c * a)) * ((b " ) * ( [.a, c.] * b))))) * [.b, c.]) by GROUP_1:def 3

      .= ((((a " ) * (c " )) * ((a * c) * (((a * c) " ) * ((c * a) * ((b " ) * ( [.a, c.] * b)))))) * [.b, c.]) by GROUP_1:def 3

      .= ((((a " ) * (c " )) * (((a * c) * ((a * c) " )) * ((c * a) * ((b " ) * ( [.a, c.] * b))))) * [.b, c.]) by GROUP_1:def 3

      .= ((((a " ) * (c " )) * (( 1_ G) * ((c * a) * ((b " ) * ( [.a, c.] * b))))) * [.b, c.]) by GROUP_1:def 5

      .= ((((a " ) * (c " )) * ((c * a) * ((b " ) * ( [.a, c.] * b)))) * [.b, c.]) by GROUP_1:def 4

      .= (((((a " ) * (c " )) * (c * a)) * ((b " ) * ( [.a, c.] * b))) * [.b, c.]) by GROUP_1:def 3

      .= (((((c * a) " ) * (c * a)) * ((b " ) * ( [.a, c.] * b))) * [.b, c.]) by GROUP_1: 17

      .= ((( 1_ G) * ((b " ) * ( [.a, c.] * b))) * [.b, c.]) by GROUP_1:def 5

      .= (((b " ) * ( [.a, c.] * b)) * [.b, c.]) by GROUP_1:def 4

      .= (((b " ) * (((((a " ) * (c " )) * a) * c) * b)) * (((b " ) * (c " )) * (b * c))) by Th16

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

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

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

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

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

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

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

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

      .= (((((((b " ) * (a " )) * (c " )) * a) * (c * b)) * ((c * b) " )) * (b * c)) by GROUP_1: 17

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

      .= ((((((b " ) * (a " )) * (c " )) * a) * ( 1_ G)) * (b * c)) by GROUP_1:def 5

      .= (((((b " ) * (a " )) * (c " )) * a) * (b * c)) by GROUP_1:def 4

      .= (((((a * b) " ) * (c " )) * a) * (b * c)) by GROUP_1: 17

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

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

      hence thesis by Th16;

    end;

    theorem :: GROUP_5:45

     [.a, (b * c).] = (( [.a, c.] * [.a, b.]) * [.a, b, c.])

    proof

      (( [.a, c.] * [.a, b.]) * [.a, b, c.]) = ( [.a, c.] * ( [.a, b.] * [. [.a, b.], c.])) by GROUP_1:def 3

      .= ( [.a, c.] * ((((a " ) * (b " )) * (a * b)) * (((( [.a, b.] " ) * (c " )) * [.a, b.]) * c))) by Th16

      .= ( [.a, c.] * ((((a " ) * (b " )) * (a * b)) * ((( [.b, a.] * (c " )) * [.a, b.]) * c))) by Th22

      .= ( [.a, c.] * ((((a " ) * (b " )) * (a * b)) * ((((((b " ) * (a " )) * (b * a)) * (c " )) * [.a, b.]) * c))) by Th16

      .= ( [.a, c.] * (((a " ) * (b " )) * ((a * b) * ((((((b " ) * (a " )) * (b * a)) * (c " )) * [.a, b.]) * c)))) by GROUP_1:def 3

      .= ( [.a, c.] * (((a " ) * (b " )) * ((a * b) * (((((b " ) * (a " )) * (b * a)) * (c " )) * ( [.a, b.] * c))))) by GROUP_1:def 3

      .= ( [.a, c.] * (((a " ) * (b " )) * ((a * b) * ((((b " ) * (a " )) * (b * a)) * ((c " ) * ( [.a, b.] * c)))))) by GROUP_1:def 3

      .= ( [.a, c.] * (((a " ) * (b " )) * (((a * b) * (((b " ) * (a " )) * (b * a))) * ((c " ) * ( [.a, b.] * c))))) by GROUP_1:def 3

      .= ( [.a, c.] * (((a " ) * (b " )) * ((((a * b) * ((b " ) * (a " ))) * (b * a)) * ((c " ) * ( [.a, b.] * c))))) by GROUP_1:def 3

      .= ( [.a, c.] * (((a " ) * (b " )) * ((((a * b) * ((a * b) " )) * (b * a)) * ((c " ) * ( [.a, b.] * c))))) by GROUP_1: 17

      .= ( [.a, c.] * (((a " ) * (b " )) * ((( 1_ G) * (b * a)) * ((c " ) * ( [.a, b.] * c))))) by GROUP_1:def 5

      .= ( [.a, c.] * (((a " ) * (b " )) * ((b * a) * ((c " ) * ( [.a, b.] * c))))) by GROUP_1:def 4

      .= ( [.a, c.] * ((((a " ) * (b " )) * (b * a)) * ((c " ) * ( [.a, b.] * c)))) by GROUP_1:def 3

      .= ( [.a, c.] * ((((b * a) " ) * (b * a)) * ((c " ) * ( [.a, b.] * c)))) by GROUP_1: 17

      .= ( [.a, c.] * (( 1_ G) * ((c " ) * ( [.a, b.] * c)))) by GROUP_1:def 5

      .= ( [.a, c.] * ((c " ) * ( [.a, b.] * c))) by GROUP_1:def 4

      .= ((((a " ) * (c " )) * (a * c)) * ((c " ) * ( [.a, b.] * c))) by Th16

      .= ((((a " ) * (c " )) * (a * c)) * ((c " ) * (((a " ) * (((b " ) * a) * b)) * c))) by Th16

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

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

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

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

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

      .= ((((a " ) * (c " )) * ((a * c) * ((a * c) " ))) * ((((b " ) * a) * b) * c)) by GROUP_1: 17

      .= ((((a " ) * (c " )) * ( 1_ G)) * ((((b " ) * a) * b) * c)) by GROUP_1:def 5

      .= (((a " ) * (c " )) * ((((b " ) * a) * b) * c)) by GROUP_1:def 4

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

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

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

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

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

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

      .= (((a " ) * ((b * c) " )) * (a * (b * c))) by GROUP_1: 17;

      hence thesis by Th16;

    end;

    theorem :: GROUP_5:46

    ((( [.a, (b " ), c.] |^ b) * ( [.b, (c " ), a.] |^ c)) * ( [.c, (a " ), b.] |^ a)) = ( 1_ G)

    proof

      set d = (((a " ) * [.b, (c " ).]) * a);

      set e = (((c " ) * [.a, (b " ).]) * c);

      set f = (((b " ) * [.c, (a " ).]) * b);

      set x = ( [.a, (b " ), c.] |^ b);

      set y = ( [.b, (c " ), a.] |^ c);

      set z = ( [.c, (a " ), b.] |^ a);

      

       A1: [.(c " ), b.] = (((c " ) " ) * (((b " ) * (c " )) * b)) by Th16;

      

       A2: [.(a " ), c.] = (((a " ) " ) * (((c " ) * (a " )) * c)) by Th16;

      

       A3: [.(b " ), a.] = (((b " ) " ) * (((a " ) * (b " )) * a)) by Th16;

       [.a, (b " ), c.] = (( [.a, (b " ).] " ) * e) by Th16

      .= ( [.(b " ), a.] * e) by Th22;

      

      then

       A4: ( [.a, (b " ), c.] |^ b) = (((b " ) * (((b " ) " ) * ((((a " ) * (b " )) * a) * e))) * b) by A3, GROUP_1:def 3

      .= (((((a " ) * (b " )) * a) * e) * b) by GROUP_3: 1;

       [.c, (a " ), b.] = (( [.c, (a " ).] " ) * f) by Th16

      .= ( [.(a " ), c.] * f) by Th22;

      

      then

       A5: z = (((a " ) * (((a " ) " ) * ((((c " ) * (a " )) * c) * f))) * a) by A2, GROUP_1:def 3

      .= (((((c " ) * (a " )) * c) * f) * a) by GROUP_3: 1;

       [.b, (c " ), a.] = (( [.b, (c " ).] " ) * (((a " ) * [.b, (c " ).]) * a)) by Th16

      .= ( [.(c " ), b.] * (((a " ) * [.b, (c " ).]) * a)) by Th22;

      

      then ( [.b, (c " ), a.] |^ c) = (((c " ) * (((c " ) " ) * ((((b " ) * (c " )) * b) * d))) * c) by A1, GROUP_1:def 3

      .= (((((b " ) * (c " )) * b) * d) * c) by GROUP_3: 1

      .= ((((b " ) * (c " )) * b) * (d * c)) by GROUP_1:def 3

      .= (((b " ) * ((c " ) * b)) * (d * c)) by GROUP_1:def 3

      .= ((b " ) * (((c " ) * b) * (d * c))) by GROUP_1:def 3;

      

      then (x * y) = (((((a " ) * (b " )) * a) * e) * (b * ((b " ) * (((c " ) * b) * (d * c))))) by A4, GROUP_1:def 3

      .= (((((a " ) * (b " )) * a) * e) * (((c " ) * b) * (d * c))) by GROUP_3: 1

      .= (((((a " ) * (b " )) * a) * ((c " ) * ( [.a, (b " ).] * c))) * (((c " ) * b) * (d * c))) by GROUP_1:def 3

      .= ((((((a " ) * (b " )) * a) * (c " )) * ( [.a, (b " ).] * c)) * (((c " ) * b) * (d * c))) by GROUP_1:def 3

      .= (((((a " ) * (b " )) * a) * (c " )) * (( [.a, (b " ).] * c) * (((c " ) * b) * (d * c)))) by GROUP_1:def 3

      .= (((((a " ) * (b " )) * a) * (c " )) * ((( [.a, (b " ).] * c) * ((c " ) * b)) * (d * c))) by GROUP_1:def 3

      .= (((((a " ) * (b " )) * a) * (c " )) * (((( [.a, (b " ).] * c) * (c " )) * b) * (d * c))) by GROUP_1:def 3

      .= (((((a " ) * (b " )) * a) * (c " )) * ((((((a " ) * ((b " ) " )) * a) * (b " )) * b) * (d * c))) by GROUP_3: 1

      .= (((((a " ) * (b " )) * a) * (c " )) * ((((a " ) * ((b " ) " )) * a) * (d * c))) by GROUP_3: 1

      .= (((((a " ) * (b " )) * a) * (c " )) * ((((a " ) * ((b " ) " )) * a) * (((a " ) * [.b, (c " ).]) * (a * c)))) by GROUP_1:def 3

      .= (((((a " ) * (b " )) * a) * (c " )) * ((((a " ) * ((b " ) " )) * a) * ((a " ) * ( [.b, (c " ).] * (a * c))))) by GROUP_1:def 3

      .= (((((a " ) * (b " )) * a) * (c " )) * (((((a " ) * ((b " ) " )) * a) * (a " )) * ( [.b, (c " ).] * (a * c)))) by GROUP_1:def 3

      .= (((((a " ) * (b " )) * a) * (c " )) * (((a " ) * ((b " ) " )) * ( [.b, (c " ).] * (a * c)))) by GROUP_3: 1

      .= (((((a " ) * (b " )) * a) * (c " )) * ((((a " ) * ((b " ) " )) * [.b, (c " ).]) * (a * c))) by GROUP_1:def 3

      .= (((((a " ) * (b " )) * a) * (c " )) * ((((a " ) * ((b " ) " )) * ((b " ) * ((((c " ) " ) * b) * (c " )))) * (a * c))) by Th16

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

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

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

      .= (((((a " ) * (b " )) * a) * (c " )) * ((a " ) * (((((c " ) " ) * b) * (c " )) * (a * c)))) by GROUP_3: 1;

      

      then ((x * y) * z) = ((((((a " ) * (b " )) * a) * (c " )) * (((a " ) * ((((c " ) " ) * b) * (c " ))) * (a * c))) * (((((c " ) * (a " )) * c) * f) * a)) by A5, GROUP_1:def 3

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

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

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

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

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

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

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

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

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

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

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

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

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

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

      .= (((((((((a " ) * (b " )) * a) * (c " )) * (a " )) * ((c " ) " )) * b) * (c " )) * (((a * c) * ((a * c) " )) * (c * (f * a)))) by GROUP_1: 17

      .= (((((((((a " ) * (b " )) * a) * (c " )) * (a " )) * ((c " ) " )) * b) * (c " )) * (( 1_ G) * (c * (f * a)))) by GROUP_1:def 5

      .= (((((((((a " ) * (b " )) * a) * (c " )) * (a " )) * ((c " ) " )) * b) * (c " )) * (c * (f * a))) by GROUP_1:def 4

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

      .= ((((((((a " ) * (b " )) * a) * (c " )) * (a " )) * ((c " ) " )) * b) * (f * a)) by GROUP_3: 1

      .= ((((((((a " ) * (b " )) * a) * (c " )) * (a " )) * ((c " ) " )) * b) * (((b " ) * [.c, (a " ).]) * (b * a))) by GROUP_1:def 3

      .= ((((((((a " ) * (b " )) * a) * (c " )) * (a " )) * ((c " ) " )) * b) * ((b " ) * ( [.c, (a " ).] * (b * a)))) by GROUP_1:def 3

      .= (((((((((a " ) * (b " )) * a) * (c " )) * (a " )) * ((c " ) " )) * b) * (b " )) * ( [.c, (a " ).] * (b * a))) by GROUP_1:def 3

      .= (((((((a " ) * (b " )) * a) * (c " )) * (a " )) * ((c " ) " )) * ( [.c, (a " ).] * (b * a))) by GROUP_3: 1

      .= (((((((a " ) * (b " )) * a) * (c " )) * (a " )) * ((c " ) " )) * (((c " ) * ((((a " ) " ) * c) * (a " ))) * (b * a))) by Th16

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

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

      .= ((((((a " ) * (b " )) * a) * (c " )) * (a " )) * (((((a " ) " ) * c) * (a " )) * (b * a))) by GROUP_3: 1

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

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

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

      .= (((((a " ) * (b " )) * a) * (c " )) * ((c * (a " )) * (b * a))) by GROUP_3: 1

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

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

      .= (((((a " ) * (b " )) * (a * (c " ))) * (((c " ) " ) * (a " ))) * (b * a))

      .= (((((a " ) * (b " )) * (a * (c " ))) * ((a * (c " )) " )) * (b * a)) by GROUP_1: 17

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

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

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

      .= (((b * a) " ) * (b * a)) by GROUP_1: 17;

      hence thesis by GROUP_1:def 5;

    end;

    definition

      let G, A, B;

      :: GROUP_5:def4

      func commutators (A,B) -> Subset of G equals { [.a, b.] : a in A & b in B };

      coherence

      proof

        defpred P[ Element of G, Element of G] means $1 in A & $2 in B;

        deffunc F( Element of G, Element of G) = [.$1, $2.];

        { F(a,b) : P[a, b] } is Subset of G from DOMAIN_1:sch 9;

        hence thesis;

      end;

    end

    theorem :: GROUP_5:47

    

     Th47: x in ( commutators (A,B)) iff ex a, b st x = [.a, b.] & a in A & b in B;

    theorem :: GROUP_5:48

    ( commutators (( {} the carrier of G),A)) = {} & ( commutators (A,( {} the carrier of G))) = {}

    proof

      ( commutators (( {} the carrier of G),A)) c= {}

      proof

        let x be object;

        assume x in ( commutators (( {} the carrier of G),A));

        then ex a, b st x = [.a, b.] & a in ( {} the carrier of G) & b in A;

        hence thesis;

      end;

      hence ( commutators (( {} the carrier of G),A)) = {} ;

      thus ( commutators (A,( {} the carrier of G))) c= {}

      proof

        let x be object;

        assume x in ( commutators (A,( {} the carrier of G)));

        then ex a, b st x = [.a, b.] & a in A & b in ( {} the carrier of G);

        hence thesis;

      end;

      thus thesis;

    end;

    theorem :: GROUP_5:49

    ( commutators ( {a}, {b})) = { [.a, b.]}

    proof

      thus ( commutators ( {a}, {b})) c= { [.a, b.]}

      proof

        let x be object;

        assume x in ( commutators ( {a}, {b}));

        then

        consider c, d such that

         A1: x = [.c, d.] and

         A2: c in {a} & d in {b};

        c = a & b = d by A2, TARSKI:def 1;

        hence thesis by A1, TARSKI:def 1;

      end;

      let x be object;

      assume x in { [.a, b.]};

      then

       A3: x = [.a, b.] by TARSKI:def 1;

      a in {a} & b in {b} by TARSKI:def 1;

      hence thesis by A3;

    end;

    theorem :: GROUP_5:50

    

     Th50: A c= B & C c= D implies ( commutators (A,C)) c= ( commutators (B,D))

    proof

      assume

       A1: A c= B & C c= D;

      let x be object;

      assume x in ( commutators (A,C));

      then ex a, c st x = [.a, c.] & a in A & c in C;

      hence thesis by A1;

    end;

    theorem :: GROUP_5:51

    

     Th51: G is commutative Group iff for A, B st A <> {} & B <> {} holds ( commutators (A,B)) = {( 1_ G)}

    proof

      thus G is commutative Group implies for A, B st A <> {} & B <> {} holds ( commutators (A,B)) = {( 1_ G)}

      proof

        assume

         A1: G is commutative Group;

        let A, B;

        assume

         A2: A <> {} & B <> {} ;

        thus ( commutators (A,B)) c= {( 1_ G)}

        proof

          let x be object;

          assume x in ( commutators (A,B));

          then

          consider a, b such that

           A3: x = [.a, b.] and a in A and b in B;

          x = (((a " ) * ((b " ) * a)) * b) by A3, Th16

          .= (((a " ) * (a * (b " ))) * b) by A1, Lm1

          .= ((b " ) * b) by GROUP_3: 1

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

          hence thesis by TARSKI:def 1;

        end;

        set b = the Element of B;

        set a = the Element of A;

        reconsider a, b as Element of G by A2, TARSKI:def 3;

        let x be object;

        assume x in {( 1_ G)};

        then

         A4: x = ( 1_ G) by TARSKI:def 1;

         [.a, b.] = (((a " ) * ((b " ) * a)) * b) by Th16

        .= (((a " ) * (a * (b " ))) * b) by A1, Lm1

        .= ((b " ) * b) by GROUP_3: 1

        .= x by A4, GROUP_1:def 5;

        hence thesis by A2;

      end;

      assume

       A5: for A, B st A <> {} & B <> {} holds ( commutators (A,B)) = {( 1_ G)};

      G is commutative

      proof

        let a, b;

        a in {a} & b in {b} by TARSKI:def 1;

        then

         A6: [.a, b.] in ( commutators ( {a}, {b}));

        ( commutators ( {a}, {b})) = {( 1_ G)} by A5;

        then [.a, b.] = ( 1_ G) by A6, TARSKI:def 1;

        then (((a " ) * (b " )) * (a * b)) = ( 1_ G) by Th16;

        then (((b * a) " ) * (a * b)) = ( 1_ G) by GROUP_1: 17;

        then (a * b) = (((b * a) " ) " ) by GROUP_1: 12;

        hence thesis;

      end;

      hence thesis;

    end;

    definition

      let G, H1, H2;

      :: GROUP_5:def5

      func commutators (H1,H2) -> Subset of G equals ( commutators (( carr H1),( carr H2)));

      correctness ;

    end

    theorem :: GROUP_5:52

    

     Th52: x in ( commutators (H1,H2)) iff ex a, b st x = [.a, b.] & a in H1 & b in H2

    proof

      thus x in ( commutators (H1,H2)) implies ex a, b st x = [.a, b.] & a in H1 & b in H2

      proof

        assume x in ( commutators (H1,H2));

        then

        consider a, b such that

         A1: x = [.a, b.] and

         A2: a in ( carr H1) & b in ( carr H2);

        a in H1 & b in H2 by A2, STRUCT_0:def 5;

        hence thesis by A1;

      end;

      given a, b such that

       A3: x = [.a, b.] and

       A4: a in H1 & b in H2;

      a in ( carr H1) & b in ( carr H2) by A4, STRUCT_0:def 5;

      hence thesis by A3;

    end;

    theorem :: GROUP_5:53

    

     Th53: ( 1_ G) in ( commutators (H1,H2))

    proof

      

       A1: ( 1_ G) in H2 by GROUP_2: 46;

       [.( 1_ G), ( 1_ G).] = ( 1_ G) & ( 1_ G) in H1 by Th19, GROUP_2: 46;

      hence thesis by A1, Th52;

    end;

    theorem :: GROUP_5:54

    ( commutators (( (1). G),H)) = {( 1_ G)} & ( commutators (H,( (1). G))) = {( 1_ G)}

    proof

      

       A1: ( commutators (( (1). G),H)) c= {( 1_ G)}

      proof

        let x be object;

        assume x in ( commutators (( (1). G),H));

        then

        consider a, b such that

         A2: x = [.a, b.] and

         A3: a in ( (1). G) and b in H by Th52;

        a = ( 1_ G) by A3, Th1;

        then x = ( 1_ G) by A2, Th19;

        hence thesis by TARSKI:def 1;

      end;

      ( 1_ G) in ( commutators (( (1). G),H)) by Th53;

      hence ( commutators (( (1). G),H)) = {( 1_ G)} by A1, ZFMISC_1: 33;

      thus ( commutators (H,( (1). G))) c= {( 1_ G)}

      proof

        let x be object;

        assume x in ( commutators (H,( (1). G)));

        then

        consider a, b such that

         A4: x = [.a, b.] and a in H and

         A5: b in ( (1). G) by Th52;

        b = ( 1_ G) by A5, Th1;

        then x = ( 1_ G) by A4, Th19;

        hence thesis by TARSKI:def 1;

      end;

      ( 1_ G) in ( commutators (H,( (1). G))) by Th53;

      hence thesis by ZFMISC_1: 31;

    end;

    theorem :: GROUP_5:55

    

     Th55: for N be strict normal Subgroup of G holds ( commutators (H,N)) c= ( carr N) & ( commutators (N,H)) c= ( carr N)

    proof

      let N be strict normal Subgroup of G;

      thus ( commutators (H,N)) c= ( carr N)

      proof

        let x be object;

        assume x in ( commutators (H,N));

        then

        consider a, b such that

         A1: x = [.a, b.] and a in H and

         A2: b in N by Th52;

        (b " ) in N by A2, GROUP_2: 51;

        then ((b " ) |^ a) in (N |^ a) by GROUP_3: 58;

        then ((b " ) |^ a) in N by GROUP_3:def 13;

        then x in N by A1, A2, GROUP_2: 50;

        hence thesis by STRUCT_0:def 5;

      end;

      let x be object;

      assume x in ( commutators (N,H));

      then

      consider a, b such that

       A3: x = [.a, b.] and

       A4: a in N and b in H by Th52;

      (a |^ b) in (N |^ b) by A4, GROUP_3: 58;

      then

       A5: (a |^ b) in N by GROUP_3:def 13;

      x = ((a " ) * (a |^ b)) & (a " ) in N by A3, A4, Th16, GROUP_2: 51;

      then x in N by A5, GROUP_2: 50;

      hence thesis by STRUCT_0:def 5;

    end;

    theorem :: GROUP_5:56

    

     Th56: H1 is Subgroup of H2 & H3 is Subgroup of H4 implies ( commutators (H1,H3)) c= ( commutators (H2,H4))

    proof

      assume H1 is Subgroup of H2 & H3 is Subgroup of H4;

      then the carrier of H1 c= the carrier of H2 & the carrier of H3 c= the carrier of H4 by GROUP_2:def 5;

      hence thesis by Th50;

    end;

    theorem :: GROUP_5:57

    

     Th57: G is commutative Group iff for H1, H2 holds ( commutators (H1,H2)) = {( 1_ G)}

    proof

      thus G is commutative Group implies for H1, H2 holds ( commutators (H1,H2)) = {( 1_ G)} by Th51;

      assume

       A1: for H1, H2 holds ( commutators (H1,H2)) = {( 1_ G)};

      G is commutative

      proof

        let a, b;

        b in {b} by TARSKI:def 1;

        then

         A2: b in ( gr {b}) by GROUP_4: 29;

        a in {a} by TARSKI:def 1;

        then a in ( gr {a}) by GROUP_4: 29;

        then [.a, b.] in ( commutators (( gr {a}),( gr {b}))) by A2, Th52;

        then [.a, b.] in {( 1_ G)} by A1;

        then [.a, b.] = ( 1_ G) by TARSKI:def 1;

        hence thesis by Th36;

      end;

      hence thesis;

    end;

    definition

      let G;

      :: GROUP_5:def6

      func commutators G -> Subset of G equals ( commutators (( (Omega). G),( (Omega). G)));

      correctness ;

    end

    theorem :: GROUP_5:58

    

     Th58: x in ( commutators G) iff ex a, b st x = [.a, b.]

    proof

      thus x in ( commutators G) implies ex a, b st x = [.a, b.]

      proof

        assume x in ( commutators G);

        then ex a, b st x = [.a, b.] & a in ( (Omega). G) & b in ( (Omega). G) by Th52;

        hence thesis;

      end;

      given a, b such that

       A1: x = [.a, b.];

      thus thesis by A1;

    end;

    theorem :: GROUP_5:59

    G is commutative Group iff ( commutators G) = {( 1_ G)}

    proof

      thus G is commutative Group implies ( commutators G) = {( 1_ G)} by Th57;

      assume

       A1: ( commutators G) = {( 1_ G)};

      G is commutative

      proof

        let a, b;

         [.a, b.] in {( 1_ G)} by A1;

        then [.a, b.] = ( 1_ G) by TARSKI:def 1;

        hence thesis by Th36;

      end;

      hence thesis;

    end;

    definition

      let G, A, B;

      :: GROUP_5:def7

      func [.A,B.] -> strict Subgroup of G equals ( gr ( commutators (A,B)));

      correctness ;

    end

    theorem :: GROUP_5:60

    

     Th60: a in A & b in B implies [.a, b.] in [.A, B.]

    proof

      assume a in A & b in B;

      then [.a, b.] in ( commutators (A,B));

      hence thesis by GROUP_4: 29;

    end;

    theorem :: GROUP_5:61

    

     Th61: x in [.A, B.] iff ex F, I st ( len F) = ( len I) & ( rng F) c= ( commutators (A,B)) & x = ( Product (F |^ I))

    proof

      thus x in [.A, B.] implies ex F, I st ( len F) = ( len I) & ( rng F) c= ( commutators (A,B)) & x = ( Product (F |^ I))

      proof

        assume

         A1: x in [.A, B.];

        then x in G by GROUP_2: 40;

        then

        reconsider a = x as Element of G by STRUCT_0:def 5;

        a in ( gr ( commutators (A,B))) by A1;

        hence thesis by GROUP_4: 28;

      end;

      thus thesis by GROUP_4: 28;

    end;

    theorem :: GROUP_5:62

    A c= C & B c= D implies [.A, B.] is Subgroup of [.C, D.] by Th50, GROUP_4: 32;

    definition

      let G, H1, H2;

      :: GROUP_5:def8

      func [.H1,H2.] -> strict Subgroup of G equals [.( carr H1), ( carr H2).];

      correctness ;

    end

    theorem :: GROUP_5:63

     [.H1, H2.] = ( gr ( commutators (H1,H2)));

    theorem :: GROUP_5:64

    x in [.H1, H2.] iff ex F, I st ( len F) = ( len I) & ( rng F) c= ( commutators (H1,H2)) & x = ( Product (F |^ I)) by Th61;

    theorem :: GROUP_5:65

    

     Th65: a in H1 & b in H2 implies [.a, b.] in [.H1, H2.]

    proof

      assume a in H1 & b in H2;

      then a in ( carr H1) & b in ( carr H2) by STRUCT_0:def 5;

      hence thesis by Th60;

    end;

    theorem :: GROUP_5:66

    H1 is Subgroup of H2 & H3 is Subgroup of H4 implies [.H1, H3.] is Subgroup of [.H2, H4.]

    proof

      assume H1 is Subgroup of H2 & H3 is Subgroup of H4;

      then ( commutators (H1,H3)) c= ( commutators (H2,H4)) by Th56;

      hence thesis by GROUP_4: 32;

    end;

    theorem :: GROUP_5:67

    for N be strict normal Subgroup of G holds [.N, H.] is Subgroup of N & [.H, N.] is Subgroup of N

    proof

      let N be strict normal Subgroup of G;

      now

        let a;

        assume a in [.N, H.];

        then

        consider F, I such that

         A1: ( len F) = ( len I) and

         A2: ( rng F) c= ( commutators (N,H)) and

         A3: a = ( Product (F |^ I)) by Th61;

        ( commutators (N,H)) c= ( carr N) by Th55;

        then ( rng F) c= ( carr N) by A2;

        then a in ( gr ( carr N)) by A1, A3, GROUP_4: 28;

        hence a in N by GROUP_4: 31;

      end;

      hence [.N, H.] is Subgroup of N by GROUP_2: 58;

      now

        let a;

        assume a in [.H, N.];

        then

        consider F, I such that

         A4: ( len F) = ( len I) and

         A5: ( rng F) c= ( commutators (H,N)) and

         A6: a = ( Product (F |^ I)) by Th61;

        ( commutators (H,N)) c= ( carr N) by Th55;

        then ( rng F) c= ( carr N) by A5;

        then a in ( gr ( carr N)) by A4, A6, GROUP_4: 28;

        hence a in N by GROUP_4: 31;

      end;

      hence thesis by GROUP_2: 58;

    end;

    theorem :: GROUP_5:68

    

     Th68: for N1,N2 be strict normal Subgroup of G holds [.N1, N2.] is normal Subgroup of G

    proof

      let N1,N2 be strict normal Subgroup of G;

      now

        let a;

        now

          let b;

          assume b in ( [.N1, N2.] |^ a);

          then

          consider c such that

           A1: b = (c |^ a) and

           A2: c in [.N1, N2.] by GROUP_3: 58;

          consider F, I such that

           A3: ( len F) = ( len I) and

           A4: ( rng F) c= ( commutators (( carr N1),( carr N2))) and

           A5: c = ( Product (F |^ I)) by A2, GROUP_4: 28;

          

           A6: ( len (F |^ a)) = ( len F) by Def1;

          

           A7: ( rng (F |^ a)) c= ( commutators (( carr N1),( carr N2)))

          proof

            let x be object;

            assume x in ( rng (F |^ a));

            then

            consider y be object such that

             A8: y in ( dom (F |^ a)) and

             A9: ((F |^ a) . y) = x by FUNCT_1:def 3;

            reconsider y as Element of NAT by A8;

            

             A10: y in ( dom F) by A6, A8, FINSEQ_3: 29;

            then

             A11: (F . y) = (F /. y) by PARTFUN1:def 6;

            y in ( dom F) by A6, A8, FINSEQ_3: 29;

            then (F . y) in ( rng F) by FUNCT_1:def 3;

            then

            consider d, e such that

             A12: (F . y) = [.d, e.] and

             A13: d in ( carr N1) and

             A14: e in ( carr N2) by A4, Th47;

            d in N1 by A13, STRUCT_0:def 5;

            then (d |^ a) in (N1 |^ a) by GROUP_3: 58;

            then (d |^ a) in N1 by GROUP_3:def 13;

            then

             A15: (d |^ a) in ( carr N1) by STRUCT_0:def 5;

            e in N2 by A14, STRUCT_0:def 5;

            then (e |^ a) in (N2 |^ a) by GROUP_3: 58;

            then (e |^ a) in N2 by GROUP_3:def 13;

            then

             A16: (e |^ a) in ( carr N2) by STRUCT_0:def 5;

            x = ((F /. y) |^ a) by A9, A10, Def1;

            then x = [.(d |^ a), (e |^ a).] by A12, A11, Th23;

            hence thesis by A15, A16;

          end;

          b = ( Product ((F |^ I) |^ a)) by A1, A5, Th14

          .= ( Product ((F |^ a) |^ I)) by Th15;

          hence b in [.N1, N2.] by A3, A6, A7, GROUP_4: 28;

        end;

        hence ( [.N1, N2.] |^ a) is Subgroup of [.N1, N2.] by GROUP_2: 58;

      end;

      hence thesis by GROUP_3: 122;

    end;

    

     Lm2: [.N1, N2.] is Subgroup of [.N2, N1.]

    proof

      now

        let a;

        assume a in [.N1, N2.];

        then

        consider F, I such that ( len F) = ( len I) and

         A1: ( rng F) c= ( commutators (N1,N2)) and

         A2: a = ( Product (F |^ I)) by Th61;

        deffunc F( Nat) = ((F /. $1) " );

        consider F1 such that

         A3: ( len F1) = ( len F) and

         A4: for k be Nat st k in ( dom F1) holds (F1 . k) = F(k) from FINSEQ_2:sch 1;

        

         A5: ( dom F) = ( Seg ( len F)) by FINSEQ_1:def 3;

        

         A6: ( rng F1) c= ( commutators (N2,N1))

        proof

          let x be object;

          assume x in ( rng F1);

          then

          consider y be object such that

           A7: y in ( dom F1) and

           A8: (F1 . y) = x by FUNCT_1:def 3;

          reconsider y as Element of NAT by A7;

          y in ( dom F) by A3, A7, FINSEQ_3: 29;

          then

           A9: (F /. y) = (F . y) by PARTFUN1:def 6;

          y in ( dom F) by A3, A7, FINSEQ_3: 29;

          then (F . y) in ( rng F) by FUNCT_1:def 3;

          then

          consider b, c such that

           A10: (F . y) = [.b, c.] and

           A11: b in N1 & c in N2 by A1, Th52;

          x = ((F /. y) " ) by A4, A7, A8;

          then x = [.c, b.] by A10, A9, Th22;

          hence thesis by A11, Th52;

        end;

        

         A12: ( len (F |^ I)) = ( len F) by GROUP_4:def 3;

        then

         A13: ( dom (F |^ I)) = ( Seg ( len F)) by FINSEQ_1:def 3;

        deffunc F( Nat) = ( @ ( - ( @ (I /. $1))));

        consider I1 such that

         A14: ( len I1) = ( len F) and

         A15: for k be Nat st k in ( dom I1) holds (I1 . k) = F(k) from FINSEQ_2:sch 1;

        set J = (F1 |^ I1);

        

         A16: ( dom F1) = ( dom F) by A3, FINSEQ_3: 29;

        

         A17: ( dom I1) = ( dom F) by A14, FINSEQ_3: 29;

         A18:

        now

          let k be Nat;

          assume

           A19: k in ( dom (F |^ I));

          then

           A20: k in ( dom F) by A13, FINSEQ_1:def 3;

          

           A21: (J . k) = ((F1 /. k) |^ ( @ (I1 /. k))) & (F1 /. k) = (F1 . k) by A5, A16, A13, A19, GROUP_4:def 3, PARTFUN1:def 6;

          

           A22: (I1 . k) = ( @ ( - ( @ (I /. k)))) by A15, A5, A17, A13, A19;

          (F1 . k) = ((F /. k) " ) & (I1 . k) = (I1 /. k) by A4, A5, A16, A17, A13, A19, PARTFUN1:def 6;

          

          then (J . k) = ((((F /. k) " ) |^ ( @ (I /. k))) " ) by A21, A22, GROUP_1: 36

          .= ((((F /. k) |^ ( @ (I /. k))) " ) " ) by GROUP_1: 37

          .= ((F /. k) |^ ( @ (I /. k)));

          hence ((F |^ I) . k) = (J . k) by A20, GROUP_4:def 3;

        end;

        ( len J) = ( len F) by A3, GROUP_4:def 3;

        then J = (F |^ I) by A12, A18, FINSEQ_2: 9;

        hence a in [.N2, N1.] by A2, A3, A14, A6, Th61;

      end;

      hence thesis by GROUP_2: 58;

    end;

    theorem :: GROUP_5:69

    

     Th69: [.N1, N2.] = [.N2, N1.]

    proof

       [.N1, N2.] is Subgroup of [.N2, N1.] & [.N2, N1.] is Subgroup of [.N1, N2.] by Lm2;

      hence thesis by GROUP_2: 55;

    end;

    theorem :: GROUP_5:70

    

     Th70: for N1,N2,N3 be strict normal Subgroup of G holds [.(N1 "\/" N2), N3.] = ( [.N1, N3.] "\/" [.N2, N3.])

    proof

      let N1,N2,N3 be strict normal Subgroup of G;

      

       A1: [.N1, N3.] is normal Subgroup of G by Th68;

      

       A2: [.N2, N3.] is normal Subgroup of G by Th68;

      now

        let a;

        

         A3: N3 is Subgroup of N3 by GROUP_2: 54;

        N2 is Subgroup of (N1 "\/" N2) by GROUP_4: 60;

        then

         A4: ( commutators (N2,N3)) c= ( commutators ((N1 "\/" N2),N3)) by A3, Th56;

        assume a in ( [.N1, N3.] "\/" [.N2, N3.]);

        then

        consider b, c such that

         A5: a = (b * c) and

         A6: b in [.N1, N3.] and

         A7: c in [.N2, N3.] by A1, A2, Th7;

        consider F1, I1 such that

         A8: ( len F1) = ( len I1) and

         A9: ( rng F1) c= ( commutators (N1,N3)) and

         A10: b = ( Product (F1 |^ I1)) by A6, Th61;

        consider F2, I2 such that

         A11: ( len F2) = ( len I2) and

         A12: ( rng F2) c= ( commutators (N2,N3)) and

         A13: c = ( Product (F2 |^ I2)) by A7, Th61;

        

         A14: ( len (F1 ^ F2)) = (( len I1) + ( len I2)) by A8, A11, FINSEQ_1: 22

        .= ( len (I1 ^ I2)) by FINSEQ_1: 22;

        ( rng (F1 ^ F2)) = (( rng F1) \/ ( rng F2)) by FINSEQ_1: 31;

        then

         A15: ( rng (F1 ^ F2)) c= (( commutators (N1,N3)) \/ ( commutators (N2,N3))) by A9, A12, XBOOLE_1: 13;

        N1 is Subgroup of (N1 "\/" N2) by GROUP_4: 60;

        then ( commutators (N1,N3)) c= ( commutators ((N1 "\/" N2),N3)) by A3, Th56;

        then (( commutators (N1,N3)) \/ ( commutators (N2,N3))) c= ( commutators ((N1 "\/" N2),N3)) by A4, XBOOLE_1: 8;

        then

         A16: ( rng (F1 ^ F2)) c= ( commutators ((N1 "\/" N2),N3)) by A15;

        ( Product ((F1 ^ F2) |^ (I1 ^ I2))) = ( Product ((F1 |^ I1) ^ (F2 |^ I2))) by A8, A11, GROUP_4: 19

        .= a by A5, A10, A13, GROUP_4: 5;

        hence a in [.(N1 "\/" N2), N3.] by A16, A14, Th61;

      end;

      then

       A17: ( [.N1, N3.] "\/" [.N2, N3.]) is Subgroup of [.(N1 "\/" N2), N3.] by GROUP_2: 58;

      ( commutators ((N1 "\/" N2),N3)) c= ( [.N1, N3.] * [.N2, N3.])

      proof

        let x be object;

        assume x in ( commutators ((N1 "\/" N2),N3));

        then

        consider a, b such that

         A18: x = [.a, b.] and

         A19: a in (N1 "\/" N2) and

         A20: b in N3 by Th52;

        consider c, d such that

         A21: a = (c * d) and

         A22: c in N1 and

         A23: d in N2 by A19, Th7;

         [.c, b.] in [.N1, N3.] by A20, A22, Th65;

        then ( [.c, b.] |^ d) in ( [.N1, N3.] |^ d) by GROUP_3: 58;

        then

         A24: ( [.c, b.] |^ d) in [.N1, N3.] by A1, GROUP_3:def 13;

        x = (( [.c, b.] |^ d) * [.d, b.]) & [.d, b.] in [.N2, N3.] by A18, A20, A21, A23, Th25, Th65;

        hence thesis by A24, Th4;

      end;

      then ( gr ( commutators ((N1 "\/" N2),N3))) is Subgroup of ( gr ( [.N1, N3.] * [.N2, N3.])) by GROUP_4: 32;

      then [.(N1 "\/" N2), N3.] is Subgroup of ( [.N1, N3.] "\/" [.N2, N3.]) by GROUP_4: 50;

      hence thesis by A17, GROUP_2: 55;

    end;

    theorem :: GROUP_5:71

    for N1,N2,N3 be strict normal Subgroup of G holds [.N1, (N2 "\/" N3).] = ( [.N1, N2.] "\/" [.N1, N3.])

    proof

      let N1,N2,N3 be strict normal Subgroup of G;

      (N2 "\/" N3) is normal Subgroup of G by GROUP_4: 54;

      

      hence [.N1, (N2 "\/" N3).] = [.(N2 "\/" N3), N1.] by Th69

      .= ( [.N2, N1.] "\/" [.N3, N1.]) by Th70

      .= ( [.N1, N2.] "\/" [.N3, N1.]) by Th69

      .= ( [.N1, N2.] "\/" [.N1, N3.]) by Th69;

    end;

    definition

      let G be Group;

      :: GROUP_5:def9

      func G ` -> strict normal Subgroup of G equals [.( (Omega). G), ( (Omega). G).];

      coherence

      proof

        ( (Omega). G) is normal Subgroup of G by GROUP_3: 114;

        hence thesis by Th68;

      end;

    end

    theorem :: GROUP_5:72

    for G be Group holds (G ` ) = ( gr ( commutators G));

    theorem :: GROUP_5:73

    

     Th73: for G be Group holds x in (G ` ) iff ex F be FinSequence of the carrier of G, I st ( len F) = ( len I) & ( rng F) c= ( commutators G) & x = ( Product (F |^ I))

    proof

      let G be Group;

      thus x in (G ` ) implies ex F be FinSequence of the carrier of G, I st ( len F) = ( len I) & ( rng F) c= ( commutators G) & x = ( Product (F |^ I))

      proof

        assume

         A1: x in (G ` );

        then x in G by GROUP_2: 40;

        then

        reconsider a = x as Element of G by STRUCT_0:def 5;

        ex F be FinSequence of the carrier of G, I st ( len F) = ( len I) & ( rng F) c= ( commutators G) & a = ( Product (F |^ I)) by A1, GROUP_4: 28;

        hence thesis;

      end;

      given F be FinSequence of the carrier of G, I such that

       A2: ( len F) = ( len I) & ( rng F) c= ( commutators G) & x = ( Product (F |^ I));

      thus thesis by A2, GROUP_4: 28;

    end;

    theorem :: GROUP_5:74

    

     Th74: for G be strict Group, a,b be Element of G holds [.a, b.] in (G ` )

    proof

      let G be strict Group, a,b be Element of G;

      a in ( (Omega). G) & b in ( (Omega). G) by STRUCT_0:def 5;

      hence thesis by Th65;

    end;

    theorem :: GROUP_5:75

    for G be strict Group holds G is commutative Group iff (G ` ) = ( (1). G)

    proof

      let G be strict Group;

      thus G is commutative Group implies (G ` ) = ( (1). G)

      proof

        assume

         A1: G is commutative Group;

        now

          let a be Element of G;

          assume a in (G ` );

          then a in ( gr {( 1_ G)}) by A1, Th51;

          then a in ( gr ( {( 1_ G)} \ {( 1_ G)})) by GROUP_4: 35;

          then a in ( gr ( {} the carrier of G)) by XBOOLE_1: 37;

          hence a in ( (1). G) by GROUP_4: 30;

        end;

        then

         A2: (G ` ) is Subgroup of ( (1). G) by GROUP_2: 58;

        ( (1). G) is Subgroup of (G ` ) by GROUP_2: 65;

        hence thesis by A2, GROUP_2: 55;

      end;

      assume

       A3: (G ` ) = ( (1). G);

      G is commutative

      proof

        let a,b be Element of G;

         [.a, b.] in (G ` ) by Th74;

        then [.a, b.] = ( 1_ G) by A3, Th1;

        hence thesis by Th36;

      end;

      hence thesis;

    end;

    theorem :: GROUP_5:76

    for G be Group, H be strict Subgroup of G holds ( Left_Cosets H) is finite & ( index H) = 2 implies (G ` ) is Subgroup of H

    proof

      let G be Group, H be strict Subgroup of G;

      assume that

       A1: ( Left_Cosets H) is finite and

       A2: ( index H) = 2;

      

       A3: H is normal Subgroup of G by A1, A2, GROUP_3: 128;

      now

        let a be Element of G;

        assume a in (G ` );

        then

        consider F be FinSequence of the carrier of G, I such that

         A4: ( len F) = ( len I) and

         A5: ( rng F) c= ( commutators G) and

         A6: a = ( Product (F |^ I)) by Th73;

        ( rng F) c= ( carr H)

        proof

          ex B be finite set st B = ( Left_Cosets H) & ( index H) = ( card B) by A1, GROUP_2: 146;

          then

          consider x,y be object such that x <> y and

           A7: ( Left_Cosets H) = {x, y} by A2, CARD_2: 60;

          x in ( Left_Cosets H) by A7, TARSKI:def 2;

          then

          consider d be Element of G such that

           A8: x = (d * H) by GROUP_2:def 15;

          y in ( Left_Cosets H) by A7, TARSKI:def 2;

          then

          consider e be Element of G such that

           A9: y = (e * H) by GROUP_2:def 15;

          ( carr H) in ( Left_Cosets H) by GROUP_2: 135;

          then ( Left_Cosets H) = {( carr H), (e * H)} or ( Left_Cosets H) = {(d * H), ( carr H)} by A7, A8, A9, TARSKI:def 2;

          then

          consider c be Element of G such that

           A10: ( Left_Cosets H) = {( carr H), (c * H)};

          let X be object;

          assume X in ( rng F);

          then

          consider a,b be Element of G such that

           A11: X = [.a, b.] by A5, Th58;

          b in the carrier of G;

          then b in ( union ( Left_Cosets H)) by GROUP_2: 137;

          then

           A12: b in (( carr H) \/ (c * H)) by A10, ZFMISC_1: 75;

          a in the carrier of G;

          then a in ( union ( Left_Cosets H)) by GROUP_2: 137;

          then

           A13: a in (( carr H) \/ (c * H)) by A10, ZFMISC_1: 75;

          now

            per cases by A13, A12, XBOOLE_0:def 3;

              suppose a in ( carr H) & b in ( carr H);

              then a in H & b in H by STRUCT_0:def 5;

              then X in H by A11, Th38;

              hence thesis by STRUCT_0:def 5;

            end;

              suppose a in ( carr H) & b in (c * H);

              then a in H by STRUCT_0:def 5;

              then (a |^ b) in H & (a " ) in H by A3, Th3, GROUP_2: 51;

              then ((a " ) * (a |^ b)) in H by GROUP_2: 50;

              then X in H by A11, Th16;

              hence thesis by STRUCT_0:def 5;

            end;

              suppose a in (c * H) & b in ( carr H);

              then

               A14: b in H by STRUCT_0:def 5;

              then (b " ) in H by GROUP_2: 51;

              then ((b " ) |^ a) in H by A3, Th3;

              then (((b " ) |^ a) * b) in H by A14, GROUP_2: 50;

              hence thesis by A11, STRUCT_0:def 5;

            end;

              suppose

               A15: a in (c * H) & b in (c * H);

              then

              consider d be Element of G such that

               A16: a = (c * d) and

               A17: d in H by GROUP_2: 103;

              consider e be Element of G such that

               A18: b = (c * e) and

               A19: e in H by A15, GROUP_2: 103;

              (e " ) in H by A19, GROUP_2: 51;

              then

               A20: ((e " ) |^ c) in H by A3, Th3;

              (d " ) in H by A17, GROUP_2: 51;

              then

               A21: ((d " ) * ((e " ) |^ c)) in H by A20, GROUP_2: 50;

              (d |^ c) in H by A3, A17, Th3;

              then

               A22: ((d |^ c) * e) in H by A19, GROUP_2: 50;

               [.a, b.] = (((a " ) * (b " )) * (a * b)) by Th16

              .= ((((d " ) * (c " )) * (b " )) * ((c * d) * (c * e))) by A16, A18, GROUP_1: 17

              .= ((((d " ) * (c " )) * ((e " ) * (c " ))) * ((c * d) * (c * e))) by A18, GROUP_1: 17

              .= (((((d " ) * (c " )) * (e " )) * (c " )) * ((c * d) * (c * e))) by GROUP_1:def 3

              .= (((((d " ) * (c " )) * (e " )) * (c " )) * (c * (d * (c * e)))) by GROUP_1:def 3

              .= ((((((d " ) * (c " )) * (e " )) * (c " )) * c) * (d * (c * e))) by GROUP_1:def 3

              .= (((((d " ) * (c " )) * (e " )) * ((c " ) * c)) * (d * (c * e))) by GROUP_1:def 3

              .= (((((d " ) * (c " )) * (e " )) * ( 1_ G)) * (d * (c * e))) by GROUP_1:def 5

              .= (((((d " ) * (c " )) * (e " )) * (c * (c " ))) * (d * (c * e))) by GROUP_1:def 5

              .= ((((((d " ) * (c " )) * (e " )) * c) * (c " )) * (d * (c * e))) by GROUP_1:def 3

              .= (((((d " ) * ((c " ) * (e " ))) * c) * (c " )) * (d * (c * e))) by GROUP_1:def 3

              .= ((((d " ) * ((e " ) |^ c)) * (c " )) * (d * (c * e))) by GROUP_1:def 3

              .= ((((d " ) * ((e " ) |^ c)) * (c " )) * ((d * c) * e)) by GROUP_1:def 3

              .= (((d " ) * ((e " ) |^ c)) * ((c " ) * ((d * c) * e))) by GROUP_1:def 3

              .= (((d " ) * ((e " ) |^ c)) * ((c " ) * (d * (c * e)))) by GROUP_1:def 3

              .= (((d " ) * ((e " ) |^ c)) * (((c " ) * d) * (c * e))) by GROUP_1:def 3

              .= (((d " ) * ((e " ) |^ c)) * ((d |^ c) * e)) by GROUP_1:def 3;

              then X in H by A11, A21, A22, GROUP_2: 50;

              hence thesis by STRUCT_0:def 5;

            end;

          end;

          hence thesis;

        end;

        then a in ( gr ( carr H)) by A4, A6, GROUP_4: 28;

        hence a in H by GROUP_4: 31;

      end;

      hence thesis by GROUP_2: 58;

    end;

    begin

    definition

      let G;

      :: GROUP_5:def10

      func center G -> strict Subgroup of G means

      : Def10: the carrier of it = { a : for b holds (a * b) = (b * a) };

      existence

      proof

        defpred P[ Element of G] means for b holds ($1 * b) = (b * $1);

        reconsider A = { a : P[a] } as Subset of G from DOMAIN_1:sch 7;

         A1:

        now

          let a, b;

          assume that

           A2: a in A and

           A3: b in A;

          consider c such that

           A4: c = a and

           A5: for b holds (c * b) = (b * c) by A2;

          consider d such that

           A6: d = b and

           A7: for a holds (d * a) = (a * d) by A3;

          now

            let e;

            

            thus ((a * b) * e) = (a * (b * e)) by GROUP_1:def 3

            .= (a * (e * d)) by A6, A7

            .= ((a * e) * b) by A6, GROUP_1:def 3

            .= ((e * c) * b) by A4, A5

            .= (e * (a * b)) by A4, GROUP_1:def 3;

          end;

          hence (a * b) in A;

        end;

         A8:

        now

          let a;

          assume a in A;

          then

          consider b such that

           A9: b = a and

           A10: for c holds (b * c) = (c * b);

          now

            let c;

            

            thus ((a " ) * c) = ((((a " ) * c) " ) " )

            .= (((c " ) * ((a " ) " )) " ) by GROUP_1: 17

            .= (((c " ) * b) " ) by A9

            .= ((b * (c " )) " ) by A10

            .= ((((a " ) " ) * (c " )) " ) by A9

            .= (((c * (a " )) " ) " ) by GROUP_1: 17

            .= (c * (a " ));

          end;

          hence (a " ) in A;

        end;

        now

          let b;

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

          hence (( 1_ G) * b) = (b * ( 1_ G)) by GROUP_1:def 4;

        end;

        then ( 1_ G) in A;

        hence thesis by A1, A8, GROUP_2: 52;

      end;

      uniqueness by GROUP_2: 59;

    end

    theorem :: GROUP_5:77

    

     Th77: a in ( center G) iff for b holds (a * b) = (b * a)

    proof

      thus a in ( center G) implies for b holds (a * b) = (b * a)

      proof

        assume a in ( center G);

        then a in the carrier of ( center G) by STRUCT_0:def 5;

        then a in { b : for c holds (b * c) = (c * b) } by Def10;

        then ex b st a = b & for c holds (b * c) = (c * b);

        hence thesis;

      end;

      assume for b holds (a * b) = (b * a);

      then a in { c : for b holds (c * b) = (b * c) };

      then a in the carrier of ( center G) by Def10;

      hence thesis by STRUCT_0:def 5;

    end;

    theorem :: GROUP_5:78

    ( center G) is normal Subgroup of G

    proof

      now

        let a;

        thus (a * ( center G)) c= (( center G) * a)

        proof

          let x be object;

          assume x in (a * ( center G));

          then

          consider b such that

           A1: x = (a * b) and

           A2: b in ( center G) by GROUP_2: 103;

          x = (b * a) by A1, A2, Th77;

          hence thesis by A2, GROUP_2: 104;

        end;

      end;

      hence thesis by GROUP_3: 118;

    end;

    theorem :: GROUP_5:79

    for H be Subgroup of G holds H is Subgroup of ( center G) implies H is normal Subgroup of G

    proof

      let H be Subgroup of G;

      assume

       A1: H is Subgroup of ( center G);

      now

        let a;

        thus (H * a) c= (a * H)

        proof

          let x be object;

          assume x in (H * a);

          then

          consider b such that

           A2: x = (b * a) and

           A3: b in H by GROUP_2: 104;

          b in ( center G) by A1, A3, GROUP_2: 40;

          then x = (a * b) by A2, Th77;

          hence thesis by A3, GROUP_2: 103;

        end;

      end;

      hence thesis by GROUP_3: 119;

    end;

    theorem :: GROUP_5:80

    ( center G) is commutative

    proof

      let a,b be Element of ( center G);

      reconsider x = a, y = b as Element of G by GROUP_2: 42;

      

       A1: a in ( center G) by STRUCT_0:def 5;

      

      thus (a * b) = (x * y) by GROUP_2: 43

      .= (y * x) by A1, Th77

      .= (b * a) by GROUP_2: 43;

    end;

    theorem :: GROUP_5:81

    a in ( center G) iff ( con_class a) = {a}

    proof

      thus a in ( center G) implies ( con_class a) = {a}

      proof

        assume

         A1: a in ( center G);

        thus ( con_class a) c= {a}

        proof

          let x be object;

          assume x in ( con_class a);

          then

          consider b such that

           A2: b = x and

           A3: (a,b) are_conjugated by GROUP_3: 80;

          consider c such that

           A4: a = (b |^ c) by A3;

          a = ((c " ) * (b * c)) by A4, GROUP_1:def 3;

          then (c * a) = (b * c) by GROUP_1: 13;

          then (a * c) = (b * c) by A1, Th77;

          then a = b by GROUP_1: 6;

          hence thesis by A2, TARSKI:def 1;

        end;

        a in ( con_class a) by GROUP_3: 83;

        hence thesis by ZFMISC_1: 31;

      end;

      assume

       A5: ( con_class a) = {a};

      now

        let b;

        (a |^ b) in ( con_class a) by GROUP_3: 82;

        then (a |^ b) = a by A5, TARSKI:def 1;

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

        hence (a * b) = (b * a) by GROUP_1: 13;

      end;

      hence thesis by Th77;

    end;

    theorem :: GROUP_5:82

    for G be strict Group holds G is commutative Group iff ( center G) = G

    proof

      let G be strict Group;

      thus G is commutative Group implies ( center G) = G

      proof

        assume

         A1: G is commutative Group;

        now

          let a be Element of G;

          for b be Element of G holds (a * b) = (b * a) by A1, Lm1;

          hence a in ( center G) by Th77;

        end;

        hence thesis by GROUP_2: 62;

      end;

      assume

       A2: ( center G) = G;

      G is commutative by STRUCT_0:def 5, A2, Th77;

      hence thesis;

    end;