group_6.miz

    begin

    theorem :: GROUP_6:1



     Th1: for A,B be non empty set, f be Function of A, B holds f is one-to-one iff for a,b be Element of A st (f . a) = (f . b) holds a = b

    proof

      let A,B be non empty set;

      let f be Function of A, B;

      thus f is one-to-one implies for a,b be Element of A st (f . a) = (f . b) holds a = b by FUNCT_2: 19;

      assume for a,b be Element of A st (f . a) = (f . b) holds a = b;

      then for a,b be object st a in A & b in A & (f . a) = (f . b) holds a = b;

      hence thesis by FUNCT_2: 19;

    end;

    definition

      let G be Group, A be Subgroup of G;

      :: original: Subgroup

      redefine

      mode Subgroup of A -> Subgroup of G ;

      coherence by GROUP_2: 56;

    end

    registration

      let G be Group;

      cluster ( (1). G) -> normal;

      coherence by GROUP_3: 114;

      cluster ( (Omega). G) -> normal;

      coherence by GROUP_3: 114;

    end

    reserve n for Element of NAT ;

    reserve i for Integer;

    reserve G,H,I for Group;

    reserve A,B for Subgroup of G;

    reserve N for normal Subgroup of G;

    reserve a,a1,a2,a3,b,b1 for Element of G;

    reserve c,d for Element of H;

    reserve f for Function of the carrier of G, the carrier of H;

    reserve x,y,y1,y2,z for set;

    reserve A1,A2 for Subset of G;

    theorem :: GROUP_6:2



     Th2: for X be Subgroup of A, x be Element of A st x = a holds (x * X) = (a * X qua Subgroup of G) & (X * x) = (X qua Subgroup of G * a)

    proof

      let X be Subgroup of A, x be Element of A;

      set I = X qua Subgroup of G;

      assume

       A1: x = a;

      thus (x * X) c= (a * I)

      proof

        let y be object;

        assume y in (x * X);

        then

        consider g be Element of A such that

         A2: y = (x * g) & g in X by GROUP_2: 103;

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

        (a * h) = (x * g) by A1, GROUP_2: 43;

        hence thesis by A2, GROUP_2: 103;

      end;

      thus (a * I) c= (x * X)

      proof

        let y be object;

        assume y in (a * I);

        then

        consider b such that

         A3: y = (a * b) and

         A4: b in X by GROUP_2: 103;

        reconsider c = b as Element of X by A4;

        reconsider c as Element of A by GROUP_2: 42;

        (a * b) = (x * c) by A1, GROUP_2: 43;

        hence thesis by A3, A4, GROUP_2: 103;

      end;

      thus (X * x) c= (I * a)

      proof

        let y be object;

        assume y in (X * x);

        then

        consider g be Element of A such that

         A5: y = (g * x) & g in X by GROUP_2: 104;

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

        (h * a) = (g * x) by A1, GROUP_2: 43;

        hence thesis by A5, GROUP_2: 104;

      end;

      thus (I * a) c= (X * x)

      proof

        let y be object;

        assume y in (I * a);

        then

        consider b such that

         A6: y = (b * a) and

         A7: b in X by GROUP_2: 104;

        reconsider c = b as Element of X by A7;

        reconsider c as Element of A by GROUP_2: 42;

        (b * a) = (c * x) by A1, GROUP_2: 43;

        hence thesis by A6, A7, GROUP_2: 104;

      end;

    end;

    theorem :: GROUP_6:3

    for X,Y be Subgroup of A holds (X qua Subgroup of G /\ Y qua Subgroup of G) = (X /\ Y)

    proof

      let X,Y be Subgroup of A;

      reconsider Z = (X /\ Y) as Subgroup of G by GROUP_2: 56;

      the carrier of (X /\ Y) = (( carr X) /\ ( carr Y)) by GROUP_2:def 10;

      then (X qua Subgroup of G /\ Y qua Subgroup of G) = Z by GROUP_2: 80;

      hence thesis;

    end;

    theorem :: GROUP_6:4



     Th4: ((a * b) * (a " )) = (b |^ (a " )) & (a * (b * (a " ))) = (b |^ (a " ))

    proof



      thus ((a * b) * (a " )) = ((((a " ) " ) * b) * (a " ))

      .= (b |^ (a " )) by GROUP_3:def 2;

      hence thesis by GROUP_1:def 3;

    end;

    theorem :: GROUP_6:5



     Th5: ((a * A) * A) = (a * A) & (a * (A * A)) = (a * A) & ((A * A) * a) = (A * a) & (A * (A * a)) = (A * a)

    proof



      thus ((a * A) * A) = (a * (A * A)) by GROUP_4: 45

      .= (a * A) by GROUP_2: 76;

      hence (a * (A * A)) = (a * A) by GROUP_4: 45;

      thus ((A * A) * a) = (A * a) by GROUP_2: 76;

      hence thesis by GROUP_4: 46;

    end;

    theorem :: GROUP_6:6



     Th6: for G be Group, A1 be Subset of G holds A1 = the set of all [.a, b.] where a be Element of G, b be Element of G implies (G ` ) = ( gr A1)

    proof

      let G be Group, A1 be Subset of G;

      assume

       A1: A1 = the set of all [.a, b.] where a be Element of G, b be Element of G;

      A1 = ( commutators G)

      proof

        thus A1 c= ( commutators G)

        proof

          let x be object;

          assume x in A1;

          then ex a,b be Element of G st x = [.a, b.] by A1;

          hence thesis by GROUP_5: 58;

        end;

        let x be object;

        assume x in ( commutators G);

        then ex a,b be Element of G st x = [.a, b.] by GROUP_5: 58;

        hence thesis by A1;

      end;

      hence thesis by GROUP_5: 72;

    end;

    theorem :: GROUP_6:7



     Th7: for G be strict Group, B be strict Subgroup of G holds (G ` ) is Subgroup of B iff for a,b be Element of G holds [.a, b.] in B

    proof

      defpred P[ set, set] means not contradiction;

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

      thus (G ` ) is Subgroup of B implies for a,b be Element of G holds [.a, b.] in B by GROUP_2: 40, GROUP_5: 74;

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

      reconsider X = { F(a,b) where a be Element of G, b be Element of G : P[a, b] } as Subset of G from DOMAIN_1:sch 9;

      assume

       A1: for a,b be Element of G holds [.a, b.] in B;

      X c= the carrier of B

      proof

        let x be object;

        assume x in X;

        then ex a,b be Element of G st x = [.a, b.];

        then x in B by A1;

        hence thesis;

      end;

      then ( gr X) is Subgroup of B by GROUP_4:def 4;

      hence thesis by Th6;

    end;

    theorem :: GROUP_6:8



     Th8: for N be normal Subgroup of G holds N is Subgroup of B implies N is normal Subgroup of B

    proof

      let N be normal Subgroup of G;

      assume N is Subgroup of B;

      then

      reconsider N9 = N as Subgroup of B;

      now

        let n be Element of B;

        thus (n * N9) c= (N9 * n)

        proof

          let x be object;

          assume x in (n * N9);

          then

          consider a be Element of B such that

           A1: x = (n * a) and

           A2: a in N9 by GROUP_2: 103;

          reconsider a9 = a, n9 = n as Element of G by GROUP_2: 42;

          x = (n9 * a9) by A1, GROUP_2: 43;

          then

           A3: x in (n9 * N) by A2, GROUP_2: 103;

          (n9 * N) c= (N * n9) by GROUP_3: 118;

          then

          consider a1 such that

           A4: x = (a1 * n9) and

           A5: a1 in N by A3, GROUP_2: 104;

          a1 in N9 by A5;

          then a1 in B by GROUP_2: 40;

          then

          reconsider a19 = a1 as Element of B;

          x = (a19 * n) by A4, GROUP_2: 43;

          hence thesis by A5, GROUP_2: 104;

        end;

      end;

      hence thesis by GROUP_3: 118;

    end;

    definition

      let G, B;

      let M be normal Subgroup of G;

      assume

       A1: the multMagma of M is Subgroup of B;

      :: GROUP_6:def1

      func (B,M) `*` -> strict normal Subgroup of B equals

      : Def1: the multMagma of M;

      coherence

      proof

        reconsider x = the multMagma of M as Subgroup of G by A1;

        now

          let a;



          thus (a * x) = (a * M)

          .= (M * a) by GROUP_3: 117

          .= (x * a);

        end;

        then x is normal Subgroup of G by GROUP_3: 117;

        hence thesis by A1, Th8;

      end;

      correctness ;

    end

    theorem :: GROUP_6:9



     Th9: (B /\ N) is normal Subgroup of B & (N /\ B) is normal Subgroup of B

    proof

      thus (B /\ N) is normal Subgroup of B

      proof

        reconsider A = (B /\ N) as Subgroup of B by GROUP_2: 88;

        now

          let b be Element of B;

          thus (b * A) c= (A * b)

          proof

            let x be object;

            assume x in (b * A);

            then

            consider a be Element of B such that

             A1: x = (b * a) and

             A2: a in A by GROUP_2: 103;

            reconsider a9 = a, b9 = b as Element of G by GROUP_2: 42;

            a in N & x = (b9 * a9) by A1, A2, GROUP_2: 43, GROUP_2: 82;

            then

             A3: x in (b9 * N) by GROUP_2: 103;

            reconsider x9 = x as Element of B by A1;



             A4: (b9 " ) = (b " ) by GROUP_2: 48;

            (b9 * N) c= (N * b9) by GROUP_3: 118;

            then

            consider b1 such that

             A5: x = (b1 * b9) and

             A6: b1 in N by A3, GROUP_2: 104;

            reconsider x99 = x as Element of G by A5;

            b1 = (x99 * (b9 " )) by A5, GROUP_1: 14;

            then

             A7: b1 = (x9 * (b " )) by A4, GROUP_2: 43;

            then

            reconsider b19 = b1 as Element of B;

            b1 in B by A7;

            then

             A8: b19 in A by A6, GROUP_2: 82;

            (b19 * b) = x by A5, GROUP_2: 43;

            hence thesis by A8, GROUP_2: 104;

          end;

        end;

        hence thesis by GROUP_3: 118;

      end;

      hence thesis;

    end;

    definition

      let G, B;

      let N be normal Subgroup of G;

      :: original: /\

      redefine

      func B /\ N -> strict normal Subgroup of B ;

      coherence by Th9;

    end

    definition

      let G;

      let N be normal Subgroup of G;

      let B;

      :: original: /\

      redefine

      func N /\ B -> strict normal Subgroup of B ;

      coherence by Th9;

    end

    definition

      let G be non empty 1-sorted;

      :: original: trivial

      redefine

      :: GROUP_6:def2

      attr G is trivial means

      : Def2: ex x be object st the carrier of G = {x};

      compatibility

      proof

        hereby

          set y = the Element of G;

          assume G is trivial;

          then for x be object holds x in the carrier of G iff x = y;

          then the carrier of G = {y} by TARSKI:def 1;

          hence ex x be object st the carrier of G = {x};

        end;

        given x be object such that

         A1: the carrier of G = {x};

        now

          let a,b be Element of G;



          thus a = x by A1, TARSKI:def 1

          .= b by A1, TARSKI:def 1;

        end;

        hence thesis;

      end;

    end

    theorem :: GROUP_6:10



     Th10: ( (1). G) is trivial

    proof

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

      hence thesis;

    end;

    registration

      let G;

      cluster ( (1). G) -> trivial;

      coherence by Th10;

    end

    registration

      cluster strict trivial for Group;

      existence

      proof

        set G = the Group;

        take ( (1). G);

        thus thesis;

      end;

    end

    theorem :: GROUP_6:11



     Th11: (for G be trivial Group holds ( card G) = 1 & G is finite) & for G be finite Group st ( card G) = 1 holds G is trivial

    proof

      thus for G be trivial Group holds ( card G) = 1 & G is finite

      proof

        let G be trivial Group;

        ex x be object st the carrier of G = {x} by Def2;

        hence thesis by CARD_1: 30;

      end;

      let G be finite Group;

      assume ( card G) = 1;

      hence ex x be object st the carrier of G = {x} by CARD_2: 42;

    end;

    theorem :: GROUP_6:12



     Th12: for G be strict trivial Group holds ( (1). G) = G

    proof

      let G be strict trivial Group;

      ( card G) = 1 by Th11;

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

      hence thesis by GROUP_2: 73;

    end;

    notation

      let G, N;

      synonym Cosets N for Left_Cosets N;

    end

    registration

      let G, N;

      cluster ( Cosets N) -> non empty;

      coherence by GROUP_2: 135;

    end

    theorem :: GROUP_6:13



     Th13: for x be object holds for N be normal Subgroup of G holds x in ( Cosets N) implies ex a st x = (a * N) & x = (N * a)

    proof

      let x be object;

      let N be normal Subgroup of G;

      assume x in ( Cosets N);

      then

      consider a such that

       A1: x = (a * N) by GROUP_2:def 15;

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

      hence thesis by A1;

    end;

    theorem :: GROUP_6:14



     Th14: for N be normal Subgroup of G holds (a * N) in ( Cosets N) & (N * a) in ( Cosets N)

    proof

      let N be normal Subgroup of G;

      (N * a) in ( Right_Cosets N) by GROUP_2:def 16;

      hence thesis by GROUP_2:def 15, GROUP_3: 127;

    end;

    theorem :: GROUP_6:15



     Th15: for N be normal Subgroup of G holds x in ( Cosets N) implies x is Subset of G;

    theorem :: GROUP_6:16



     Th16: for N be normal Subgroup of G holds A1 in ( Cosets N) & A2 in ( Cosets N) implies (A1 * A2) in ( Cosets N)

    proof

      let N be normal Subgroup of G;

      assume that

       A1: A1 in ( Cosets N) and

       A2: A2 in ( Cosets N);

      consider a such that

       A3: A1 = (a * N) and A1 = (N * a) by A1, Th13;

      consider b such that

       A4: A2 = (b * N) and

       A5: A2 = (N * b) by A2, Th13;

      (A1 * A2) = (a * (N * (b * N))) by A3, A4, GROUP_3: 10

      .= (a * ((b * N) * N)) by A4, A5, GROUP_3: 13

      .= (a * (b * (N * N))) by GROUP_4: 45

      .= (a * (b * N)) by GROUP_2: 76

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

      hence thesis by GROUP_2:def 15;

    end;

    definition

      let G;

      let N be normal Subgroup of G;

      :: GROUP_6:def3

      func CosOp N -> BinOp of ( Cosets N) means

      : Def3: for W1,W2 be Element of ( Cosets N) holds for A1, A2 st W1 = A1 & W2 = A2 holds (it . (W1,W2)) = (A1 * A2);

      existence

      proof

        defpred P[ Element of ( Cosets N), Element of ( Cosets N), set] means for A1, A2 st $1 = A1 & $2 = A2 holds $3 = (A1 * A2);



         A1: for W1,W2 be Element of ( Cosets N) holds ex V be Element of ( Cosets N) st P[W1, W2, V]

        proof

          let W1,W2 be Element of ( Cosets N);

          reconsider A1 = W1, A2 = W2 as Subset of G by Th15;

          reconsider C = (A1 * A2) as Element of ( Cosets N) by Th16;

          take C;

          thus thesis;

        end;

        thus ex B be BinOp of ( Cosets N) st for W1,W2 be Element of ( Cosets N) holds P[W1, W2, (B . (W1,W2))] from BINOP_1:sch 3( A1);

      end;

      uniqueness

      proof

        let o1,o2 be BinOp of ( Cosets N);

        assume

         A2: for W1,W2 be Element of ( Cosets N) holds for A1, A2 st W1 = A1 & W2 = A2 holds (o1 . (W1,W2)) = (A1 * A2);

        assume

         A3: for W1,W2 be Element of ( Cosets N) holds for A1, A2 st W1 = A1 & W2 = A2 holds (o2 . (W1,W2)) = (A1 * A2);

        now

          let x,y be set;

          assume

           A4: x in ( Cosets N) & y in ( Cosets N);

          then

          reconsider W = x, V = y as Element of ( Cosets N);

          reconsider A1 = x, A2 = y as Subset of G by A4;

          (o1 . (W,V)) = (A1 * A2) by A2;

          hence (o1 . (x,y)) = (o2 . (x,y)) by A3;

        end;

        hence thesis;

      end;

    end

    definition

      let G;

      let N be normal Subgroup of G;

      :: GROUP_6:def4

      func G ./. N -> multMagma equals multMagma (# ( Cosets N), ( CosOp N) #);

      correctness ;

    end

    registration

      let G;

      let N be normal Subgroup of G;

      cluster (G ./. N) -> strict non empty;

      coherence ;

    end

    theorem :: GROUP_6:17

    for N be normal Subgroup of G holds the carrier of (G ./. N) = ( Cosets N);

    theorem :: GROUP_6:18

    for N be normal Subgroup of G holds the multF of (G ./. N) = ( CosOp N);

    reserve N for normal Subgroup of G;

    reserve S,T1,T2 for Element of (G ./. N);

    definition

      let G, N, S;

      :: GROUP_6:def5

      func @ S -> Subset of G equals S;

      coherence by Th15;

    end

    theorem :: GROUP_6:19

    for N be normal Subgroup of G, T1,T2 be Element of (G ./. N) holds (( @ T1) * ( @ T2)) = (T1 * T2) by Def3;

    theorem :: GROUP_6:20

    ( @ (T1 * T2)) = (( @ T1) * ( @ T2)) by Def3;

    registration

      let G;

      let N be normal Subgroup of G;

      cluster (G ./. N) -> associative Group-like;

      coherence

      proof

        thus for f,g,h be Element of (G ./. N) holds (f * (g * h)) = ((f * g) * h)

        proof

          let f,g,h be Element of (G ./. N);

          consider a such that

           A1: f = (a * N) and f = (N * a) by Th13;

          consider c be Element of G such that

           A2: h = (c * N) and h = (N * c) by Th13;



          thus (f * (g * h)) = (( @ f) * ( @ (g * h))) by Def3

          .= ((a * N) * (( @ g) * ( @ h))) by A1, Def3

          .= ((( @ f) * ( @ g)) * (c * N)) by A1, A2, GROUP_2: 10

          .= (( @ (f * g)) * ( @ h)) by A2, Def3

          .= ((f * g) * h) by Def3;

        end;

        reconsider e = ( carr N) as Element of (G ./. N) by GROUP_2: 135;

        take e;

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

        consider a such that

         A3: h = (a * N) and

         A4: h = (N * a) by Th13;



        thus (h * e) = ((a * N) * N) by A3, Def3

        .= (a * (N * N)) by GROUP_4: 45

        .= h by A3, GROUP_2: 76;



        thus (e * h) = (N * (N * a)) by A4, Def3

        .= ((N * N) * a) by GROUP_4: 46

        .= h by A4, GROUP_2: 76;

        reconsider g = ((a " ) * N) as Element of (G ./. N) by GROUP_2:def 15;

        take g;



        thus (h * g) = ((N * a) * ((a " ) * N)) by A4, Def3

        .= (((N * a) * (a " )) * N) by GROUP_3: 9

        .= ((N * (a * (a " ))) * N) by GROUP_2: 107

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

        .= (( carr N) * ( carr N)) by GROUP_2: 109

        .= e by GROUP_2: 76;



        thus (g * h) = (( @ g) * ( @ h)) by Def3

        .= ((((a " ) * N) * a) * N) by A3, GROUP_3: 9

        .= (((a " ) * (N * a)) * N) by GROUP_2: 106

        .= (((a " ) * (a * N)) * N) by GROUP_3: 117

        .= ((((a " ) * a) * N) * N) by GROUP_2: 105

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

        .= (( 1_ G) * (N * N)) by GROUP_4: 45

        .= (( 1_ G) * ( carr N)) by GROUP_2: 76

        .= e by GROUP_2: 37;

      end;

    end

    theorem :: GROUP_6:21

    for N be normal Subgroup of G, S be Element of (G ./. N) holds ex a st S = (a * N) & S = (N * a) by Th13;

    theorem :: GROUP_6:22

    (N * a) is Element of (G ./. N) & (a * N) is Element of (G ./. N) & ( carr N) is Element of (G ./. N) by Th14, GROUP_2: 135;

    theorem :: GROUP_6:23



     Th23: for x be object holds for N be normal Subgroup of G holds x in (G ./. N) iff ex a st x = (a * N) & x = (N * a) by Th13, Th14;

    theorem :: GROUP_6:24



     Th24: for N be normal Subgroup of G holds ( 1_ (G ./. N)) = ( carr N)

    proof

      let N be normal Subgroup of G;

      reconsider e = ( carr N) as Element of (G ./. N) by GROUP_2: 135;

      now

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

        consider a such that

         A1: h = (a * N) and

         A2: h = (N * a) by Th13;



        thus (h * e) = ((a * N) * N) by A1, Def3

        .= (a * (N * N)) by GROUP_4: 45

        .= h by A1, GROUP_2: 76;



        thus (e * h) = (N * (N * a)) by A2, Def3

        .= ((N * N) * a) by GROUP_4: 46

        .= h by A2, GROUP_2: 76;

      end;

      hence thesis by GROUP_1: 4;

    end;

    theorem :: GROUP_6:25



     Th25: for N be normal Subgroup of G, S be Element of (G ./. N) st S = (a * N) holds (S " ) = ((a " ) * N)

    proof

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

      reconsider g = ((a " ) * N) as Element of (G ./. N) by Th14;

      assume

       A1: S = (a * N);



       A2: (g * S) = (( @ g) * ( @ S)) by Def3

      .= ((((a " ) * N) * a) * N) by A1, GROUP_3: 9

      .= (((a " ) * (N * a)) * N) by GROUP_2: 106

      .= (((a " ) * (a * N)) * N) by GROUP_3: 117

      .= ((((a " ) * a) * N) * N) by GROUP_2: 105

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

      .= (( 1_ G) * (N * N)) by GROUP_4: 45

      .= (( 1_ G) * ( carr N)) by GROUP_2: 76

      .= ( carr N) by GROUP_2: 37;



       A3: ( 1_ (G ./. N)) = ( carr N) by Th24;

      (S * g) = (( @ S) * ( @ g)) by Def3

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

      .= (((N * a) * (a " )) * N) by GROUP_3: 9

      .= ((N * (a * (a " ))) * N) by GROUP_2: 107

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

      .= (( carr N) * ( carr N)) by GROUP_2: 109

      .= ( carr N) by GROUP_2: 76;

      hence thesis by A2, A3, GROUP_1:def 5;

    end;

    theorem :: GROUP_6:26

    for N be normal Subgroup of G holds ( card (G ./. N)) = ( Index N);

    theorem :: GROUP_6:27

    for N be normal Subgroup of G holds ( Left_Cosets N) is finite implies ( card (G ./. N)) = ( index N)

    proof

      let N be normal Subgroup of G;

      assume ( Left_Cosets N) is finite;

      then

      reconsider LC = ( Left_Cosets N) as finite set;



      thus ( card (G ./. N)) = ( card LC)

      .= ( index N) by GROUP_2:def 18;

    end;

    theorem :: GROUP_6:28



     Th28: for M be strict normal Subgroup of G holds M is Subgroup of B implies (B ./. ((B,M) `*` )) is Subgroup of (G ./. M)

    proof

      let M be strict normal Subgroup of G;

      set I = (B ./. ((B,M) `*` ));

      set J = ((B,M) `*` );

      set g = the multF of I;

      set f = the multF of (G ./. M);

      set X = [:the carrier of I, the carrier of I:];

      assume

       A1: M is Subgroup of B;



       A2: the carrier of I c= the carrier of (G ./. M)

      proof

        let x be object;

        assume x in the carrier of I;

        then

        consider a be Element of B such that

         A3: x = (a * J) and x = (J * a) by Th13;

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

        J = M by A1, Def1;

        then (a * J) = (b * M) by Th2;

        hence thesis by A3, Th14;

      end;

       A4:

      now

        let x be object;

        assume

         A5: x in ( dom g);

        then

        consider y,z be object such that

         A6: [y, z] = x by RELAT_1:def 1;

        z in the carrier of I by A5, A6, ZFMISC_1: 87;

        then

        consider b be Element of B such that

         A7: z = (b * J) and

         A8: z = (J * b) by Th13;

        y in the carrier of I by A5, A6, ZFMISC_1: 87;

        then

        consider a be Element of B such that

         A9: y = (a * J) and y = (J * a) by Th13;

        reconsider W1 = y, W2 = z as Element of ( Cosets J) by A9, A7, Th14;



         A10: (g . x) = (g . (W1,W2)) by A6

        .= ((a * J) * (J * b)) by A9, A8, Def3

        .= (((a * J) * J) * b) by GROUP_3: 11

        .= ((a * (J * J)) * b) by GROUP_4: 45

        .= ((a * J) * b) by GROUP_2: 76

        .= (a * (J * b)) by GROUP_2: 106

        .= (a * (b * J)) by GROUP_3: 117

        .= ((a * b) * J) by GROUP_2: 105;

        reconsider a9 = a, b9 = b as Element of G by GROUP_2: 42;



         A11: J = M by A1, Def1;

        then

         A12: y = (a9 * M) by A9, Th2;

        z = (b9 * M) by A7, A11, Th2;

        then

        reconsider V1 = y, V2 = z as Element of ( Cosets M) by A12, Th14;



         A13: (a9 * b9) = (a * b) by GROUP_2: 43;



         A14: z = (M * b9) by A8, A11, Th2;

        (f . x) = (f . (V1,V2)) by A6

        .= ((a9 * M) * (M * b9)) by A12, A14, Def3

        .= (((a9 * M) * M) * b9) by GROUP_3: 11

        .= ((a9 * (M * M)) * b9) by GROUP_4: 45

        .= ((a9 * M) * b9) by GROUP_2: 76

        .= (a9 * (M * b9)) by GROUP_2: 106

        .= (a9 * (b9 * M)) by GROUP_3: 117

        .= ((a9 * b9) * M) by GROUP_2: 105;

        hence (g . x) = (f . x) by A10, A11, A13, Th2;

      end;

      ( dom g) = X & ( dom f) = [:the carrier of (G ./. M), the carrier of (G ./. M):] by FUNCT_2:def 1;

      then ( dom g) = (( dom f) /\ X) by A2, XBOOLE_1: 28, ZFMISC_1: 96;

      then g = (f || the carrier of I) by A4, FUNCT_1: 46;

      hence thesis by A2, GROUP_2:def 5;

    end;

    theorem :: GROUP_6:29

    for N,M be strict normal Subgroup of G holds M is Subgroup of N implies (N ./. ((N,M) `*` )) is normal Subgroup of (G ./. M)

    proof

      let N,M be strict normal Subgroup of G;

      assume

       A1: M is Subgroup of N;

      then

       A2: ((N,M) `*` ) = M by Def1;

      then

      reconsider I = M as normal Subgroup of N;

      reconsider J = (N ./. ((N,M) `*` )) as Subgroup of (G ./. M) by A1, Th28;

      now

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

        thus (S * J) c= (J * S)

        proof

          let x be object;

          assume x in (S * J);

          then

          consider T be Element of (G ./. M) such that

           A3: x = (S * T) and

           A4: T in J by GROUP_2: 103;

          consider c be Element of N such that T = (c * I) and

           A5: T = (I * c) by A2, A4, Th23;

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

          consider a such that S = (a * M) and

           A6: S = (M * a) by Th13;

          set e = (a * (d * (a " )));

          c in N & e = (d |^ (a " )) by Th4;

          then e in N by GROUP_5: 3;

          then

          reconsider f = e as Element of N;



           A7: (M * e) = (I * f) by Th2;

          reconsider V = (I * f) as Element of J by A2, Th14;



           A8: V in J;

          reconsider V as Element of (G ./. M) by GROUP_2: 42;

          (M * d) = (I * c) by Th2;



          then x = ((M * a) * (M * d)) by A3, A6, A5, Def3

          .= ((M * a) * ((M * d) * ( 1_ G))) by GROUP_2: 37

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

          .= ((M * a) * (M * (d * ((a " ) * a)))) by GROUP_2: 107

          .= (((M * a) * M) * (d * ((a " ) * a))) by GROUP_3: 11

          .= ((M * (a * M)) * (d * ((a " ) * a))) by GROUP_3: 13

          .= ((M * (M * a)) * (d * ((a " ) * a))) by GROUP_3: 117

          .= (M * ((M * a) * (d * ((a " ) * a)))) by GROUP_2: 98

          .= (M * (M * (a * (d * ((a " ) * a))))) by GROUP_2: 107

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

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

          .= (M * ((M * e) * a)) by GROUP_2: 107

          .= (M * ((e * M) * a)) by GROUP_3: 117

          .= (M * (e * (M * a))) by GROUP_2: 106

          .= ((M * e) * (M * a)) by GROUP_3: 12

          .= (V * S) by A6, A7, Def3;

          hence thesis by A8, GROUP_2: 104;

        end;

      end;

      hence thesis by GROUP_3: 118;

    end;

    theorem :: GROUP_6:30

    for G be strict Group, N be strict normal Subgroup of G holds (G ./. N) is commutative Group iff (G ` ) is Subgroup of N

    proof

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

      thus (G ./. N) is commutative Group implies (G ` ) is Subgroup of N

      proof

        assume

         A1: (G ./. N) is commutative Group;

        now

          let a,b be Element of G;

          reconsider S = (a * N), T = (b * N) as Element of (G ./. N) by Th14;



           A2: [.S, T.] = ( 1_ (G ./. N)) & ( 1_ (G ./. N)) = ( carr N) by A1, Th24, GROUP_5: 37;

          (S " ) = ((a " ) * N) & (T " ) = ((b " ) * N) by Th25;

          then

           A3: ((S " ) * (T " )) = (((a " ) * N) * ((b " ) * N)) by Def3;

          (S * T) = ((a * N) * (b * N)) & [.S, T.] = (((S " ) * (T " )) * (S * T)) by Def3, GROUP_5: 16;

          then [.S, T.] = ((((a " ) * N) * ((b " ) * N)) * ((a * N) * (b * N))) by A3, Def3;



          then ( carr N) = ((((a " ) * N) * ((b " ) * N)) * (a * (N * (b * N)))) by A2, GROUP_3: 10

          .= ((((a " ) * N) * ((b " ) * N)) * (a * ((N * b) * N))) by GROUP_3: 13

          .= ((((a " ) * N) * ((b " ) * N)) * (a * ((b * N) * N))) by GROUP_3: 117

          .= ((((a " ) * N) * ((b " ) * N)) * (a * (b * N))) by Th5

          .= ((((a " ) * N) * ((b " ) * N)) * ((a * b) * N)) by GROUP_2: 105

          .= (((a " ) * (N * ((b " ) * N))) * ((a * b) * N)) by GROUP_3: 10

          .= (((a " ) * ((N * (b " )) * N)) * ((a * b) * N)) by GROUP_3: 13

          .= (((a " ) * (((b " ) * N) * N)) * ((a * b) * N)) by GROUP_3: 117

          .= (((a " ) * ((b " ) * N)) * ((a * b) * N)) by Th5

          .= ((((a " ) * (b " )) * N) * ((a * b) * N)) by GROUP_2: 105

          .= (((a " ) * (b " )) * (N * ((a * b) * N))) by GROUP_3: 10

          .= (((a " ) * (b " )) * ((N * (a * b)) * N)) by GROUP_3: 13

          .= (((a " ) * (b " )) * (((a * b) * N) * N)) by GROUP_3: 117

          .= (((a " ) * (b " )) * ((a * b) * N)) by Th5

          .= ((((a " ) * (b " )) * (a * b)) * N) by GROUP_2: 105

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

          hence [.a, b.] in N by GROUP_2: 113;

        end;

        hence thesis by Th7;

      end;

      assume

       A4: (G ` ) is Subgroup of N;

      now

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



         A5: [.S, T.] = (((S " ) * (T " )) * (S * T)) by GROUP_5: 16;

        consider b be Element of G such that

         A6: T = (b * N) and T = (N * b) by Th13;



         A7: (T " ) = ((b " ) * N) by A6, Th25;

        consider a be Element of G such that

         A8: S = (a * N) and S = (N * a) by Th13;

        (S " ) = ((a " ) * N) by A8, Th25;

        then

         A9: ((S " ) * (T " )) = (((a " ) * N) * ((b " ) * N)) by A7, Def3;

         [.a, b.] in N by A4, Th7;



        then

         A10: ( carr N) = ( [.a, b.] * N) by GROUP_2: 113

        .= ((((a " ) * (b " )) * (a * b)) * N) by GROUP_5: 16

        .= (((a " ) * (b " )) * ((a * b) * N)) by GROUP_2: 105

        .= (((a " ) * (b " )) * (((a * b) * N) * N)) by Th5

        .= (((a " ) * (b " )) * ((N * (a * b)) * N)) by GROUP_3: 117

        .= (((a " ) * (b " )) * (N * ((a * b) * N))) by GROUP_3: 13

        .= ((((a " ) * (b " )) * N) * ((a * b) * N)) by GROUP_3: 10

        .= (((a " ) * ((b " ) * N)) * ((a * b) * N)) by GROUP_2: 105

        .= (((a " ) * (((b " ) * N) * N)) * ((a * b) * N)) by Th5

        .= (((a " ) * ((N * (b " )) * N)) * ((a * b) * N)) by GROUP_3: 117

        .= (((a " ) * (N * ((b " ) * N))) * ((a * b) * N)) by GROUP_3: 13

        .= ((((a " ) * N) * ((b " ) * N)) * ((a * b) * N)) by GROUP_3: 10

        .= ((((a " ) * N) * ((b " ) * N)) * (a * (b * N))) by GROUP_2: 105

        .= ((((a " ) * N) * ((b " ) * N)) * (a * ((b * N) * N))) by Th5

        .= ((((a " ) * N) * ((b " ) * N)) * (a * ((N * b) * N))) by GROUP_3: 117

        .= ((((a " ) * N) * ((b " ) * N)) * (a * (N * (b * N)))) by GROUP_3: 13

        .= ((((a " ) * N) * ((b " ) * N)) * ((a * N) * (b * N))) by GROUP_3: 10;

        (S * T) = ((a * N) * (b * N)) by A8, A6, Def3;

        then [.S, T.] = ((((a " ) * N) * ((b " ) * N)) * ((a * N) * (b * N))) by A9, A5, Def3;

        hence [.S, T.] = ( 1_ (G ./. N)) by A10, Th24;

      end;

      hence thesis by GROUP_5: 37;

    end;



     Lm1: for G,H be unital non empty multMagma, f be Function of G, H holds (for a be Element of G holds (f . a) = ( 1_ H)) implies for a,b be Element of G holds (f . (a * b)) = ((f . a) * (f . b))

    proof

      let G,H be unital non empty multMagma, f be Function of G, H;

      assume

       A1: for a be Element of G holds (f . a) = ( 1_ H);

      let a,b be Element of G;



      thus (f . (a * b)) = ( 1_ H) by A1

      .= (( 1_ H) * ( 1_ H)) by GROUP_1:def 4

      .= ((f . a) * ( 1_ H)) by A1

      .= ((f . a) * (f . b)) by A1;

    end;

    definition

      let G,H be non empty multMagma;

      let f be Function of G, H;

      :: GROUP_6:def6

      attr f is multiplicative means

      : Def6: for a,b be Element of G holds (f . (a * b)) = ((f . a) * (f . b));

    end

    registration

      let G,H be unital non empty multMagma;

      cluster multiplicative for Function of G, H;

      existence

      proof

        take f = (G --> ( 1_ H));

        for a be Element of G holds (f . a) = ( 1_ H) by FUNCOP_1: 7;

        hence for a,b be Element of G holds (f . (a * b)) = ((f . a) * (f . b)) by Lm1;

      end;

    end

    definition

      let G, H;

      mode Homomorphism of G,H is multiplicative Function of G, H;

    end

    reserve g,h for Homomorphism of G, H;

    reserve h1 for Homomorphism of H, I;

    theorem :: GROUP_6:31



     Th31: (g . ( 1_ G)) = ( 1_ H)

    proof

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

      .= ((g . ( 1_ G)) * (g . ( 1_ G))) by Def6;

      hence thesis by GROUP_1: 7;

    end;

    registration

      let G, H;

      cluster -> unity-preserving for Homomorphism of G, H;

      coherence by Th31;

    end

    theorem :: GROUP_6:32



     Th32: (g . (a " )) = ((g . a) " )

    proof

      ((g . (a " )) * (g . a)) = (g . ((a " ) * a)) by Def6

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

      .= ( 1_ H) by Th31;

      hence thesis by GROUP_1: 12;

    end;

    theorem :: GROUP_6:33



     Th33: (g . (a |^ b)) = ((g . a) |^ (g . b))

    proof



      thus (g . (a |^ b)) = (g . (((b " ) * a) * b)) by GROUP_3:def 2

      .= ((g . ((b " ) * a)) * (g . b)) by Def6

      .= (((g . (b " )) * (g . a)) * (g . b)) by Def6

      .= ((((g . b) " ) * (g . a)) * (g . b)) by Th32

      .= ((g . a) |^ (g . b)) by GROUP_3:def 2;

    end;

    theorem :: GROUP_6:34



     Th34: (g . [.a, b.]) = [.(g . a), (g . b).]

    proof



      thus (g . [.a, b.]) = (g . ((((a " ) * (b " )) * a) * b)) by GROUP_5: 16

      .= ((g . (((a " ) * (b " )) * a)) * (g . b)) by Def6

      .= (((g . ((a " ) * (b " ))) * (g . a)) * (g . b)) by Def6

      .= ((((g . (a " )) * (g . (b " ))) * (g . a)) * (g . b)) by Def6

      .= (((((g . a) " ) * (g . (b " ))) * (g . a)) * (g . b)) by Th32

      .= (((((g . a) " ) * ((g . b) " )) * (g . a)) * (g . b)) by Th32

      .= [.(g . a), (g . b).] by GROUP_5: 16;

    end;

    theorem :: GROUP_6:35

    (g . [.a1, a2, a3.]) = [.(g . a1), (g . a2), (g . a3).]

    proof



      thus (g . [.a1, a2, a3.]) = (g . [. [.a1, a2.], a3.]) by GROUP_5:def 3

      .= [.(g . [.a1, a2.]), (g . a3).] by Th34

      .= [. [.(g . a1), (g . a2).], (g . a3).] by Th34

      .= [.(g . a1), (g . a2), (g . a3).] by GROUP_5:def 3;

    end;

    theorem :: GROUP_6:36



     Th36: (g . (a |^ n)) = ((g . a) |^ n)

    proof

      defpred Q[ Nat] means (g . (a |^ $1)) = ((g . a) |^ $1);



       A1: for n be Nat st Q[n] holds Q[(n + 1)]

      proof

        let n be Nat;

        assume

         A2: Q[n];



        thus (g . (a |^ (n + 1))) = (g . ((a |^ n) * a)) by GROUP_1: 34

        .= (((g . a) |^ n) * (g . a)) by A2, Def6

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

      end;

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

      .= ( 1_ H) by Th31

      .= ((g . a) |^ 0 ) by GROUP_1: 25;

      then

       A3: Q[ 0 ];

      for n be Nat holds Q[n] from NAT_1:sch 2( A3, A1);

      hence thesis;

    end;

    theorem :: GROUP_6:37

    (g . (a |^ i)) = ((g . a) |^ i)

    proof

      per cases ;

        suppose

         A1: i >= 0 ;



        hence (g . (a |^ i)) = (g . (a |^ |.i.|)) by ABSVALUE:def 1

        .= ((g . a) |^ |.i.|) by Th36

        .= ((g . a) |^ i) by A1, ABSVALUE:def 1;

      end;

        suppose

         A2: i < 0 ;



        hence (g . (a |^ i)) = (g . ((a |^ |.i.|) " )) by GROUP_1: 30

        .= ((g . (a |^ |.i.|)) " ) by Th32

        .= (((g . a) |^ |.i.|) " ) by Th36

        .= ((g . a) |^ i) by A2, GROUP_1: 30;

      end;

    end;

    theorem :: GROUP_6:38



     Th38: for G be non empty multMagma holds ( id the carrier of G) is multiplicative;

    theorem :: GROUP_6:39



     Th39: for G,H,I be unital non empty multMagma, h be multiplicative Function of G, H, h1 be multiplicative Function of H, I holds (h1 * h) is multiplicative

    proof

      let G,H,I be unital non empty multMagma, h be multiplicative Function of G, H, h1 be multiplicative Function of H, I;

      set f = (h1 * h);

      let a,b be Element of G;



      thus (f . (a * b)) = (h1 . (h . (a * b))) by FUNCT_2: 15

      .= (h1 . ((h . a) * (h . b))) by Def6

      .= ((h1 . (h . a)) * (h1 . (h . b))) by Def6

      .= ((f . a) * (h1 . (h . b))) by FUNCT_2: 15

      .= ((f . a) * (f . b)) by FUNCT_2: 15;

    end;

    registration

      let G,H,I be unital non empty multMagma, h be multiplicative Function of G, H, h1 be multiplicative Function of H, I;

      cluster (h1 * h) -> multiplicative;

      coherence by Th39;

    end

    definition

      let G,H be non empty multMagma;

      :: GROUP_6:def7

      func 1: (G,H) -> Function of G, H equals (G --> ( 1_ H));

      coherence ;

    end

    registration

      let G,H be unital non empty multMagma;

      cluster ( 1: (G,H)) -> multiplicative;

      coherence

      proof

        set f = ( 1: (G,H));

        let a,b be Element of G;

        for a be Element of G holds (f . a) = ( 1_ H) by FUNCOP_1: 7;

        hence (f . (a * b)) = ((f . a) * (f . b)) by Lm1;

      end;

    end

    theorem :: GROUP_6:40

    (h1 * ( 1: (G,H))) = ( 1: (G,I)) & (( 1: (H,I)) * h) = ( 1: (G,I))

    proof

      thus (h1 * ( 1: (G,H))) = ( 1: (G,I))

      proof

        let a be Element of G;



        thus ((h1 * ( 1: (G,H))) . a) = (h1 . (( 1: (G,H)) . a)) by FUNCT_2: 15

        .= (h1 . ( 1_ H)) by FUNCOP_1: 7

        .= ( 1_ I) by Th31

        .= (( 1: (G,I)) . a) by FUNCOP_1: 7;

      end;

      let a;



      thus ((( 1: (H,I)) * h) . a) = (( 1: (H,I)) . (h . a)) by FUNCT_2: 15

      .= ( 1_ I) by FUNCOP_1: 7

      .= (( 1: (G,I)) . a) by FUNCOP_1: 7;

    end;

    definition

      let G;

      let N be normal Subgroup of G;

      :: GROUP_6:def8

      func nat_hom N -> Function of G, (G ./. N) means

      : Def8: for a holds (it . a) = (a * N);

      existence

      proof

        defpred P[ object, object] means ex a st $1 = a & $2 = (a * N);



         A1: for x be object st x in the carrier of G holds ex y be object st P[x, y]

        proof

          let x be object;

          assume x in the carrier of G;

          then

          reconsider a = x as Element of G;

          reconsider y = (a * N) as set;

          take y;

          take a;

          thus thesis;

        end;

        consider f be Function such that

         A2: ( dom f) = the carrier of G and

         A3: for x be object st x in the carrier of G holds P[x, (f . x)] from CLASSES1:sch 1( A1);

        ( rng f) c= the carrier of (G ./. N)

        proof

          let x be object;

          assume x in ( rng f);

          then

          consider y be object such that

           A4: y in ( dom f) and

           A5: (f . y) = x by FUNCT_1:def 3;

          consider a such that y = a and

           A6: (f . y) = (a * N) by A2, A3, A4;

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

          then x in (G ./. N) by A5, A6, Th23;

          hence thesis;

        end;

        then

        reconsider f as Function of G, (G ./. N) by A2, FUNCT_2:def 1, RELSET_1: 4;

        take f;

        let a;

        ex b st a = b & (f . a) = (b * N) by A3;

        hence thesis;

      end;

      uniqueness

      proof

        let n1,n2 be Function of G, (G ./. N) such that

         A7: for a holds (n1 . a) = (a * N) and

         A8: for a holds (n2 . a) = (a * N);

        now

          let a;

          (n1 . a) = (a * N) by A7;

          hence (n1 . a) = (n2 . a) by A8;

        end;

        hence thesis;

      end;

    end

    registration

      let G;

      let N be normal Subgroup of G;

      cluster ( nat_hom N) -> multiplicative;

      coherence

      proof

        set f = ( nat_hom N);

        let a, b;



         A1: (f . a) = (a * N) by Def8;



         A2: (f . b) = (b * N) by Def8;



         A3: (f . (a * b)) = ((a * b) * N) by Def8;



        thus ((f . a) * (f . b)) = (( @ (f . a)) * ( @ (f . b))) by Def3

        .= (((a * N) * b) * N) by A1, A2, GROUP_3: 9

        .= ((a * (N * b)) * N) by GROUP_2: 106

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

        .= (a * ((b * N) * N)) by GROUP_2: 96

        .= (a * (b * N)) by Th5

        .= (f . (a * b)) by A3, GROUP_2: 105;

      end;

    end

    definition

      let G, H, g;

      :: GROUP_6:def9

      func Ker g -> strict Subgroup of G means

      : Def9: the carrier of it = { a : (g . a) = ( 1_ H) };

      existence

      proof

        defpred P[ set] means (g . $1) = ( 1_ H);

        reconsider A = { a : P[a] } as Subset of G from DOMAIN_1:sch 7;

         A1:

        now

          let a, b;

          assume a in A & b in A;

          then

           A2: (ex a1 st a1 = a & (g . a1) = ( 1_ H)) & ex b1 st b1 = b & (g . b1) = ( 1_ H);

          (g . (a * b)) = ((g . a) * (g . b)) by Def6

          .= ( 1_ H) by A2, GROUP_1:def 4;

          hence (a * b) in A;

        end;

         A3:

        now

          let a;

          assume a in A;

          then ex a1 st a1 = a & (g . a1) = ( 1_ H);



          then (g . (a " )) = (( 1_ H) " ) by Th32

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

          hence (a " ) in A;

        end;

        (g . ( 1_ G)) = ( 1_ H) by Th31;

        then ( 1_ G) in A;

        then

        consider B be strict Subgroup of G such that

         A4: the carrier of B = A by A1, A3, GROUP_2: 52;

        reconsider B as strict Subgroup of G;

        take B;

        thus thesis by A4;

      end;

      uniqueness by GROUP_2: 59;

    end

    registration

      let G, H, g;

      cluster ( Ker g) -> normal;

      coherence

      proof

        defpred P[ set] means (g . $1) = ( 1_ H);

        reconsider A = { a : P[a] } as Subset of G from DOMAIN_1:sch 7;

         A1:

        now

          let a, b;

          assume a in A & b in A;

          then

           A2: (ex a1 st a1 = a & (g . a1) = ( 1_ H)) & ex b1 st b1 = b & (g . b1) = ( 1_ H);

          (g . (a * b)) = ((g . a) * (g . b)) by Def6

          .= ( 1_ H) by A2, GROUP_1:def 4;

          hence (a * b) in A;

        end;

         A3:

        now

          let a;

          assume a in A;

          then ex a1 st a1 = a & (g . a1) = ( 1_ H);



          then (g . (a " )) = (( 1_ H) " ) by Th32

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

          hence (a " ) in A;

        end;

        (g . ( 1_ G)) = ( 1_ H) by Th31;

        then ( 1_ G) in A;

        then

        consider B be strict Subgroup of G such that

         A4: the carrier of B = A by A1, A3, GROUP_2: 52;

        now

          let a;

          now

            let b;

            assume b in (B |^ a);

            then

            consider c be Element of G such that

             A5: b = (c |^ a) and

             A6: c in B by GROUP_3: 58;

            c in A by A4, A6;

            then ex a1 st c = a1 & (g . a1) = ( 1_ H);



            then (g . b) = (( 1_ H) |^ (g . a)) by A5, Th33

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

            then b in A;

            hence b in B by A4;

          end;

          hence (B |^ a) is Subgroup of B by GROUP_2: 58;

        end;

        then B is normal Subgroup of G by GROUP_3: 122;

        hence thesis by A4, Def9;

      end;

    end

    theorem :: GROUP_6:41



     Th41: a in ( Ker h) iff (h . a) = ( 1_ H)

    proof

      thus a in ( Ker h) implies (h . a) = ( 1_ H)

      proof

        assume a in ( Ker h);

        then a in the carrier of ( Ker h);

        then a in { b : (h . b) = ( 1_ H) } by Def9;

        then ex b st a = b & (h . b) = ( 1_ H);

        hence thesis;

      end;

      assume (h . a) = ( 1_ H);

      then a in { b : (h . b) = ( 1_ H) };

      then a in the carrier of ( Ker h) by Def9;

      hence thesis;

    end;

    theorem :: GROUP_6:42

    for G,H be strict Group holds ( Ker ( 1: (G,H))) = G

    proof

      let G,H be strict Group;

      now

        let a be Element of G;

        (( 1: (G,H)) . a) = ( 1_ H) by FUNCOP_1: 7;

        hence a in ( Ker ( 1: (G,H))) by Th41;

      end;

      hence thesis by GROUP_2: 62;

    end;

    theorem :: GROUP_6:43



     Th43: for N be strict normal Subgroup of G holds ( Ker ( nat_hom N)) = N

    proof

      let N be strict normal Subgroup of G;

      let a;

      thus a in ( Ker ( nat_hom N)) implies a in N

      proof

        assume a in ( Ker ( nat_hom N));

        then

         A1: (( nat_hom N) . a) = ( 1_ (G ./. N)) by Th41;

        (( nat_hom N) . a) = (a * N) & ( 1_ (G ./. N)) = ( carr N) by Def8, Th24;

        hence thesis by A1, GROUP_2: 113;

      end;

      assume a in N;

      then

       A2: (a * N) = ( carr N) by GROUP_2: 113;

      (( nat_hom N) . a) = (a * N) & ( 1_ (G ./. N)) = ( carr N) by Def8, Th24;

      hence thesis by A2, Th41;

    end;

    definition

      let G, H, g;

      :: GROUP_6:def10

      func Image g -> strict Subgroup of H means

      : Def10: the carrier of it = (g .: the carrier of G);

      existence

      proof

        the carrier of G c= the carrier of G;

        then

        reconsider X = the carrier of G as Subset of G;

        set S = (g .: X);

         A1:

        now

          let c, d;

          assume that

           A2: c in S and

           A3: d in S;

          consider b such that b in X and

           A4: d = (g . b) by A3, FUNCT_2: 65;

          consider a such that a in X and

           A5: c = (g . a) by A2, FUNCT_2: 65;

          (c * d) = (g . (a * b)) by A5, A4, Def6;

          hence (c * d) in S by FUNCT_2: 35;

        end;

         A6:

        now

          let c;

          assume c in S;

          then

          consider a such that a in X and

           A7: c = (g . a) by FUNCT_2: 65;

          (g . (a " )) = (c " ) by A7, Th32;

          hence (c " ) in S by FUNCT_2: 35;

        end;

        ( dom g) = the carrier of G by FUNCT_2:def 1;

        then

        consider D be strict Subgroup of H such that

         A8: the carrier of D = S by A1, A6, GROUP_2: 52;

        take D;

        thus thesis by A8;

      end;

      uniqueness by GROUP_2: 59;

    end

    theorem :: GROUP_6:44



     Th44: ( rng g) = the carrier of ( Image g)

    proof

      the carrier of ( Image g) = (g .: the carrier of G) by Def10

      .= (g .: ( dom g)) by FUNCT_2:def 1

      .= ( rng g) by RELAT_1: 113;

      hence thesis;

    end;

    theorem :: GROUP_6:45



     Th45: for x be object holds x in ( Image g) iff ex a st x = (g . a)

    proof

      let x be object;

      thus x in ( Image g) implies ex a st x = (g . a)

      proof

        assume x in ( Image g);

        then x in the carrier of ( Image g);

        then x in (g .: the carrier of G) by Def10;

        then

        consider y be object such that y in ( dom g) and

         A1: y in the carrier of G and

         A2: (g . y) = x by FUNCT_1:def 6;

        reconsider y as Element of G by A1;

        take y;

        thus thesis by A2;

      end;

      given a such that

       A3: x = (g . a);

      the carrier of G = ( dom g) by FUNCT_2:def 1;

      then x in (g .: the carrier of G) by A3, FUNCT_1:def 6;

      then x in the carrier of ( Image g) by Def10;

      hence thesis;

    end;

    theorem :: GROUP_6:46

    ( Image g) = ( gr ( rng g))

    proof

      ( rng g) = the carrier of ( Image g) & the carrier of ( Image g) = ( carr ( Image g)) by Th44;

      hence thesis by GROUP_4: 31;

    end;

    theorem :: GROUP_6:47

    ( Image ( 1: (G,H))) = ( (1). H)

    proof

      set g = ( 1: (G,H));



       A1: the carrier of ( Image g) c= {( 1_ H)}

      proof

        let x be object;

        assume x in the carrier of ( Image g);

        then x in (g .: the carrier of G) by Def10;

        then

        consider y be object such that y in ( dom g) and

         A2: y in the carrier of G and

         A3: (g . y) = x by FUNCT_1:def 6;

        reconsider y as Element of G by A2;

        (g . y) = ( 1_ H) by FUNCOP_1: 7;

        hence thesis by A3, TARSKI:def 1;

      end;

      ( 1_ H) in ( Image g) by GROUP_2: 46;

      then ( 1_ H) in the carrier of ( Image g);

      then {( 1_ H)} c= the carrier of ( Image g) by ZFMISC_1: 31;

      then the carrier of ( Image g) = {( 1_ H)} by A1;

      hence thesis by GROUP_2:def 7;

    end;

    theorem :: GROUP_6:48



     Th48: for N be normal Subgroup of G holds ( Image ( nat_hom N)) = (G ./. N)

    proof

      let N be normal Subgroup of G;

      now

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

        consider a such that

         A1: S = (a * N) and S = (N * a) by Th13;

        (( nat_hom N) . a) = (a * N) by Def8;

        hence S in ( Image ( nat_hom N)) by A1, Th45;

      end;

      hence thesis by GROUP_2: 62;

    end;

    theorem :: GROUP_6:49



     Th49: h is Homomorphism of G, ( Image h)

    proof

      ( rng h) = the carrier of ( Image h) & ( dom h) = the carrier of G by Th44, FUNCT_2:def 1;

      then

      reconsider f9 = h as Function of G, ( Image h) by RELSET_1: 4;

      now

        let a, b;



        thus ((f9 . a) * (f9 . b)) = ((h . a) * (h . b)) by GROUP_2: 43

        .= (f9 . (a * b)) by Def6;

      end;

      hence thesis by Def6;

    end;

    theorem :: GROUP_6:50



     Th50: G is finite implies ( Image g) is finite

    proof

      assume G is finite;

      then (g .: the carrier of G) is finite;

      hence thesis by Def10;

    end;

    registration

      let G be finite Group;

      let H be Group;

      let g be Homomorphism of G, H;

      cluster ( Image g) -> finite;

      coherence by Th50;

    end



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

    theorem :: GROUP_6:51

    G is commutative Group implies ( Image g) is commutative

    proof

      assume

       A1: G is commutative Group;

      let h1,h2 be Element of ( Image g);

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

      h1 in ( Image g);

      then

      consider a such that

       A2: h1 = (g . a) by Th45;

      h2 in ( Image g);

      then

      consider b such that

       A3: h2 = (g . b) by Th45;



      thus (h1 * h2) = (c * d) by GROUP_2: 43

      .= (g . (a * b)) by A2, A3, Def6

      .= (g . (b * a)) by A1, Lm2

      .= (d * c) by A2, A3, Def6

      .= (h2 * h1) by GROUP_2: 43;

    end;

    theorem :: GROUP_6:52



     Th52: ( card ( Image g)) c= ( card G)

    proof

      ( card (g .: the carrier of G)) c= ( card the carrier of G) by CARD_1: 67;

      hence thesis by Def10;

    end;

    theorem :: GROUP_6:53

    for G be finite Group, H be Group, g be Homomorphism of G, H holds ( card ( Image g)) <= ( card G)

    proof

      let G be finite Group, H be Group, g be Homomorphism of G, H;

      ( Segm ( card ( Image g))) c= ( Segm ( card G)) by Th52;

      hence thesis by NAT_1: 39;

    end;

    theorem :: GROUP_6:54

    h is one-to-one & c in ( Image h) implies (h . ((h " ) . c)) = c

    proof

      reconsider h9 = h as Function of G, ( Image h) by Th49;

      assume that

       A1: h is one-to-one and

       A2: c in ( Image h);



       A3: ( rng h9) = the carrier of ( Image h) by Th44;

      c in the carrier of ( Image h) by A2;

      hence thesis by A1, A3, FUNCT_1: 35;

    end;

    theorem :: GROUP_6:55

    h is one-to-one implies (h " ) is Homomorphism of ( Image h), G

    proof

      assume

       A1: h is one-to-one;

      reconsider Imh = ( Image h) as Group;

      h is Function of G, Imh & ( rng h) = the carrier of Imh by Th44, Th49;

      then

      reconsider h9 = (h " ) as Function of Imh, G by A1, FUNCT_2: 25;

      now

        let a,b be Element of Imh;

        reconsider a9 = a, b9 = b as Element of H by GROUP_2: 42;

        a9 in Imh;

        then

        consider a1 be Element of G such that

         A2: (h . a1) = a9 by Th45;

        b9 in Imh;

        then

        consider b1 be Element of G such that

         A3: (h . b1) = b9 by Th45;



        thus (h9 . (a * b)) = (h9 . ((h . a1) * (h . b1))) by A2, A3, GROUP_2: 43

        .= (h9 . (h . (a1 * b1))) by Def6

        .= (a1 * b1) by A1, FUNCT_2: 26

        .= ((h9 . a) * b1) by A1, A2, FUNCT_2: 26

        .= ((h9 . a) * (h9 . b)) by A1, A3, FUNCT_2: 26;

      end;

      hence thesis by Def6;

    end;

    theorem :: GROUP_6:56



     Th56: h is one-to-one iff ( Ker h) = ( (1). G)

    proof

      thus h is one-to-one implies ( Ker h) = ( (1). G)

      proof

        assume

         A1: h is one-to-one;

        now

          let x be object;

          thus x in the carrier of ( Ker h) iff x = ( 1_ G)

          proof

            thus x in the carrier of ( Ker h) implies x = ( 1_ G)

            proof

              assume

               A2: x in the carrier of ( Ker h);

              then x in ( Ker h);

              then x in G by GROUP_2: 40;

              then

              reconsider a = x as Element of G;

              a in ( Ker h) by A2;



              then (h . a) = ( 1_ H) by Th41

              .= (h . ( 1_ G)) by Th31;

              hence thesis by A1, Th1;

            end;

            assume

             A3: x = ( 1_ G);

            then

            reconsider a = x as Element of G;

            (h . a) = ( 1_ H) by A3, Th31;

            then a in ( Ker h) by Th41;

            hence thesis;

          end;

        end;

        then the carrier of ( Ker h) = {( 1_ G)} by TARSKI:def 1;

        hence thesis by GROUP_2:def 7;

      end;

      assume ( Ker h) = ( (1). G);

      then

       A4: the carrier of ( Ker h) = {( 1_ G)} by GROUP_2:def 7;

      now

        let a, b;

        assume that

         A5: a <> b and

         A6: (h . a) = (h . b);

        ((h . a) * (h . (a " ))) = (h . (a * (a " ))) by Def6

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

        .= ( 1_ H) by Th31;

        then ( 1_ H) = (h . (b * (a " ))) by A6, Def6;

        then (b * (a " )) in ( Ker h) by Th41;

        then

         A7: (b * (a " )) in the carrier of ( Ker h);

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

        .= ((b * (a " )) * a) by A4, A7, TARSKI:def 1

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

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

        .= b by GROUP_1:def 4;

        hence contradiction by A5;

      end;

      then for a, b st (h . a) = (h . b) holds a = b;

      hence thesis by Th1;

    end;

    theorem :: GROUP_6:57



     Th57: for H be strict Group, h be Homomorphism of G, H holds h is onto iff ( Image h) = H

    proof

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

      thus h is onto implies ( Image h) = H

      proof

        assume ( rng h) = the carrier of H;

        then the carrier of ( Image h) = the carrier of H by Th44;

        hence thesis by GROUP_2: 61;

      end;

      assume

       A1: ( Image h) = H;

      the carrier of H c= ( rng h)

      proof

        let x be object;

        assume x in the carrier of H;

        then x in (h .: the carrier of G) by A1, Def10;

        then ex y be object st y in ( dom h) & y in the carrier of G & (h . y) = x by FUNCT_1:def 6;

        hence thesis by FUNCT_1:def 3;

      end;

      then ( rng h) = the carrier of H;

      hence thesis;

    end;

    theorem :: GROUP_6:58



     Th58: for G,H be non empty set, h be Function of G, H st h is onto holds for c be Element of H holds ex a be Element of G st (h . a) = c

    proof

      let G,H be non empty set, h be Function of G, H;

      assume

       A1: ( rng h) = H;

      let c be Element of H;

      ex a be object st a in G & (h . a) = c by A1, FUNCT_2: 11;

      hence ex a be Element of G st (h . a) = c;

    end;

    theorem :: GROUP_6:59



     Th59: for N be normal Subgroup of G holds ( nat_hom N) is onto

    proof

      let N be normal Subgroup of G;

      ( Image ( nat_hom N)) = (G ./. N) by Th48;

      hence thesis by Th57;

    end;

    theorem :: GROUP_6:60

    for G,H be set holds for h be Function of G, H holds h is bijective iff ( rng h) = H & h is one-to-one by FUNCT_2:def 3;

    theorem :: GROUP_6:61

    for G be set, H be non empty set holds for h be Function of G, H holds h is bijective implies ( dom h) = G & ( rng h) = H by FUNCT_2:def 1, FUNCT_2:def 3;

    theorem :: GROUP_6:62



     Th62: for H be Group, h be Homomorphism of G, H st h is bijective holds (h " ) is Homomorphism of H, G

    proof

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

      assume

       A1: h is bijective;

      then

       A2: h is one-to-one & ( rng h) = the carrier of H by FUNCT_2:def 3;

      then

      reconsider h1 = (h " ) as Function of H, G by FUNCT_2: 25;

      now

        let a,b be Element of H;

        set a1 = (h1 . a), b1 = (h1 . b);

        (h . a1) = a & (h . b1) = b by A2, FUNCT_1: 32;



        hence (h1 . (a * b)) = (h1 . (h . (a1 * b1))) by Def6

        .= ((h1 . a) * (h1 . b)) by A1, FUNCT_2: 26;

      end;

      hence thesis by Def6;

    end;

    theorem :: GROUP_6:63



     Th63: for G be set, H be non empty set holds for h be Function of G, H holds for g1 be Function of H, G holds h is bijective & g1 = (h " ) implies g1 is bijective

    proof

      let G be set, H be non empty set;

      let h be Function of G, H, g1 be Function of H, G;

      assume

       A1: h is bijective & g1 = (h " );

      then ( dom h) = G & ( rng g1) = ( dom h) by FUNCT_1: 33, FUNCT_2:def 1;

      hence thesis by A1, FUNCT_2:def 3;

    end;

    theorem :: GROUP_6:64



     Th64: for G be set, H,I be non empty set holds for h be Function of G, H holds for h1 be Function of H, I holds h is bijective & h1 is bijective implies (h1 * h) is bijective

    proof

      let G be set, H,I be non empty set;

      let h be Function of G, H, h1 be Function of H, I;

      assume that

       A1: h is bijective and

       A2: h1 is bijective;

      ( dom h1) = H & ( rng h) = H by A1, FUNCT_2:def 3, FUNCT_2:def 1;



      then ( rng (h1 * h)) = ( rng h1) by RELAT_1: 28

      .= I by A2, FUNCT_2:def 3;

      hence thesis by A1, A2, FUNCT_2:def 3;

    end;

    theorem :: GROUP_6:65



     Th65: for G be Group holds ( nat_hom ( (1). G)) is bijective

    proof

      let G be Group;

      set g = ( nat_hom ( (1). G));

      ( Ker g) = ( (1). G) by Th43;

      then g is one-to-one by Th56;

      hence thesis by Th59;

    end;

    definition

      let G, H;

      :: GROUP_6:def11

      pred G,H are_isomorphic means

      : Def11: ex h st h is bijective;

      reflexivity

      proof

        let G;

        reconsider i = ( id the carrier of G) as Homomorphism of G, G by Th38;

        i is bijective;

        hence thesis;

      end;

    end

    theorem :: GROUP_6:66



     Th66: for G,H be Group holds (G,H) are_isomorphic implies (H,G) are_isomorphic

    proof

      let G,H be Group;

      assume (G,H) are_isomorphic ;

      then

      consider h be Homomorphism of G, H such that

       A1: h is bijective;

      reconsider g = (h " ) as Homomorphism of H, G by A1, Th62;

      take g;

      thus thesis by A1, Th63;

    end;

    definition

      let G,H be Group;

      :: original: are_isomorphic

      redefine

      pred G,H are_isomorphic ;

      symmetry by Th66;

    end

    theorem :: GROUP_6:67

    (G,H) are_isomorphic & (H,I) are_isomorphic implies (G,I) are_isomorphic

    proof

      assume that

       A1: (G,H) are_isomorphic and

       A2: (H,I) are_isomorphic ;

      consider g such that

       A3: g is bijective by A1;

      consider h1 such that

       A4: h1 is bijective by A2;

      (h1 * g) is bijective by A3, A4, Th64;

      hence thesis;

    end;

    theorem :: GROUP_6:68

    h is one-to-one implies (G,( Image h)) are_isomorphic

    proof

      reconsider ih = h as Homomorphism of G, ( Image h) by Th49;

      assume

       A1: h is one-to-one;

      take ih;

      ih is onto by Th44;

      hence thesis by A1;

    end;

    theorem :: GROUP_6:69



     Th69: for G,H be strict Group holds G is trivial & H is trivial implies (G,H) are_isomorphic

    proof

      let G,H be strict Group;

      assume that

       A1: G is trivial and

       A2: H is trivial;

      take ( 1: (G,H));



       A3: H = ( (1). H) by A2, Th12;

      set h = ( 1: (G,H));



       A4: G = ( (1). G) by A1, Th12;

      now

        let a,b be Element of G;

        assume (h . a) = (h . b);

        a in the carrier of ( (1). G) by A4;

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

        then

         A5: a = ( 1_ G) by TARSKI:def 1;

        b in the carrier of ( (1). G) by A4;

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

        hence a = b by A5, TARSKI:def 1;

      end;

      then

       A6: h is one-to-one by Th1;

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



      then ( rng h) = {(h . ( 1_ G))} by A4, FUNCT_2: 48

      .= {( 1_ H)} by FUNCOP_1: 7

      .= the carrier of ( (1). H) by GROUP_2:def 7;

      then h is onto by A3;

      hence thesis by A6;

    end;

    theorem :: GROUP_6:70

    (( (1). G),( (1). H)) are_isomorphic by Th69;

    theorem :: GROUP_6:71

    for G be Group holds (G,(G ./. ( (1). G))) are_isomorphic

    proof

      let G be Group;

      ( nat_hom ( (1). G)) is bijective by Th65;

      hence thesis;

    end;

    theorem :: GROUP_6:72

    for G be Group holds (G ./. ( (Omega). G)) is trivial

    proof

      let G be Group;

      the carrier of (G ./. ( (Omega). G)) = {the carrier of G} by GROUP_2: 142;

      hence thesis;

    end;

    theorem :: GROUP_6:73



     Th73: for G,H be strict Group holds (G,H) are_isomorphic implies ( card G) = ( card H)

    proof

      let G,H be strict Group;

      assume

       A1: (G,H) are_isomorphic ;

      then

      consider h be Homomorphism of G, H such that

       A2: h is bijective;

      consider g1 be Homomorphism of H, G such that

       A3: g1 is bijective by A1, Def11;

      ( Image g1) = G by A3, Th57;

      then

       A4: ( card G) c= ( card H) by Th52;

      ( Image h) = H by A2, Th57;

      hence thesis by A4, Th52;

    end;

    theorem :: GROUP_6:74



     Th74: (G,H) are_isomorphic & G is finite implies H is finite

    proof

      assume that

       A1: (G,H) are_isomorphic and

       A2: G is finite;

      consider h such that

       A3: h is bijective by A1;

      ( rng h) = the carrier of H by A3, FUNCT_2:def 3;

      hence thesis by A2;

    end;

    theorem :: GROUP_6:75

    for G,H be strict Group holds (G,H) are_isomorphic implies ( card G) = ( card H) by Th73;

    theorem :: GROUP_6:76

    for G be strict trivial Group, H be strict Group holds (G,H) are_isomorphic implies H is trivial

    proof

      let G be strict trivial Group, H be strict Group;

      assume

       A1: (G,H) are_isomorphic ;

      then

      reconsider H as finite Group by Th74;

      ( card G) = 1 by Th11;

      then ( card H) = 1 by A1, Th73;

      hence thesis by Th11;

    end;

    theorem :: GROUP_6:77

    for H be Group st (G,H) are_isomorphic & G is commutative holds H is commutative

    proof

      let H be Group;

      assume that

       A1: (G,H) are_isomorphic and

       A2: G is commutative;

      consider h be Homomorphism of G, H such that

       A3: h is bijective by A1;

      now

        let c,d be Element of H;

        consider a such that

         A4: (h . a) = c by A3, Th58;

        consider b such that

         A5: (h . b) = d by A3, Th58;



        thus (c * d) = (h . (a * b)) by A4, A5, Def6

        .= (h . (b * a)) by A2

        .= (d * c) by A4, A5, Def6;

      end;

      hence thesis;

    end;



     Lm3: ((G ./. ( Ker g)),( Image g)) are_isomorphic & ex h be Homomorphism of (G ./. ( Ker g)), ( Image g) st h is bijective & g = (h * ( nat_hom ( Ker g)))

    proof

      set I = (G ./. ( Ker g));

      set J = ( Image g);

      defpred P[ set, set] means for a st $1 = (a * ( Ker g)) holds $2 = (g . a);



       A1: ( dom ( nat_hom ( Ker g))) = the carrier of G by FUNCT_2:def 1;



       A2: for S be Element of I holds ex T be Element of J st P[S, T]

      proof

        let S be Element of I;

        consider a such that

         A3: S = (a * ( Ker g)) and S = (( Ker g) * a) by Th13;

        (g . a) in J by Th45;

        then

        reconsider T = (g . a) as Element of J;

        take T;

        let b;

        assume S = (b * ( Ker g));

        then ((a " ) * b) in ( Ker g) by A3, GROUP_2: 114;



        then ( 1_ H) = (g . ((a " ) * b)) by Th41

        .= ((g . (a " )) * (g . b)) by Def6

        .= (((g . a) " ) * (g . b)) by Th32;

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

        hence thesis;

      end;

      consider f be Function of I, J such that

       A4: for S be Element of I holds P[S, (f . S)] from FUNCT_2:sch 3( A2);

      now

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

        consider a such that

         A5: S = (a * ( Ker g)) and S = (( Ker g) * a) by Th13;

        consider b such that

         A6: T = (b * ( Ker g)) and

         A7: T = (( Ker g) * b) by Th13;



         A8: (f . T) = (g . b) by A4, A6;

        (f . S) = (g . a) by A4, A5;



        then

         A9: ((f . S) * (f . T)) = ((g . a) * (g . b)) by A8, GROUP_2: 43

        .= (g . (a * b)) by Def6;

        (S * T) = ((a * ( Ker g)) * (( Ker g) * b)) by A5, A7, Def3

        .= (((a * ( Ker g)) * ( Ker g)) * b) by GROUP_3: 11

        .= ((a * ( Ker g)) * b) by Th5

        .= (a * (( Ker g) * b)) by GROUP_2: 106

        .= (a * (b * ( Ker g))) by GROUP_3: 117

        .= ((a * b) * ( Ker g)) by GROUP_2: 105;

        hence (f . (S * T)) = ((f . S) * (f . T)) by A4, A9;

      end;

      then

      reconsider f as Homomorphism of (G ./. ( Ker g)), J by Def6;



       A10: f is one-to-one

      proof

        let y1,y2 be object;

        assume y1 in ( dom f) & y2 in ( dom f);

        then

        reconsider S = y1, T = y2 as Element of I;

        assume

         A11: (f . y1) = (f . y2);

        consider a such that

         A12: S = (a * ( Ker g)) and S = (( Ker g) * a) by Th13;

        consider b such that

         A13: T = (b * ( Ker g)) and T = (( Ker g) * b) by Th13;



         A14: (f . T) = (g . b) by A4, A13;

        (f . S) = (g . a) by A4, A12;

        then (((g . b) " ) * (g . a)) = ( 1_ H) by A11, A14, GROUP_1:def 5;



        then ( 1_ H) = ((g . (b " )) * (g . a)) by Th32

        .= (g . ((b " ) * a)) by Def6;

        then ((b " ) * a) in ( Ker g) by Th41;

        hence thesis by A12, A13, GROUP_2: 114;

      end;



       A15: ( dom g) = the carrier of G by FUNCT_2:def 1;

       A16:

      now

        let x be object;

        thus x in ( dom g) implies x in ( dom ( nat_hom ( Ker g))) & (( nat_hom ( Ker g)) . x) in ( dom f)

        proof

          assume

           A17: x in ( dom g);

          hence x in ( dom ( nat_hom ( Ker g))) by A1;



           A18: ( dom f) = the carrier of I by FUNCT_2:def 1;

          (( nat_hom ( Ker g)) . x) in ( rng ( nat_hom ( Ker g))) by A1, A17, FUNCT_1:def 3;

          hence thesis by A18;

        end;

        assume that

         A19: x in ( dom ( nat_hom ( Ker g))) and (( nat_hom ( Ker g)) . x) in ( dom f);

        thus x in ( dom g) by A15, A19;

      end;

      the carrier of J c= ( rng f)

      proof

        let x be object;

        assume x in the carrier of J;

        then x in ( Image g);

        then

        consider a such that

         A20: x = (g . a) by Th45;

        reconsider S = (a * ( Ker g)) as Element of I by Th14;

        (f . S) = (g . a) & the carrier of I = ( dom f) by A4, FUNCT_2:def 1;

        hence thesis by A20, FUNCT_1:def 3;

      end;

      then

       A21: ( rng f) = the carrier of J;

      then f is bijective by A10, FUNCT_2:def 3;

      hence ((G ./. ( Ker g)),( Image g)) are_isomorphic ;

      take f;

      thus f is bijective by A21, A10, FUNCT_2:def 3;

      now

        let x be object;

        assume x in ( dom g);

        then

        reconsider a = x as Element of G;

        (( nat_hom ( Ker g)) . a) = (a * ( Ker g)) by Def8;

        hence (g . x) = (f . (( nat_hom ( Ker g)) . x)) by A4;

      end;

      hence thesis by A16, FUNCT_1: 10;

    end;

    theorem :: GROUP_6:78

    ((G ./. ( Ker g)),( Image g)) are_isomorphic by Lm3;

    ::$Notion-Name

    theorem :: GROUP_6:79

    ex h be Homomorphism of (G ./. ( Ker g)), ( Image g) st h is bijective & g = (h * ( nat_hom ( Ker g))) by Lm3;

    ::$Notion-Name

    theorem :: GROUP_6:80

    for M be strict normal Subgroup of G holds for J be strict normal Subgroup of (G ./. M) st J = (N ./. ((N,M) `*` )) & M is Subgroup of N holds (((G ./. M) ./. J),(G ./. N)) are_isomorphic

    proof

      let M be strict normal Subgroup of G;

      let J be strict normal Subgroup of (G ./. M);

      assume that

       A1: J = (N ./. ((N,M) `*` )) and

       A2: M is Subgroup of N;

      defpred P[ set, set] means for a st $1 = (a * M) holds $2 = (a * N);



       A3: for x be Element of (G ./. M) holds ex y be Element of (G ./. N) st P[x, y]

      proof

        let x be Element of (G ./. M);

        consider a such that

         A4: x = (a * M) and x = (M * a) by Th13;

        reconsider y = (a * N) as Element of (G ./. N) by Th14;

        take y;

        let b;

        assume x = (b * M);

        then ((a " ) * b) in M by A4, GROUP_2: 114;

        then ((a " ) * b) in N by A2, GROUP_2: 40;

        hence thesis by GROUP_2: 114;

      end;

      consider f be Function of (G ./. M), (G ./. N) such that

       A5: for x be Element of (G ./. M) holds P[x, (f . x)] from FUNCT_2:sch 3( A3);

      now

        let x,y be Element of (G ./. M);

        consider a such that

         A6: x = (a * M) and x = (M * a) by Th13;

        consider b such that

         A7: y = (b * M) and y = (M * b) by Th13;



         A8: (x * y) = (( @ x) * ( @ y)) by Def3

        .= (((a * M) * b) * M) by A6, A7, GROUP_3: 9

        .= ((a * (M * b)) * M) by GROUP_2: 106

        .= ((a * (b * M)) * M) by GROUP_3: 117

        .= (a * ((b * M) * M)) by GROUP_2: 96

        .= (a * (b * M)) by Th5

        .= ((a * b) * M) by GROUP_2: 105;



         A9: (f . y) = (b * N) by A5, A7;



         A10: (f . x) = (a * N) by A5, A6;

        ((f . x) * (f . y)) = (( @ (f . x)) * ( @ (f . y))) by Def3

        .= (((a * N) * b) * N) by A10, A9, GROUP_3: 9

        .= ((a * (N * b)) * N) by GROUP_2: 106

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

        .= (a * ((b * N) * N)) by GROUP_2: 96

        .= (a * (b * N)) by Th5

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

        hence (f . (x * y)) = ((f . x) * (f . y)) by A5, A8;

      end;

      then

      reconsider f as Homomorphism of (G ./. M), (G ./. N) by Def6;



       A11: ( Ker f) = J

      proof

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

        thus S in ( Ker f) implies S in J

        proof

          assume S in ( Ker f);



          then

           A12: (f . S) = ( 1_ (G ./. N)) by Th41

          .= ( carr N) by Th24;

          consider a such that

           A13: S = (a * M) and

           A14: S = (M * a) by Th13;

          (f . S) = (a * N) by A5, A13;

          then a in N by A12, GROUP_2: 113;

          then

          reconsider q = a as Element of N;

          ((N,M) `*` ) = M by A2, Def1;

          then S = (q * ((N,M) `*` )) & S = (((N,M) `*` ) * q) by A13, A14, Th2;

          hence thesis by A1, Th23;

        end;

        assume S in J;

        then

        consider a be Element of N such that

         A15: S = (a * ((N,M) `*` )) and S = (((N,M) `*` ) * a) by A1, Th23;

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

        ((N,M) `*` ) = M by A2, Def1;

        then S = (a9 * M) by A15, Th2;

        then

         A16: (f . S) = (a9 * N) by A5;

        a in N;



        then (f . S) = ( carr N) by A16, GROUP_2: 113

        .= ( 1_ (G ./. N)) by Th24;

        hence thesis by Th41;

      end;

      the carrier of (G ./. N) c= ( rng f)

      proof

        let x be object;

        assume x in the carrier of (G ./. N);

        then x in (G ./. N);

        then

        consider a such that

         A17: x = (a * N) and x = (N * a) by Th23;

        reconsider S = (a * M) as Element of (G ./. M) by Th14;

        (f . S) = (a * N) & ( dom f) = the carrier of (G ./. M) by A5, FUNCT_2:def 1;

        hence thesis by A17, FUNCT_1:def 3;

      end;

      then ( rng f) = the carrier of (G ./. N);

      then f is onto;

      then ( Image f) = (G ./. N) by Th57;

      hence thesis by A11, Lm3;

    end;

    ::$Notion-Name

    theorem :: GROUP_6:81

    for N be strict normal Subgroup of G holds (((B "\/" N) ./. (((B "\/" N),N) `*` )),(B ./. (B /\ N))) are_isomorphic

    proof

      let N be strict normal Subgroup of G;

      set f = ( nat_hom N);

      set g = (f | the carrier of B);

      set I = ((B "\/" N) ./. (((B "\/" N),N) `*` ));

      set J = (((B "\/" N),N) `*` );



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



       A2: ( dom g) = (( dom f) /\ the carrier of B) & ( dom f) = the carrier of G by FUNCT_2:def 1, RELAT_1: 61;

      then

       A3: ( dom g) = the carrier of B by A1, XBOOLE_1: 28;



       A4: N is Subgroup of (B "\/" N) by GROUP_4: 60;

      then

       A5: N = (((B "\/" N),N) `*` ) by Def1;



       A6: B is Subgroup of (B "\/" N) by GROUP_4: 60;

      ( rng g) c= the carrier of I

      proof

        let y be object;

        assume y in ( rng g);

        then

        consider x be object such that

         A7: x in ( dom g) and

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

        reconsider x as Element of B by A2, A1, A7, XBOOLE_1: 28;

        reconsider x9 = x as Element of G by GROUP_2: 42;

        reconsider x99 = x as Element of (B "\/" N) by A6, GROUP_2: 42;



         A9: (x99 * (((B "\/" N),N) `*` )) = (x9 * N) & (N * x9) = ((((B "\/" N),N) `*` ) * x99) by A5, Th2;



         A10: (g . x) = (f . x9) by A7, FUNCT_1: 47

        .= (x9 * N) by Def8;

        then (g . x) = (N * x9) by GROUP_3: 117;

        then y in I by A8, A10, A9, Th23;

        hence thesis;

      end;

      then

      reconsider g as Function of B, ((B "\/" N) ./. (((B "\/" N),N) `*` )) by A3, FUNCT_2:def 1, RELSET_1: 4;



       A11: I is Subgroup of (G ./. N) by A4, Th28;

      now

        let a,b be Element of B;

        reconsider a9 = a, b9 = b as Element of G by GROUP_2: 42;



         A12: (f . a9) = (g . a) & (f . b9) = (g . b) by FUNCT_1: 49;

        (a * b) = (a9 * b9) by GROUP_2: 43;



        hence (g . (a * b)) = (f . (a9 * b9)) by FUNCT_1: 49

        .= ((f . a9) * (f . b9)) by Def6

        .= ((g . a) * (g . b)) by A11, A12, GROUP_2: 43;

      end;

      then

      reconsider g as Homomorphism of B, ((B "\/" N) ./. (((B "\/" N),N) `*` )) by Def6;



       A13: ( Ker g) = (B /\ N)

      proof

        let b be Element of B;

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



         A14: (g . b) = (f . c) by FUNCT_1: 49

        .= (c * N) by Def8;

        thus b in ( Ker g) implies b in (B /\ N)

        proof

          assume b in ( Ker g);



          then (g . b) = ( 1_ I) by Th41

          .= ( carr J) by Th24

          .= ( carr N) by A4, Def1;

          then b in B & b in N by A14, GROUP_2: 113;

          hence thesis by GROUP_2: 82;

        end;

        assume b in (B /\ N);

        then b in N by GROUP_2: 82;



        then (c * N) = ( carr J) by A5, GROUP_2: 113

        .= ( 1_ I) by Th24;

        hence thesis by A14, Th41;

      end;

      the carrier of I c= ( rng g)

      proof

        let x be object;

        assume x in the carrier of I;

        then x in I;

        then

        consider b be Element of (B "\/" N) such that

         A15: x = (b * J) and x = (J * b) by Th23;

        (B * N) = (N * B) & b in (B "\/" N) by GROUP_5: 8;

        then

        consider a1, a2 such that

         A16: b = (a1 * a2) and

         A17: a1 in B and

         A18: a2 in N by GROUP_5: 5;



         A19: a1 in the carrier of B by A17;

        x = ((a1 * a2) * N) by A5, A15, A16, Th2

        .= (a1 * (a2 * N)) by GROUP_2: 105

        .= (a1 * N) by A18, GROUP_2: 113

        .= (f . a1) by Def8

        .= (g . a1) by A19, FUNCT_1: 49;

        hence thesis by A3, A19, FUNCT_1:def 3;

      end;

      then the carrier of I = ( rng g);

      then g is onto;

      then ( Image g) = ((B "\/" N) ./. (((B "\/" N),N) `*` )) by Th57;

      hence thesis by A13, Lm3;

    end;