grnilp_1.miz



    begin

    reserve x,y for set,

G for Group,

A,B,H,H1,H2 for Subgroup of G,

a,b,c for Element of G,

F,F1 for FinSequence of the carrier of G,

I,I1 for FinSequence of INT ,

i,j for Element of NAT ;

    theorem :: GRNILP_1:1

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

    proof

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

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

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

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

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

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

      hence thesis;

    end;

    theorem :: GRNILP_1:2

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

    proof

      

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

      .= (((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))) by GROUP_1:def 3

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

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

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

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

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

    end;

    theorem :: GRNILP_1:3

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

    proof

      

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

      .= (((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))) by GROUP_1:def 3

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

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

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

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

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

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

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

      .= ( [.(a " ), b.] |^ a) by GROUP_5: 16;

    end;

    theorem :: GRNILP_1:4

    

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

    proof

      

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

      .= ( [.(b " ), a.] |^ b) by GROUP_5: 22;

    end;

    theorem :: GRNILP_1:5

    

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

    proof

      

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

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

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

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

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

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

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

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

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

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

      .= (( [.(b " ), a.] |^ b) * (( [.a, (b " ).] |^ c) |^ b)) by GROUP_5: 22

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

      hence thesis by A1;

    end;

    theorem :: GRNILP_1:6

    

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

    proof

      

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

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

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

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

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

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

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

      .= [.b, a.];

    end;

    theorem :: GRNILP_1:7

    

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

    proof

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

      hence thesis by Th6;

    end;

    theorem :: GRNILP_1:8

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

    proof

       [.a, b, (c |^ a).] = ( [.b, (a " ), c.] |^ a) & [.c, a, (b |^ c).] = ( [.a, (c " ), b.] |^ c) & [.b, c, (a |^ b).] = ( [.c, (b " ), a.] |^ b) by Th7;

      hence thesis by GROUP_5: 46;

    end;

    theorem :: GRNILP_1:9

    

     Th9: [.A, B.] is Subgroup of [.B, A.]

    proof

      now

        let a;

        assume a in [.A, B.];

        then

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

         A1: ( rng F) c= ( commutators (A,B)) and

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

        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 F1) = ( Seg ( len F)) by A3, FINSEQ_1:def 3;

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

        consider I1 such that

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

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

        

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

        

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

        

         A10: ( dom I1) = ( dom F) by A6, FINSEQ_3: 29;

        set J = (F1 |^ I1);

        

         A11: ( len J) = ( len F) & ( len (F |^ I)) = ( len F) by A3, GROUP_4:def 3;

        then

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

        now

          let k be Nat;

          assume

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

          then

           A14: k in ( dom F) by A12, FINSEQ_1:def 3;

          (J . k) = ((F1 /. k) |^ ( @ (I1 /. k))) & (F1 /. k) = (F1 . k) & (F1 . k) = ((F /. k) " ) & (I1 . k) = (I1 /. k) & ( @ (I1 /. k)) = (I1 /. k) & (I1 . k) = ( @ ( - ( @ (I /. k)))) & ( @ ( - ( @ (I /. k)))) = ( - ( @ (I /. k))) by A4, A7, A8, A9, A10, A13, A12, GROUP_4:def 3, PARTFUN1:def 6;

          

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

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

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

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

        end;

        then

         A15: J = (F |^ I) by A11, FINSEQ_2: 9;

        ( rng F1) c= ( commutators (B,A))

        proof

          let x be object;

          assume x in ( rng F1);

          then

          consider y be object such that

           A16: y in ( dom F1) and

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

          reconsider y as Element of NAT by A16;

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

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

          then

          consider b, c such that

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

           A19: b in A & c in B by A1, GROUP_5: 52;

          x = ((F /. y) " ) & (F /. y) = (F . y) by A16, A4, A8, A17, A5, PARTFUN1:def 6;

          then x = [.c, b.] by A18, GROUP_5: 22;

          hence thesis by A19, GROUP_5: 52;

        end;

        hence a in [.B, A.] by A2, A3, A6, A15, GROUP_5: 61;

      end;

      hence thesis by GROUP_2: 58;

    end;

    definition

      let G, A, B;

      :: original: [.

      redefine

      func [.A,B.];

      commutativity

      proof

        let A, B;

         [.A, B.] is Subgroup of [.B, A.] & [.B, A.] is Subgroup of [.A, B.] by Th9;

        hence thesis by GROUP_2: 55;

      end;

    end

    theorem :: GRNILP_1:10

    

     Th10: B is Subgroup of A implies ( commutators (A,B)) c= ( carr A)

    proof

      assume

       A1: B is Subgroup of A;

      let x be object;

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

      then

      consider a, b such that

       A2: x = [.a, b.] & a in A & b in B by GROUP_5: 52;

      

       A3: b in A by A1, A2, GROUP_2: 40;

      then

       A4: (a * b) in A by A2, GROUP_2: 50;

      (a " ) in A & (b " ) in A by A2, A3, GROUP_2: 51;

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

      then

       A5: (((a " ) * (b " )) * (a * b)) in A by A4, GROUP_2: 50;

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

      hence thesis by A2, A5, STRUCT_0:def 5;

    end;

    

     Lm1: ( gr ( carr A)) is Subgroup of A

    proof

      set A9 = multMagma (# the carrier of A, the multF of A #);

      the carrier of A9 c= the carrier of G & the multF of A9 = (the multF of G || the carrier of A) by GROUP_2:def 5;

      then

      reconsider A9 = multMagma (# the carrier of A, the multF of A #) as strict Subgroup of G by GROUP_2:def 5;

      

       A1: ( gr ( carr A)) is Subgroup of A9 by GROUP_4:def 4;

      A9 is Subgroup of A by GROUP_2: 57;

      hence thesis by A1, GROUP_2: 56;

    end;

    theorem :: GRNILP_1:11

    

     Th11: B is Subgroup of A implies [.A, B.] is Subgroup of A

    proof

      

       A1: ( gr ( carr A)) is Subgroup of A by Lm1;

      assume B is Subgroup of A;

      then ( commutators (A,B)) c= ( carr A) by Th10;

      then [.A, B.] is Subgroup of ( gr ( carr A)) by GROUP_4: 32;

      hence thesis by A1, GROUP_2: 56;

    end;

    theorem :: GRNILP_1:12

    B is Subgroup of A implies [.B, A.] is Subgroup of A by Th11;

    

     Lm2: A is Subgroup of ( (Omega). G)

    proof

      ( dom the multF of G) c= [:the carrier of G, the carrier of G:];

      then the multF of G = (the multF of ( (Omega). G) || the carrier of ( (Omega). G)) by RELAT_1: 68;

      then G is Subgroup of ( (Omega). G) by GROUP_2:def 5;

      hence thesis by GROUP_2: 56;

    end;

    theorem :: GRNILP_1:13

     [.H1, ( (Omega). G).] is Subgroup of H2 implies [.(H1 /\ H), H.] is Subgroup of (H2 /\ H)

    proof

      assume

       A1: [.H1, ( (Omega). G).] is Subgroup of H2;

      (H1 /\ H) is Subgroup of H by GROUP_2: 88;

      then

       A2: [.(H1 /\ H), H.] is Subgroup of H by Th11;

      

       A3: H is Subgroup of ( (Omega). G) by Lm2;

      (H1 /\ H) is Subgroup of H1 by GROUP_2: 88;

      then [.(H1 /\ H), H.] is Subgroup of [.H1, ( (Omega). G).] by A3, GROUP_5: 66;

      then [.(H1 /\ H), H.] is Subgroup of H2 by A1, GROUP_2: 56;

      hence thesis by A2, GROUP_2: 91;

    end;

    theorem :: GRNILP_1:14

     [.H1, H2.] is Subgroup of [.H1, ( (Omega). G).]

    proof

      

       A1: H2 is Subgroup of ( (Omega). G) by Lm2;

      H1 is Subgroup of H1 by GROUP_2: 54;

      hence thesis by A1, GROUP_5: 66;

    end;

    

     Lm3: for N be normal Subgroup of G holds [.N, H.] is Subgroup of N

    proof

      let N be normal Subgroup of G;

      the carrier of N c= the carrier of G & the multF of N = (the multF of G || the carrier of N) by GROUP_2:def 5;

      then

      reconsider N9 = multMagma (# the carrier of N, the multF of N #) as strict Subgroup of G by GROUP_2:def 5;

      now

        let a be Element of G;

        the carrier of (N |^ a) = (( carr N) |^ a) by GROUP_3:def 6

        .= (( carr N9) |^ a)

        .= the carrier of (N9 |^ a) by GROUP_3:def 6;

        

        hence (N9 |^ a) = (N |^ a) by GROUP_2: 59

        .= multMagma (# the carrier of N9, the multF of N9 #) by GROUP_3:def 13;

      end;

      then

      reconsider N9 as strict normal Subgroup of G by GROUP_3:def 13;

       [.N9, H.] = [.N, H.];

      then

       A1: [.N, H.] is Subgroup of N9 by GROUP_5: 67;

      N9 is Subgroup of N by GROUP_2: 57;

      hence thesis by A1, GROUP_2: 56;

    end;

    theorem :: GRNILP_1:15

    

     Th15: A is normal Subgroup of G iff [.A, ( (Omega). G).] is Subgroup of A

    proof

      thus A is normal Subgroup of G implies [.A, ( (Omega). G).] is Subgroup of A by Lm3;

      assume

       A1: [.A, ( (Omega). G).] is Subgroup of A;

      for b holds (b * A) c= (A * b)

      proof

        let b;

        let x be object;

        assume

         A2: x in (b * A);

        then

        reconsider x as Element of G;

        consider Z be Element of G such that

         A3: x = (b * Z) & Z in A by A2, GROUP_2: 103;

        

         A4: (Z " ) in A by A3, GROUP_2: 51;

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

        then [.(b " ), (Z " ).] in [.( (Omega). G), A.] by A4, GROUP_5: 65;

        then [.(b " ), (Z " ).] in A by A1, GROUP_2: 40;

        then

         A5: ((((b * Z) * (b " )) * (Z " )) * Z) in A by A3, GROUP_2: 50;

        

         A6: ((((b * Z) * (b " )) * (Z " )) * Z) = (((b * Z) * (b " )) * ((Z " ) * Z)) by GROUP_1:def 3

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

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

        (((b * Z) * (b " )) * b) = ((b * Z) * ((b " ) * b)) by GROUP_1:def 3

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

        .= (b * Z) by GROUP_1:def 4;

        hence thesis by A3, A5, A6, GROUP_2: 104;

      end;

      hence thesis by GROUP_3: 118;

    end;

    definition

      let G;

      :: GRNILP_1:def1

      func the_normal_subgroups_of G -> set means

      : Def1: for x be object holds x in it iff x is strict normal Subgroup of G;

      existence

      proof

        defpred P[ object, object] means ex H be strict normal Subgroup of G st $2 = H & $1 = the carrier of H;

        defpred P[ set] means ex H be strict normal Subgroup of G st $1 = the carrier of H;

        consider B be set such that

         A1: for x be set holds x in B iff x in ( bool the carrier of G) & P[x] from XFAMILY:sch 1;

        

         A2: for x,y1,y2 be object st P[x, y1] & P[x, y2] holds y1 = y2 by GROUP_2: 59;

        consider f be Function such that

         A3: for x,y be object holds [x, y] in f iff x in B & P[x, y] from FUNCT_1:sch 1( A2);

        for x be object holds x in B iff ex y be object st [x, y] in f

        proof

          let x be object;

          thus x in B implies ex y be object st [x, y] in f

          proof

            assume

             A4: x in B;

            then

            consider H be strict normal Subgroup of G such that

             A5: x = the carrier of H by A1;

            reconsider y = H as set by TARSKI: 1;

            take y;

            thus thesis by A3, A4, A5;

          end;

          given y be object such that

           A6: [x, y] in f;

          thus thesis by A3, A6;

        end;

        then

         A7: B = ( dom f) by XTUPLE_0:def 12;

        for y be object holds y in ( rng f) iff y is strict normal Subgroup of G

        proof

          let y be object;

          thus y in ( rng f) implies y is strict normal Subgroup of G

          proof

            assume y in ( rng f);

            then

            consider x be object such that

             A8: x in ( dom f) & y = (f . x) by FUNCT_1:def 3;

             [x, y] in f by A8, FUNCT_1:def 2;

            then ex H be strict normal Subgroup of G st y = H & x = the carrier of H by A3;

            hence thesis;

          end;

          assume y is strict normal Subgroup of G;

          then

          reconsider H = y as strict normal Subgroup of G;

          reconsider x = the carrier of H as set;

          

           A9: y is set by TARSKI: 1;

          the carrier of H c= the carrier of G by GROUP_2:def 5;

          then

           A10: x in ( dom f) by A1, A7;

          then [x, y] in f by A3, A7;

          then y = (f . x) by A10, FUNCT_1:def 2, A9;

          hence thesis by A10, FUNCT_1:def 3;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        defpred P[ object] means $1 is strict normal Subgroup of G;

        let A1,A2 be set;

        assume

         A11: for x be object holds x in A1 iff P[x];

        assume

         A12: for x be object holds x in A2 iff P[x];

        thus thesis from XBOOLE_0:sch 2( A11, A12);

      end;

    end

    registration

      let G;

      cluster ( the_normal_subgroups_of G) -> non empty;

      coherence

      proof

         the strict normal Subgroup of G in ( the_normal_subgroups_of G) by Def1;

        hence thesis;

      end;

    end

    theorem :: GRNILP_1:16

    

     Th16: for F be FinSequence of ( the_normal_subgroups_of G) holds for j st j in ( dom F) holds (F . j) is strict normal Subgroup of G

    proof

      let F be FinSequence of ( the_normal_subgroups_of G);

      let j;

      assume j in ( dom F);

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

      hence thesis by Def1;

    end;

    theorem :: GRNILP_1:17

    

     Th17: ( the_normal_subgroups_of G) c= ( Subgroups G)

    proof

      let x be object;

      assume x in ( the_normal_subgroups_of G);

      then x is strict normal Subgroup of G by Def1;

      hence thesis by GROUP_3:def 1;

    end;

    theorem :: GRNILP_1:18

    

     Th18: for F be FinSequence of ( the_normal_subgroups_of G) holds F is FinSequence of ( Subgroups G)

    proof

      let F be FinSequence of ( the_normal_subgroups_of G);

      ( the_normal_subgroups_of G) c= ( Subgroups G) by Th17;

      then ( rng F) c= ( Subgroups G);

      hence thesis by FINSEQ_1:def 4;

    end;

    definition

      let IT be Group;

      :: GRNILP_1:def2

      attr IT is nilpotent means

      : Def2: ex F be FinSequence of ( the_normal_subgroups_of IT) st ( len F) > 0 & (F . 1) = ( (Omega). IT) & (F . ( len F)) = ( (1). IT) & for i st i in ( dom F) & (i + 1) in ( dom F) holds for G1,G2 be strict normal Subgroup of IT st G1 = (F . i) & G2 = (F . (i + 1)) holds G2 is Subgroup of G1 & (G1 ./. ((G1,G2) `*` )) is Subgroup of ( center (IT ./. G2));

    end

    registration

      cluster nilpotent strict for Group;

      existence

      proof

        set G = the Group;

        take H = ( (1). G);

        thus H is nilpotent

        proof

          ( rng <*H*>) c= ( the_normal_subgroups_of H)

          proof

            let x be object;

            assume

             A1: x in ( rng <*H*>);

            ( rng <*H*>) = {H} by FINSEQ_1: 39;

            then x = H by A1, TARSKI:def 1;

            then x is strict normal Subgroup of H by GROUP_2: 54, GROUP_6: 8;

            hence thesis by Def1;

          end;

          then

          reconsider F = <*H*> as FinSequence of ( the_normal_subgroups_of H) by FINSEQ_1:def 4;

          take F;

          

           A2: ( len F) = 1 by FINSEQ_1: 39;

          

          then

           A3: (F . ( len F)) = H by FINSEQ_1: 40

          .= ( (1). H) by GROUP_2: 63;

          for i st i in ( dom F) & (i + 1) in ( dom F) holds for G1,G2 be strict normal Subgroup of H st G1 = (F . i) & G2 = (F . (i + 1)) holds G2 is strict Subgroup of G1 & (G1 ./. ((G1,G2) `*` )) is Subgroup of ( center (H ./. G2))

          proof

            let i;

            assume

             A4: i in ( dom F) & (i + 1) in ( dom F);

            let G1,G2 be strict normal Subgroup of H;

            assume G1 = (F . i) & G2 = (F . (i + 1));

            ( dom F) = {1} by A2, FINSEQ_1: 2, FINSEQ_1:def 3;

            then i = 1 & (i + 1) = 1 by A4, TARSKI:def 1;

            hence thesis;

          end;

          hence thesis by A3, FINSEQ_1: 40;

        end;

        thus thesis;

      end;

    end

    theorem :: GRNILP_1:19

    

     Th19: for G1 be Subgroup of G, N be strict normal Subgroup of G st N is Subgroup of G1 & (G1 ./. ((G1,N) `*` )) is Subgroup of ( center (G ./. N)) holds [.G1, ( (Omega). G).] is Subgroup of N

    proof

      let G1 be Subgroup of G;

      let N be strict normal Subgroup of G;

      assume that

       A1: N is Subgroup of G1 and

       A2: (G1 ./. ((G1,N) `*` )) is Subgroup of ( center (G ./. N));

      

       A3: ((G1,N) `*` ) = N by A1, GROUP_6:def 1;

      reconsider J = (G1 ./. ((G1,N) `*` )) as Subgroup of (G ./. N) by A1, GROUP_6: 28;

      reconsider I = N as normal Subgroup of G1 by A3;

      

       A4: ( commutators (G1,( (Omega). G))) c= ( carr N)

      proof

        now

          let x be Element of G;

          assume x in ( commutators (G1,( (Omega). G)));

          then

          consider a, b such that

           A5: x = [.a, b.] & a in G1 & b in ( (Omega). G) by GROUP_5: 52;

          reconsider c = a as Element of G1 by A5, STRUCT_0:def 5;

          reconsider S9 = (c * I) as Element of J by A3, GROUP_6: 22;

          

           A6: S9 in J by STRUCT_0:def 5;

          reconsider T = (b * N) as Element of (G ./. N) by GROUP_6: 14;

          reconsider d = c as Element of G;

          (d * N) = (c * I) by GROUP_6: 2;

          then

          reconsider S = S9 as Element of (G ./. N) by GROUP_6: 14;

          S in ( center (G ./. N)) by A2, A6, GROUP_2: 40;

          then

           A7: (S * T) = (T * S) by GROUP_5: 77;

          

           A8: S = (d * N) & T = (b * N) & ( @ S) = S & ( @ T) = T by GROUP_6: 2;

          

          then

           A9: (S * T) = ((d * N) * (b * N)) by GROUP_6:def 3

          .= (d * (N * (b * N))) by GROUP_3: 10

          .= (d * ((N * b) * N)) by GROUP_3: 13

          .= (d * ((b * N) * N)) by GROUP_3: 117

          .= (d * (b * N)) by GROUP_6: 5

          .= ((d * b) * N) by GROUP_2: 105;

          (T * S) = ((b * N) * (d * N)) by A8, GROUP_6:def 3

          .= (b * (N * (d * N))) by GROUP_3: 10

          .= (b * ((N * d) * N)) by GROUP_3: 13

          .= (b * ((d * N) * N)) by GROUP_3: 117

          .= (b * (d * N)) by GROUP_6: 5

          .= ((b * d) * N) by GROUP_2: 105;

          

          then

           A10: (((d " ) * (b " )) * ((d * b) * N)) = ((((d " ) * (b " )) * (b * d)) * N) by A7, A9, GROUP_2: 105

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

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

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

          .= (((d " ) * d) * N) by GROUP_1:def 4

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

          .= ( carr N) by GROUP_2: 109;

          (((d " ) * (b " )) * ((d * b) * N)) = ((((d " ) * (b " )) * (d * b)) * N) by GROUP_2: 105

          .= ( [.d, b.] * N) by GROUP_5: 16;

          then [.d, b.] in N by A10, GROUP_2: 113;

          hence x in ( carr N) by A5, STRUCT_0:def 5;

        end;

        hence thesis;

      end;

      ( gr ( carr N)) = N by GROUP_4: 31;

      hence thesis by A4, GROUP_4: 32;

    end;

    theorem :: GRNILP_1:20

    

     Th20: for G1 be Subgroup of G, N be normal Subgroup of G st N is strict Subgroup of G1 & [.G1, ( (Omega). G).] is strict Subgroup of N holds (G1 ./. ((G1,N) `*` )) is Subgroup of ( center (G ./. N))

    proof

      let G1 be Subgroup of G;

      let N be normal Subgroup of G;

      assume that

       A1: N is strict Subgroup of G1 and

       A2: [.G1, ( (Omega). G).] is strict Subgroup of N;

      

       A3: ((G1,N) `*` ) = N by A1, GROUP_6:def 1;

      reconsider J = (G1 ./. ((G1,N) `*` )) as Subgroup of (G ./. N) by A1, GROUP_6: 28;

      reconsider I = N as normal Subgroup of G1 by A3;

      for S1 be Element of (G ./. N) st S1 in J holds S1 in ( center (G ./. N))

      proof

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

        assume

         A4: S1 in J;

        for S be Element of (G ./. N) holds (S1 * S) = (S * S1)

        proof

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

          consider a be Element of G such that

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

          consider c be Element of G1 such that

           A6: S1 = (c * I) & S1 = (I * c) by A3, A4, GROUP_6: 23;

          reconsider d = c as Element of G by GROUP_2: 42;

          

           A7: d in G1 by STRUCT_0:def 5;

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

          then [.d, a.] in [.G1, ( (Omega). G).] by A7, GROUP_5: 65;

          then

           A8: [.d, a.] in N by A2, GROUP_2: 40;

          

           A9: ( @ S) = S & ( @ S1) = S1 & (c * I) = (d * N) & (N * d) = (I * c) by GROUP_6: 2;

          

          then

           A10: (S * S1) = ((a * N) * (d * N)) by A5, A6, GROUP_6:def 3

          .= ((a * d) * N) by GROUP_11: 1;

          

           A11: (S1 * S) = ((d * N) * (a * N)) by A5, A6, A9, GROUP_6:def 3

          .= ((d * a) * N) by GROUP_11: 1;

          

           A12: (((a * d) * [.d, a.]) * N) = ((a * d) * ( [.d, a.] * N)) by GROUP_2: 32

          .= ((a * d) * N) by A8, GROUP_2: 113;

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

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

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

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

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

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

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

          .= ((d * a) * N) by GROUP_1:def 4;

          hence thesis by A10, A11, A12;

        end;

        hence thesis by GROUP_5: 77;

      end;

      hence thesis by GROUP_2: 58;

    end;

    theorem :: GRNILP_1:21

    

     Th21: for G be Group holds G is nilpotent iff ex F be FinSequence of ( the_normal_subgroups_of G) st ( len F) > 0 & (F . 1) = ( (Omega). G) & (F . ( len F)) = ( (1). G) & for i st i in ( dom F) & (i + 1) in ( dom F) holds for G1,G2 be strict normal Subgroup of G st G1 = (F . i) & G2 = (F . (i + 1)) holds G2 is Subgroup of G1 & [.G1, ( (Omega). G).] is Subgroup of G2

    proof

      let G be Group;

       A1:

      now

        assume G is nilpotent;

        then

        consider R be FinSequence of ( the_normal_subgroups_of G) such that

         A2: ( len R) > 0 & (R . 1) = ( (Omega). G) & (R . ( len R)) = ( (1). G) & for i st i in ( dom R) & (i + 1) in ( dom R) holds for H1,H2 be strict normal Subgroup of G st H1 = (R . i) & H2 = (R . (i + 1)) holds H2 is Subgroup of H1 & (H1 ./. ((H1,H2) `*` )) is Subgroup of ( center (G ./. H2));

        reconsider F = R as FinSequence of ( the_normal_subgroups_of G);

        

         A3: for i st i in ( dom F) & (i + 1) in ( dom F) holds for G1,G2 be strict normal Subgroup of G st G1 = (F . i) & G2 = (F . (i + 1)) holds G2 is strict Subgroup of G1 & [.G1, ( (Omega). G).] is strict Subgroup of G2

        proof

          let i;

          assume

           A4: i in ( dom F) & (i + 1) in ( dom F);

          let G1,G2 be strict normal Subgroup of G;

          assume

           A5: G1 = (F . i) & G2 = (F . (i + 1));

          then

           A6: G2 is strict Subgroup of G1 & for N be strict normal Subgroup of G st N = G2 & N is strict Subgroup of G1 holds (G1 ./. ((G1,N) `*` )) is Subgroup of ( center (G ./. N)) by A2, A4;

           [.G1, ( (Omega). G).] is strict Subgroup of G2

          proof

            now

              let N be strict normal Subgroup of G;

              assume

               A7: N = G2 & N is strict Subgroup of G1;

              then (G1 ./. ((G1,N) `*` )) is Subgroup of ( center (G ./. N)) by A2, A4, A5;

              hence [.G1, ( (Omega). G).] is strict Subgroup of G2 by A7, Th19;

            end;

            hence thesis by A6;

          end;

          hence thesis by A2, A4, A5;

        end;

        take F;

        thus ( len F) > 0 & (F . 1) = ( (Omega). G) & (F . ( len F)) = ( (1). G) & for i st i in ( dom F) & (i + 1) in ( dom F) holds for G1,G2 be strict normal Subgroup of G st G1 = (F . i) & G2 = (F . (i + 1)) holds G2 is Subgroup of G1 & [.G1, ( (Omega). G).] is Subgroup of G2 by A2, A3;

      end;

      now

        given F be FinSequence of ( the_normal_subgroups_of G) such that

         A8: ( len F) > 0 & (F . 1) = ( (Omega). G) & (F . ( len F)) = ( (1). G) & for i st i in ( dom F) & (i + 1) in ( dom F) holds for G1,G2 be strict normal Subgroup of G st G1 = (F . i) & G2 = (F . (i + 1)) holds G2 is Subgroup of G1 & [.G1, ( (Omega). G).] is Subgroup of G2;

        

         A9: for i st i in ( dom F) & (i + 1) in ( dom F) holds for G1,G2 be strict normal Subgroup of G st G1 = (F . i) & G2 = (F . (i + 1)) holds G2 is strict Subgroup of G1 & (G1 ./. ((G1,G2) `*` )) is Subgroup of ( center (G ./. G2))

        proof

          let i;

          assume

           A10: i in ( dom F) & (i + 1) in ( dom F);

          let G1,G2 be strict normal Subgroup of G;

          assume

           A11: G1 = (F . i) & G2 = (F . (i + 1));

          then

           A12: G2 is strict Subgroup of G1 by A8, A10;

           [.G1, ( (Omega). G).] is strict Subgroup of G2 by A8, A10, A11;

          hence thesis by A12, Th20;

        end;

        take F;

        ( len F) > 0 & (F . 1) = ( (Omega). G) & (F . ( len F)) = ( (1). G) & for i st i in ( dom F) & (i + 1) in ( dom F) holds for G1,G2 be strict normal Subgroup of G st G1 = (F . i) & G2 = (F . (i + 1)) holds G2 is Subgroup of G1 & (G1 ./. ((G1,G2) `*` )) is Subgroup of ( center (G ./. G2)) by A8, A9;

        hence G is nilpotent;

      end;

      hence thesis by A1;

    end;

    theorem :: GRNILP_1:22

    

     Th22: for G be Group holds for H,G1 be Subgroup of G holds for G2 be strict normal Subgroup of G holds for H1 be Subgroup of H holds for H2 be normal Subgroup of H st G2 is Subgroup of G1 & (G1 ./. ((G1,G2) `*` )) is Subgroup of ( center (G ./. G2)) & H1 = (G1 /\ H) & H2 = (G2 /\ H) holds (H1 ./. ((H1,H2) `*` )) is Subgroup of ( center (H ./. H2))

    proof

      let G be Group;

      let H,G1 be Subgroup of G;

      let G2 be strict normal Subgroup of G;

      let H1 be Subgroup of H;

      let H2 be normal Subgroup of H;

      assume that

       A1: G2 is Subgroup of G1 and

       A2: (G1 ./. ((G1,G2) `*` )) is Subgroup of ( center (G ./. G2)) and

       A3: H1 = (G1 /\ H) & H2 = (G2 /\ H);

      

       A4: [.G1, ( (Omega). G).] is Subgroup of G2 by A1, A2, Th19;

      

       A5: H2 is strict Subgroup of H1 by A1, A3, GROUP_2: 92;

      then

       A6: ((H1,H2) `*` ) = H2 by GROUP_6:def 1;

      then

      reconsider I = H2 as normal Subgroup of H1;

      reconsider J = (H1 ./. ((H1,H2) `*` )) as Subgroup of (H ./. H2) by A5, GROUP_6: 28;

      for T be Element of (H ./. H2) st T in J holds T in ( center (H ./. H2))

      proof

        let T be Element of (H ./. H2);

        assume

         A7: T in J;

        for S be Element of (H ./. H2) holds (S * T) = (T * S)

        proof

          let S be Element of (H ./. H2);

          consider h be Element of H such that

           A8: S = (h * H2) & S = (H2 * h) by GROUP_6: 21;

          consider h1 be Element of H1 such that

           A9: T = (h1 * I) & T = (I * h1) by A6, A7, GROUP_6: 23;

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

          

           A10: ( @ S) = S & ( @ T) = T & (h1 * I) = (h2 * H2) by GROUP_6: 2;

          

          then

           A11: (S * T) = ((h * H2) * (h2 * H2)) by A8, A9, GROUP_6:def 3

          .= ((h * h2) * H2) by GROUP_11: 1;

          

           A12: (T * S) = ((h2 * H2) * (h * H2)) by A8, A9, A10, GROUP_6:def 3

          .= ((h2 * h) * H2) by GROUP_11: 1;

          

           A13: [.h2, h.] in H by STRUCT_0:def 5;

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

          

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

          H1 is Subgroup of G1 by A3, GROUP_2: 88;

          then

          reconsider b = h1 as Element of G1 by GROUP_2: 42;

          reconsider c = b as Element of G by GROUP_2: 42;

          b in G1 by STRUCT_0:def 5;

          then [.c, a.] in [.G1, ( (Omega). G).] by A14, GROUP_5: 65;

          then

           A15: [.c, a.] in G2 by A4, GROUP_2: 40;

          

           A16: (a " ) = (h " ) by GROUP_2: 48;

          (c " ) = (h2 " ) by GROUP_2: 48;

          then

           A17: ((h2 " ) * (h " )) = ((c " ) * (a " )) by A16, GROUP_2: 43;

          (h2 * h) = (c * a) by GROUP_2: 43;

          then

           A18: (((h2 " ) * (h " )) * (h2 * h)) = (((c " ) * (a " )) * (c * a)) by A17, GROUP_2: 43;

          

           A19: [.h2, h.] = (((h2 " ) * (h " )) * (h2 * h)) by GROUP_5: 16;

           [.c, a.] = (((c " ) * (a " )) * (c * a)) by GROUP_5: 16;

          then [.h2, h.] in H2 by A3, A13, A15, A18, A19, GROUP_2: 82;

          

          then ((h * h2) * H2) = ((h * h2) * ( [.h2, h.] * H2)) by GROUP_2: 113

          .= ((h * h2) * ((((h2 " ) * (h " )) * (h2 * h)) * H2)) by GROUP_5: 16

          .= (((h * h2) * (((h2 " ) * (h " )) * (h2 * h))) * H2) by GROUP_2: 32

          .= ((((h * h2) * ((h2 " ) * (h " ))) * (h2 * h)) * H2) by GROUP_1:def 3

          .= (((h * (h2 * ((h2 " ) * (h " )))) * (h2 * h)) * H2) by GROUP_1:def 3

          .= (((h * ((h2 * (h2 " )) * (h " ))) * (h2 * h)) * H2) by GROUP_1:def 3

          .= (((h * (( 1_ H) * (h " ))) * (h2 * h)) * H2) by GROUP_1:def 5

          .= (((h * (h " )) * (h2 * h)) * H2) by GROUP_1:def 4

          .= ((( 1_ H) * (h2 * h)) * H2) by GROUP_1:def 5

          .= ((h2 * h) * H2) by GROUP_1:def 4;

          hence thesis by A11, A12;

        end;

        hence thesis by GROUP_5: 77;

      end;

      hence thesis by GROUP_2: 58;

    end;

    

     Lm4: (( (Omega). G) /\ H) = ( (Omega). H)

    proof

      reconsider G9 = ( (Omega). G) as strict Group;

      the carrier of H c= the carrier of G & the multF of H = (the multF of G || the carrier of H) by GROUP_2:def 5;

      then

      reconsider H9 = ( (Omega). H) as strict Subgroup of G9 by GROUP_2:def 5;

      the carrier of H c= the carrier of G & the multF of H = (the multF of G || the carrier of H) by GROUP_2:def 5;

      then

       A1: H is Subgroup of ( (Omega). G) by GROUP_2:def 5;

       the multMagma of (( (Omega). G) qua Subgroup of G /\ H) = the multMagma of (H /\ ( (Omega). G) qua Subgroup of G)

      .= multMagma (# the carrier of (H /\ ( (Omega). G)), the multF of (H /\ ( (Omega). G)) #)

      .= multMagma (# the carrier of H, the multF of H #) by A1, GROUP_2: 89

      .= multMagma (# the carrier of (H9 /\ ( (Omega). G9)), the multF of (H9 /\ ( (Omega). G9)) #) by GROUP_2: 89

      .= the multMagma of (H9 /\ ( (Omega). G9) qua Subgroup of G9)

      .= the multMagma of (( (Omega). G9) qua Subgroup of G9 /\ H9);

      hence thesis by GROUP_2: 86;

    end;

    

     Lm5: for F1 be strict Subgroup of G holds for H,F2 be Subgroup of G st F1 is normal Subgroup of F2 holds (F1 /\ H) is normal Subgroup of (F2 /\ H)

    proof

      let F1 be strict Subgroup of G;

      let H,F2 be Subgroup of G;

      reconsider F = (F2 /\ H) as Subgroup of F2 by GROUP_2: 88;

      assume

       A1: F1 is normal Subgroup of F2;

      

      then

       A2: (F1 /\ H) = ((F1 /\ F2) /\ H) by GROUP_2: 89

      .= (F1 /\ (F2 /\ H)) by GROUP_2: 84;

      reconsider F1 as normal Subgroup of F2 by A1;

      (F1 /\ F) is normal Subgroup of F;

      hence thesis by A2, GROUP_6: 3;

    end;

    registration

      let G be nilpotent Group;

      cluster -> nilpotent for Subgroup of G;

      coherence

      proof

        let H be Subgroup of G;

        consider F be FinSequence of ( the_normal_subgroups_of G) such that

         A1: ( len F) > 0 & (F . 1) = ( (Omega). G) & (F . ( len F)) = ( (1). G) and

         A2: for i st i in ( dom F) & (i + 1) in ( dom F) holds for G1,G2 be strict normal Subgroup of G st G1 = (F . i) & G2 = (F . (i + 1)) holds G2 is Subgroup of G1 & (G1 ./. ((G1,G2) `*` )) is Subgroup of ( center (G ./. G2)) by Def2;

        defpred P[ set, set] means ex I be strict normal Subgroup of G st I = (F . $1) & $2 = (I /\ H);

        

         A3: for k be Nat st k in ( Seg ( len F)) holds ex x be Element of ( the_normal_subgroups_of H) st P[k, x]

        proof

          let k be Nat;

          assume k in ( Seg ( len F));

          then k in ( dom F) by FINSEQ_1:def 3;

          then (F . k) in ( the_normal_subgroups_of G) by FINSEQ_2: 11;

          then

          reconsider I = (F . k) as strict normal Subgroup of G by Def1;

          reconsider x = (I /\ H) as strict Subgroup of H;

          reconsider y = x as Element of ( the_normal_subgroups_of H) by Def1;

          take y;

          take I;

          thus thesis;

        end;

        consider R be FinSequence of ( the_normal_subgroups_of H) such that

         A4: ( dom R) = ( Seg ( len F)) & for i be Nat st i in ( Seg ( len F)) holds P[i, (R . i)] from FINSEQ_1:sch 5( A3);

        

         A5: ( len R) = ( len F) by A4, FINSEQ_1:def 3;

        

         A6: ( len R) > 0 by A1, A4, FINSEQ_1:def 3;

        

         A7: (R . 1) = ( (Omega). H)

        proof

          1 <= ( len R) by A6, NAT_1: 14;

          then 1 in ( Seg ( len F)) by A5;

          then ex I be strict normal Subgroup of G st I = (F . 1) & (R . 1) = (I /\ H) by A4;

          hence (R . 1) = ( (Omega). H) by A1, Lm4;

        end;

        

         A8: (R . ( len R)) = ( (1). H)

        proof

          ex I be strict normal Subgroup of G st I = (F . ( len R)) & (R . ( len R)) = (I /\ H) by A1, A4, A5, FINSEQ_1: 3;

          

          hence (R . ( len R)) = ( (1). G) by A1, A5, GROUP_2: 85

          .= ( (1). H) by GROUP_2: 63;

        end;

        

         A9: for i st i in ( dom R) & (i + 1) in ( dom R) holds for H1,H2 be strict normal Subgroup of H st H1 = (R . i) & H2 = (R . (i + 1)) holds H2 is Subgroup of H1 & (H1 ./. ((H1,H2) `*` )) is Subgroup of ( center (H ./. H2))

        proof

          let i;

          assume

           A10: i in ( dom R) & (i + 1) in ( dom R);

          let H1,H2 be strict normal Subgroup of H;

          assume

           A11: H1 = (R . i) & H2 = (R . (i + 1));

          consider I be strict normal Subgroup of G such that

           A12: I = (F . i) & (R . i) = (I /\ H) by A4, A10;

          consider J be strict normal Subgroup of G such that

           A13: J = (F . (i + 1)) & (R . (i + 1)) = (J /\ H) by A4, A10;

          

           A14: i in ( dom F) & (i + 1) in ( dom F) by A4, A10, FINSEQ_1:def 3;

          then

           A15: J is strict normal Subgroup of I by A12, A13, A2, GROUP_6: 8;

          (I ./. ((I,J) `*` )) is Subgroup of ( center (G ./. J)) by A14, A12, A13, A2;

          hence thesis by A13, A15, A12, A11, Th22, Lm5;

        end;

        take R;

        thus thesis by A1, A4, A7, A8, A9, FINSEQ_1:def 3;

      end;

    end

    registration

      cluster commutative -> nilpotent for Group;

      correctness

      proof

        let G be Group;

        assume

         A1: G is commutative;

        ( (Omega). G) in ( the_normal_subgroups_of G) & ( (1). G) in ( the_normal_subgroups_of G) by Def1;

        then <*( (Omega). G), ( (1). G)*> is FinSequence of ( the_normal_subgroups_of G) by FINSEQ_2: 13;

        then

        consider F be FinSequence of ( the_normal_subgroups_of G) such that

         A2: F = <*( (Omega). G), ( (1). G)*>;

        

         A3: ( len F) = 2 & (F . 1) = ( (Omega). G) & (F . 2) = ( (1). G) by A2, FINSEQ_1: 44;

        for i st i in ( dom F) & (i + 1) in ( dom F) holds for G1,G2 be strict normal Subgroup of G st G1 = (F . i) & G2 = (F . (i + 1)) holds G2 is Subgroup of G1 & [.G1, ( (Omega). G).] is Subgroup of G2

        proof

          let i;

          assume

           A4: i in ( dom F) & (i + 1) in ( dom F);

          now

            let G1,G2 be Subgroup of G;

            assume

             A5: G1 = (F . i) & G2 = (F . (i + 1));

            

             A6: ( dom F) = {1, 2} by A3, FINSEQ_1: 2, FINSEQ_1:def 3;

            

             A7: i in {1, 2} & (i + 1) in {1, 2} by A3, A4, FINSEQ_1: 2, FINSEQ_1:def 3;

            

             A8: i = 1 or i = 2 by A4, A6, TARSKI:def 2;

            ( commutators (G1,( (Omega). G))) = {( 1_ G)} by A1, GROUP_5: 57;

            

            then

             A9: [.G1, ( (Omega). G).] = ( gr ( {( 1_ G)} \ {( 1_ G)})) by GROUP_4: 35

            .= ( gr ( {} the carrier of G)) by XBOOLE_1: 37

            .= ( (1). G) by GROUP_4: 30;

            G1 = ( (Omega). G) & G2 = ( (1). G) by A2, A5, A7, A8, FINSEQ_1: 44, TARSKI:def 2;

            hence thesis by A5, A9, GROUP_2: 65;

          end;

          hence thesis;

        end;

        hence thesis by A3, Th21;

      end;

      cluster cyclic -> nilpotent for Group;

      coherence ;

    end

    theorem :: GRNILP_1:23

    

     Th23: for G,H be strict Group, h be Homomorphism of G, H holds for A be strict Subgroup of G holds for a,b be Element of G holds (((h . a) * (h . b)) * (h .: A)) = (h .: ((a * b) * A)) & (((h .: A) * (h . a)) * (h . b)) = (h .: ((A * a) * b))

    proof

      let G,H be strict Group;

      let h be Homomorphism of G, H;

      let A be strict Subgroup of G;

      let a,b be Element of G;

      

      thus (((h . a) * (h . b)) * (h .: A)) = ((h . (a * b)) * (h .: A)) by GROUP_6:def 6

      .= (h .: ((a * b) * A)) by GRSOLV_1: 13;

      

      thus (((h .: A) * (h . a)) * (h . b)) = ((h .: A) * ((h . a) * (h . b))) by GROUP_2: 107

      .= ((h .: A) * (h . (a * b))) by GROUP_6:def 6

      .= (h .: (A * (a * b))) by GRSOLV_1: 13

      .= (h .: ((A * a) * b)) by GROUP_2: 107;

    end;

    theorem :: GRNILP_1:24

    

     Th24: for G,H be strict Group, h be Homomorphism of G, H holds for A be strict Subgroup of G holds for a,b be Element of G holds for H1 be Subgroup of ( Image h) holds for a1,b1 be Element of ( Image h) st a1 = (h . a) & b1 = (h . b) & H1 = (h .: A) holds ((a1 * b1) * H1) = (((h . a) * (h . b)) * (h .: A))

    proof

      let G,H be strict Group;

      let h be Homomorphism of G, H;

      let A be strict Subgroup of G;

      let a,b be Element of G;

      let H1 be Subgroup of ( Image h);

      let a1,b1 be Element of ( Image h);

      assume that

       A1: a1 = (h . a) and

       A2: b1 = (h . b) and

       A3: H1 = (h .: A);

      

       A4: (a1 * b1) = ((h . a) * (h . b)) by A1, A2, GROUP_2: 43;

      set c1 = (a1 * b1);

      set c = (a * b);

      

       A5: (h . c) = ((h . a) * (h . b)) by GROUP_6:def 6;

      

       A6: (h .: (c * A)) = ((h . c) * (h .: A)) by GRSOLV_1: 13;

      (c1 * H1) = ((h . c) * (h .: A))

      proof

        now

          let x be object;

          assume x in (c1 * H1);

          then

          consider Z be Element of ( Image h) such that

           A7: x = (c1 * Z) and

           A8: Z in H1 by GROUP_2: 103;

          consider Z1 be Element of A such that

           A9: Z = ((h | A) . Z1) by A3, A8, GROUP_6: 45;

          

           A10: Z1 in A by STRUCT_0:def 5;

          reconsider Z1 as Element of G by GROUP_2: 42;

          Z = (h . Z1) by A9, FUNCT_1: 49;

          

          then

           A11: x = ((h . c) * (h . Z1)) by A4, A5, A7, GROUP_2: 43

          .= (h . (c * Z1)) by GROUP_6:def 6;

          (c * Z1) in (c * A) by A10, GROUP_2: 103;

          hence x in ((h . c) * (h .: A)) by A11, A6, FUNCT_2: 35;

        end;

        then

         A12: (c1 * H1) c= ((h . c) * (h .: A));

        now

          let x be object;

          assume x in ((h . c) * (h .: A));

          then

          consider y be object such that

           A13: y in the carrier of G and

           A14: y in (c * A) and

           A15: x = (h . y) by A6, FUNCT_2: 64;

          reconsider y as Element of G by A13;

          consider Z be Element of G such that

           A16: y = (c * Z) and

           A17: Z in A by A14, GROUP_2: 103;

          Z in the carrier of A by A17, STRUCT_0:def 5;

          then (h . Z) in (h .: the carrier of A) by FUNCT_2: 35;

          then (h . Z) in the carrier of (h .: A) by GRSOLV_1: 8;

          then

           A18: (h . Z) in H1 by A3, STRUCT_0:def 5;

          then (h . Z) in ( Image h) by GROUP_2: 40;

          then

          reconsider Z1 = (h . Z) as Element of ( Image h) by STRUCT_0:def 5;

          x = ((h . c) * (h . Z)) by A15, A16, GROUP_6:def 6;

          then x = (c1 * Z1) by A4, A5, GROUP_2: 43;

          hence x in (c1 * H1) by A18, GROUP_2: 103;

        end;

        then ((h . c) * (h .: A)) c= (c1 * H1);

        hence thesis by A12, XBOOLE_0:def 10;

      end;

      hence thesis by GROUP_6:def 6;

    end;

    theorem :: GRNILP_1:25

    

     Th25: for G,H be strict Group, h be Homomorphism of G, H holds for G1 be strict Subgroup of G holds for G2 be strict normal Subgroup of G holds for H1 be strict Subgroup of ( Image h) holds for H2 be strict normal Subgroup of ( Image h) st G2 is strict Subgroup of G1 & (G1 ./. ((G1,G2) `*` )) is Subgroup of ( center (G ./. G2)) & H1 = (h .: G1) & H2 = (h .: G2) holds (H1 ./. ((H1,H2) `*` )) is Subgroup of ( center (( Image h) ./. H2))

    proof

      let G,H be strict Group;

      let h be Homomorphism of G, H;

      let G1 be strict Subgroup of G;

      let G2 be strict normal Subgroup of G;

      let H1 be strict Subgroup of ( Image h);

      let H2 be strict normal Subgroup of ( Image h);

      assume that

       A1: G2 is strict Subgroup of G1 and

       A2: (G1 ./. ((G1,G2) `*` )) is Subgroup of ( center (G ./. G2)) and

       A3: H1 = (h .: G1) & H2 = (h .: G2);

      

       A4: H2 is strict Subgroup of H1 by A1, A3, GRSOLV_1: 12;

      then

       A5: ((H1,H2) `*` ) = H2 by GROUP_6:def 1;

      then

      reconsider I = H2 as normal Subgroup of H1;

      reconsider J = (H1 ./. ((H1,H2) `*` )) as Subgroup of (( Image h) ./. H2) by A4, GROUP_6: 28;

      for T be Element of (( Image h) ./. H2) st T in J holds T in ( center (( Image h) ./. H2))

      proof

        let T be Element of (( Image h) ./. H2);

        assume

         A6: T in J;

        for S be Element of (( Image h) ./. H2) holds (S * T) = (T * S)

        proof

          let S be Element of (( Image h) ./. H2);

          consider g be Element of ( Image h) such that

           A7: S = (g * H2) & S = (H2 * g) by GROUP_6: 21;

          consider h1 be Element of H1 such that

           A8: T = (h1 * I) & T = (I * h1) by A5, A6, GROUP_6: 23;

          reconsider h2 = h1 as Element of ( Image h) by GROUP_2: 42;

          

           A9: ( @ S) = S & ( @ T) = T & (h1 * I) = (h2 * H2) by GROUP_6: 2;

          

          then

           A10: (S * T) = ((g * H2) * (h2 * H2)) by A7, A8, GROUP_6:def 3

          .= ((g * h2) * H2) by GROUP_11: 1;

          

           A11: (T * S) = ((h2 * H2) * (g * H2)) by A7, A8, A9, GROUP_6:def 3

          .= ((h2 * g) * H2) by GROUP_11: 1;

          g in ( Image h) by STRUCT_0:def 5;

          then

          consider a be Element of G such that

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

          

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

          h1 in H1 by STRUCT_0:def 5;

          then

          consider a1 be Element of G1 such that

           A14: h1 = ((h | G1) . a1) by A3, GROUP_6: 45;

          

           A15: a1 in G1 by STRUCT_0:def 5;

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

          

           A16: h2 = (h . a2) by A14, FUNCT_1: 49;

          

          then

           A17: ((g * h2) * H2) = (((h . a) * (h . a2)) * (h .: G2)) by A12, A3, Th24

          .= (h .: ((a * a2) * G2)) by Th23;

          

           A18: ((h2 * g) * H2) = (((h . a2) * (h . a)) * (h .: G2)) by A12, A16, A3, Th24

          .= (h .: ((a2 * a) * G2)) by Th23;

          

           A19: [.G1, ( (Omega). G).] is strict Subgroup of G2 by A1, A2, Th19;

           [.a2, a.] in [.G1, ( (Omega). G).] by A13, A15, GROUP_5: 65;

          then [.a2, a.] in G2 by A19, GROUP_2: 40;

          

          then ((a * a2) * G2) = ((a * a2) * ( [.a2, a.] * G2)) by GROUP_2: 113

          .= ((a * a2) * ((((a2 " ) * (a " )) * (a2 * a)) * G2)) by GROUP_5: 16

          .= (((a * a2) * (((a2 " ) * (a " )) * (a2 * a))) * G2) by GROUP_2: 32

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

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

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

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

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

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

          .= ((a2 * a) * G2) by GROUP_1:def 4;

          hence thesis by A10, A11, A17, A18;

        end;

        hence thesis by GROUP_5: 77;

      end;

      hence thesis by GROUP_2: 58;

    end;

    theorem :: GRNILP_1:26

    

     Th26: for G,H be strict Group, h be Homomorphism of G, H holds for A be strict normal Subgroup of G holds (h .: A) is strict normal Subgroup of ( Image h)

    proof

      let G,H be strict Group;

      let h be Homomorphism of G, H;

      let A be strict normal Subgroup of G;

      reconsider C = (h .: A) as strict Subgroup of ( Image h) by GRSOLV_1: 9;

      for b be Element of ( Image h) holds (b * C) c= (C * b)

      proof

        let b be Element of ( Image h);

        

         A1: b in ( Image h) by STRUCT_0:def 5;

        now

          consider b1 be Element of G such that

           A2: b = (h . b1) by A1, GROUP_6: 45;

          let x be object;

          assume x in (b * C);

          then

          consider g be Element of ( Image h) such that

           A3: x = (b * g) and

           A4: g in C by GROUP_2: 103;

          consider g1 be Element of A such that

           A5: g = ((h | A) . g1) by A4, GROUP_6: 45;

          reconsider g1 as Element of G by GROUP_2: 42;

          g = (h . g1) by A5, FUNCT_1: 49;

          

          then

           A6: x = ((h . b1) * (h . g1)) by A2, A3, GROUP_2: 43

          .= (h . (b1 * g1)) by GROUP_6:def 6;

          g1 in A by STRUCT_0:def 5;

          then

           A7: (b1 * g1) in (b1 * A) by GROUP_2: 103;

          

           A8: (h .: (A * b1)) = ((h .: A) * (h . b1)) by GRSOLV_1: 13;

          (b1 * A) = (A * b1) by GROUP_3: 117;

          then x in ((h .: A) * (h . b1)) by A6, A7, A8, FUNCT_2: 35;

          hence x in (C * b) by A2, GROUP_6: 2;

        end;

        hence thesis;

      end;

      hence thesis by GROUP_3: 118;

    end;

    registration

      let G be strict nilpotent Group, H be strict Group, h be Homomorphism of G, H;

      cluster ( Image h) -> nilpotent;

      coherence

      proof

        consider F be FinSequence of ( the_normal_subgroups_of G) such that

         A1: ( len F) > 0 and

         A2: (F . 1) = ( (Omega). G) and

         A3: (F . ( len F)) = ( (1). G) and

         A4: for i st i in ( dom F) & (i + 1) in ( dom F) holds for G1,G2 be strict normal Subgroup of G st G1 = (F . i) & G2 = (F . (i + 1)) holds G2 is Subgroup of G1 & (G1 ./. ((G1,G2) `*` )) is Subgroup of ( center (G ./. G2)) by Def2;

        1 <= ( len F) by A1, NAT_1: 14;

        then

         A5: 1 in ( Seg ( len F));

        defpred P[ set, set] means ex J be strict normal Subgroup of G st J = (F . $1) & $2 = (h .: J);

        

         A6: for k be Nat st k in ( Seg ( len F)) holds ex x be Element of ( the_normal_subgroups_of ( Image h)) st P[k, x]

        proof

          let k be Nat;

          assume k in ( Seg ( len F));

          then k in ( dom F) by FINSEQ_1:def 3;

          then (F . k) in ( the_normal_subgroups_of G) by FINSEQ_2: 11;

          then (F . k) is strict normal Subgroup of G by Def1;

          then

          consider A be strict normal Subgroup of G such that

           A7: A = (F . k);

          (h .: A) is strict normal Subgroup of ( Image h) by Th26;

          then (h .: A) in ( the_normal_subgroups_of ( Image h)) by Def1;

          hence thesis by A7;

        end;

        consider Z be FinSequence of ( the_normal_subgroups_of ( Image h)) such that

         A8: ( dom Z) = ( Seg ( len F)) & for j be Nat st j in ( Seg ( len F)) holds P[j, (Z . j)] from FINSEQ_1:sch 5( A6);

        ( Seg ( len Z)) = ( Seg ( len F)) by A8, FINSEQ_1:def 3;

        

        then

         A9: ( dom F) = ( Seg ( len Z)) by FINSEQ_1:def 3

        .= ( dom Z) by FINSEQ_1:def 3;

        

         A10: for i st i in ( dom Z) & (i + 1) in ( dom Z) holds for H1,H2 be strict normal Subgroup of ( Image h) st H1 = (Z . i) & H2 = (Z . (i + 1)) holds H2 is strict Subgroup of H1 & (H1 ./. ((H1,H2) `*` )) is Subgroup of ( center (( Image h) ./. H2))

        proof

          let i;

          assume

           A11: i in ( dom Z) & (i + 1) in ( dom Z);

          let H1,H2 be strict normal Subgroup of ( Image h);

          assume that

           A12: H1 = (Z . i) and

           A13: H2 = (Z . (i + 1));

          

           A14: i in ( dom F) & (i + 1) in ( dom F) by A8, A11, FINSEQ_1:def 3;

          consider G1 be strict normal Subgroup of G such that

           A15: G1 = (F . i) and

           A16: H1 = (h .: G1) by A8, A11, A12;

          consider G2 be strict normal Subgroup of G such that

           A17: G2 = (F . (i + 1)) and

           A18: H2 = (h .: G2) by A8, A11, A13;

          

           A19: G2 is strict Subgroup of G1 by A4, A9, A11, A15, A17;

          (G1 ./. ((G1,G2) `*` )) is Subgroup of ( center (G ./. G2)) by A14, A15, A17, A4;

          hence thesis by A16, A19, A18, Th25, GRSOLV_1: 12;

        end;

        take Z;

        

         A20: ( len Z) = ( len F) by A8, FINSEQ_1:def 3;

        (Z . 1) = ( (Omega). ( Image h)) & (Z . ( len Z)) = ( (1). ( Image h))

        proof

          ex G1 be strict normal Subgroup of G st G1 = (F . 1) & (Z . 1) = (h .: G1) by A8, A5;

          hence (Z . 1) = ( (Omega). ( Image h)) by A2, GRSOLV_1: 11;

          ex G2 be strict normal Subgroup of G st G2 = (F . ( len F)) & (Z . ( len F)) = (h .: G2) by A1, A8, FINSEQ_1: 3;

          

          hence (Z . ( len Z)) = ( (1). H) by A3, A20, GRSOLV_1: 11

          .= ( (1). ( Image h)) by GROUP_2: 63;

        end;

        hence thesis by A1, A8, A10, FINSEQ_1:def 3;

      end;

    end

    registration

      let G be strict nilpotent Group, N be strict normal Subgroup of G;

      cluster (G ./. N) -> nilpotent;

      coherence

      proof

        ( Image ( nat_hom N)) = (G ./. N) by GROUP_6: 48;

        hence thesis;

      end;

    end

    theorem :: GRNILP_1:27

    for G be Group st ex F be FinSequence of ( the_normal_subgroups_of G) st ( len F) > 0 & (F . 1) = ( (Omega). G) & (F . ( len F)) = ( (1). G) & for i st i in ( dom F) & (i + 1) in ( dom F) holds for G1 be strict normal Subgroup of G st G1 = (F . i) holds [.G1, ( (Omega). G).] = (F . (i + 1)) holds G is nilpotent

    proof

      let G be Group;

      given F be FinSequence of ( the_normal_subgroups_of G) such that

       A1: ( len F) > 0 & (F . 1) = ( (Omega). G) & (F . ( len F)) = ( (1). G) and

       A2: for i st i in ( dom F) & (i + 1) in ( dom F) holds for G1 be strict normal Subgroup of G st G1 = (F . i) holds [.G1, ( (Omega). G).] = (F . (i + 1));

      for i st i in ( dom F) & (i + 1) in ( dom F) holds for H1,H2 be strict normal Subgroup of G st H1 = (F . i) & H2 = (F . (i + 1)) holds H2 is Subgroup of H1 & [.H1, ( (Omega). G).] is Subgroup of H2

      proof

        let i;

        assume

         A3: i in ( dom F) & (i + 1) in ( dom F);

        let H1,H2 be strict normal Subgroup of G;

        assume H1 = (F . i) & H2 = (F . (i + 1));

        then H2 = [.H1, ( (Omega). G).] by A2, A3;

        hence thesis by Th15, GROUP_2: 54;

      end;

      hence thesis by A1, Th21;

    end;

    theorem :: GRNILP_1:28

    for G be Group st ex F be FinSequence of ( the_normal_subgroups_of G) st ( len F) > 0 & (F . 1) = ( (Omega). G) & (F . ( len F)) = ( (1). G) & for i st i in ( dom F) & (i + 1) in ( dom F) holds for G1,G2 be strict normal Subgroup of G st G1 = (F . i) & G2 = (F . (i + 1)) holds G2 is Subgroup of G1 & (G ./. G2) is commutative Group holds G is nilpotent

    proof

      let G be Group;

      given F be FinSequence of ( the_normal_subgroups_of G) such that

       A1: ( len F) > 0 & (F . 1) = ( (Omega). G) & (F . ( len F)) = ( (1). G) and

       A2: for i st i in ( dom F) & (i + 1) in ( dom F) holds for G1,G2 be strict normal Subgroup of G st G1 = (F . i) & G2 = (F . (i + 1)) holds G2 is Subgroup of G1 & (G ./. G2) is commutative Group;

      

       A3: for i st i in ( dom F) & (i + 1) in ( dom F) holds for H1,H2 be strict normal Subgroup of G st H1 = (F . i) & H2 = (F . (i + 1)) holds H2 is Subgroup of H1 & (H1 ./. ((H1,H2) `*` )) is Subgroup of ( center (G ./. H2))

      proof

        let i;

        assume

         A4: i in ( dom F) & (i + 1) in ( dom F);

        let H1,H2 be strict normal Subgroup of G;

        assume

         A5: H1 = (F . i) & H2 = (F . (i + 1));

        then H2 is Subgroup of H1 by A2, A4;

        then

         A6: (H1 ./. ((H1,H2) `*` )) is Subgroup of (G ./. H2) by GROUP_6: 28;

        (G ./. H2) is commutative Group by A2, A4, A5;

        hence thesis by A2, A4, A5, A6, GROUP_5: 82;

      end;

      take F;

      thus thesis by A1, A3;

    end;

    theorem :: GRNILP_1:29

    for G be Group st ex F be FinSequence of ( the_normal_subgroups_of G) st ( len F) > 0 & (F . 1) = ( (Omega). G) & (F . ( len F)) = ( (1). G) & for i st i in ( dom F) & (i + 1) in ( dom F) holds for G1,G2 be strict normal Subgroup of G st G1 = (F . i) & G2 = (F . (i + 1)) holds G2 is Subgroup of G1 & (G ./. G2) is cyclic Group holds G is nilpotent

    proof

      let G be Group;

      given F be FinSequence of ( the_normal_subgroups_of G) such that

       A1: ( len F) > 0 & (F . 1) = ( (Omega). G) & (F . ( len F)) = ( (1). G) and

       A2: for i st i in ( dom F) & (i + 1) in ( dom F) holds for G1,G2 be strict normal Subgroup of G st G1 = (F . i) & G2 = (F . (i + 1)) holds G2 is Subgroup of G1 & (G ./. G2) is cyclic Group;

      

       A3: for i st i in ( dom F) & (i + 1) in ( dom F) holds for H1,H2 be strict normal Subgroup of G st H1 = (F . i) & H2 = (F . (i + 1)) holds H2 is strict Subgroup of H1 & (H1 ./. ((H1,H2) `*` )) is Subgroup of ( center (G ./. H2))

      proof

        let i;

        assume

         A4: i in ( dom F) & (i + 1) in ( dom F);

        let H1,H2 be strict normal Subgroup of G;

        assume

         A5: H1 = (F . i) & H2 = (F . (i + 1));

        then H2 is strict Subgroup of H1 by A2, A4;

        then

         A6: (H1 ./. ((H1,H2) `*` )) is Subgroup of (G ./. H2) by GROUP_6: 28;

        (G ./. H2) is commutative Group by A2, A4, A5;

        hence thesis by A2, A4, A5, A6, GROUP_5: 82;

      end;

      take F;

      thus thesis by A1, A3;

    end;

    registration

      cluster nilpotent -> solvable for Group;

      correctness

      proof

        let G be Group;

        assume G is nilpotent;

        then

        consider F be FinSequence of ( the_normal_subgroups_of G) such that

         A1: ( len F) > 0 & (F . 1) = ( (Omega). G) & (F . ( len F)) = ( (1). G) & for i st i in ( dom F) & (i + 1) in ( dom F) holds for G1,G2 be strict normal Subgroup of G st G1 = (F . i) & G2 = (F . (i + 1)) holds G2 is Subgroup of G1 & (G1 ./. ((G1,G2) `*` )) is Subgroup of ( center (G ./. G2));

        reconsider R = F as FinSequence of ( Subgroups G) by Th18;

        

         A2: for i st i in ( dom R) & (i + 1) in ( dom R) holds for H1,H2 be Subgroup of G st H1 = (R . i) & H2 = (R . (i + 1)) holds H2 is strict normal Subgroup of H1 & for N be normal Subgroup of H1 st N = H2 holds (H1 ./. N) is commutative

        proof

          let i;

          assume

           A3: i in ( dom R) & (i + 1) in ( dom R);

          then

           A4: (F . i) is strict normal Subgroup of G & (F . (i + 1)) is strict normal Subgroup of G by Th16;

          let H1,H2 be Subgroup of G;

          assume

           A5: H1 = (R . i) & H2 = (R . (i + 1));

          for N be normal Subgroup of H1 st N = H2 holds (H1 ./. N) is commutative

          proof

            let N be normal Subgroup of H1;

            assume

             A6: N = H2;

            then

            reconsider N9 = N as strict normal Subgroup of G by A5, A4;

            

             A7: (H1 ./. ((H1,N9) `*` )) is Subgroup of ( center (G ./. N9)) by A1, A3, A5, A6, A4;

            ( center (G ./. N9)) is commutative by GROUP_5: 80;

            hence (H1 ./. N) is commutative by A7, GROUP_6:def 1;

          end;

          hence thesis by A1, A3, A5, A4, GROUP_6: 8;

        end;

        take R;

        thus thesis by A1, A2;

      end;

    end