grsolv_1.miz



    begin

    reserve i for Element of NAT ;

    definition

      let IT be Group;

      :: GRSOLV_1:def1

      attr IT is solvable means

      : Def1: ex F be FinSequence of ( Subgroups 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 Subgroup of IT st G1 = (F . i) & G2 = (F . (i + 1)) holds G2 is strict normal Subgroup of G1 & for N be normal Subgroup of G1 st N = G2 holds (G1 ./. N) is commutative;

    end

    registration

      cluster solvable strict for Group;

      existence

      proof

        set G = the Group;

        take H = ( (1). G);

        thus H is solvable

        proof

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

          proof

            let x be object;

            

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

            assume x in ( rng <*H*>);

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

            then x is strict Subgroup of H by GROUP_2: 54;

            hence thesis by GROUP_3:def 1;

          end;

          then

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

          take F;

          

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

          

           A3: for i st i in ( dom F) & (i + 1) in ( dom F) holds for G1,G2 be Subgroup of H st G1 = (F . i) & G2 = (F . (i + 1)) holds G2 is normal Subgroup of G1 & for N be normal Subgroup of G1 st N = G2 holds (G1 ./. N) is commutative

          proof

            let i;

            assume that

             A4: i in ( dom F) and

             A5: (i + 1) in ( dom F);

            let G1,G2 be Subgroup of H;

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

            

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

            then i = 1 by A4, TARSKI:def 1;

            hence thesis by A5, A6, TARSKI:def 1;

          end;

          (F . ( len F)) = H by A2, FINSEQ_1: 40

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

          hence thesis by A2, A3, FINSEQ_1: 40;

        end;

        thus thesis;

      end;

    end

    theorem :: GRSOLV_1:1

    

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

    proof

      let G be Group;

      let H,F1,F2 be strict 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;

    theorem :: GRSOLV_1:2

    for G be Group holds for F2 be Subgroup of G holds for F1 be normal Subgroup of F2 holds for a,b be Element of F2 holds ((a * F1) * (b * F1)) = ((a * b) * F1)

    proof

      let G be Group;

      let F2 be Subgroup of G;

      let F1 be normal Subgroup of F2;

      let a,b be Element of F2;

      

       A1: (( nat_hom F1) . a) = (a * F1) & (( nat_hom F1) . b) = (b * F1) by GROUP_6:def 8;

      

       A2: ( @ (( nat_hom F1) . a)) = (( nat_hom F1) . a) & ( @ (( nat_hom F1) . b)) = (( nat_hom F1) . b) by GROUP_6:def 5;

      

      thus ((a * b) * F1) = (( nat_hom F1) . (a * b)) by GROUP_6:def 8

      .= ((( nat_hom F1) . a) * (( nat_hom F1) . b)) by GROUP_6:def 6

      .= ((a * F1) * (b * F1)) by A1, A2, GROUP_6: 19;

    end;

    theorem :: GRSOLV_1:3

    for G be Group holds for H,F2 be Subgroup of G holds for F1 be normal Subgroup of F2 holds for G2 be Subgroup of G st G2 = (H /\ F2) holds for G1 be normal Subgroup of G2 st G1 = (H /\ F1) holds ex G3 be Subgroup of (F2 ./. F1) st ((G2 ./. G1),G3) are_isomorphic

    proof

      let G be Group;

      let H,F2 be Subgroup of G;

      let F1 be normal Subgroup of F2;

      reconsider G2 = (H /\ F2) as strict Subgroup of G;

      consider f be Function such that

       A1: f = (( nat_hom F1) | the carrier of H);

      reconsider f1 = ( nat_hom F1) as Function of the carrier of F2, the carrier of (F2 ./. F1);

      

       A2: the carrier of F2 = ( carr F2) & the carrier of H = ( carr H);

      ( dom f1) = the carrier of F2 by FUNCT_2:def 1;

      

      then

       A3: ( dom f) = (the carrier of F2 /\ the carrier of H) by A1, RELAT_1: 61

      .= ( carr (F2 /\ H)) by A2, GROUP_2: 81

      .= the carrier of (H /\ F2);

      ( rng (( nat_hom F1) | the carrier of H)) c= ( rng ( nat_hom F1)) by RELAT_1: 70;

      then

      reconsider f as Function of the carrier of (H /\ F2), the carrier of (F2 ./. F1) by A1, A3, FUNCT_2: 2;

      for a,b be Element of (H /\ F2) holds (f . (a * b)) = ((f . a) * (f . b))

      proof

        let a,b be Element of (H /\ F2);

        

         A4: the carrier of (H /\ F2) = (( carr H) /\ ( carr F2)) by GROUP_2:def 10;

        then

        reconsider a9 = a, b9 = b as Element of F2 by XBOOLE_0:def 4;

        b in ( carr H) by A4, XBOOLE_0:def 4;

        then

         A5: ((( nat_hom F1) | the carrier of H) . b) = (( nat_hom F1) . b) by FUNCT_1: 49;

        (a * b) in ( carr H) by A4, XBOOLE_0:def 4;

        then

         A6: ((( nat_hom F1) | the carrier of H) . (a * b)) = (( nat_hom F1) . (a * b)) by FUNCT_1: 49;

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

        then

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

        a in ( carr H) by A4, XBOOLE_0:def 4;

        then ((( nat_hom F1) | the carrier of H) . a) = (( nat_hom F1) . a) by FUNCT_1: 49;

        hence thesis by A1, A7, A5, A6, GROUP_6:def 6;

      end;

      then

      reconsider f as Homomorphism of (H /\ F2), (F2 ./. F1) by GROUP_6:def 6;

      

       A8: (the carrier of H /\ the carrier of F2) = ( carr (H /\ F2)) by A2, GROUP_2: 81

      .= the carrier of (H /\ F2);

      

       A9: ( Ker f) = (H /\ F1)

      proof

        reconsider L = ( Ker f) as Subgroup of G by GROUP_2: 56;

        for g be Element of G holds g in L iff g in (H /\ F1)

        proof

          let x be Element of G;

          thus x in L implies x in (H /\ F1)

          proof

            assume

             A10: x in L;

            then x in ( carr ( Ker f)) by STRUCT_0:def 5;

            then

            reconsider a = x as Element of (H /\ F2);

            

             A11: the carrier of (H /\ F2) = (( carr H) /\ ( carr F2)) by GROUP_2:def 10;

            then

            reconsider a9 = a as Element of F2 by XBOOLE_0:def 4;

            

             A12: a in ( carr H) by A11, XBOOLE_0:def 4;

            then

             A13: a in H by STRUCT_0:def 5;

            ((( nat_hom F1) | the carrier of H) . a) = (( nat_hom F1) . a) by A12, FUNCT_1: 49;

            then

             A14: (f . a) = (a9 * F1) by A1, GROUP_6:def 8;

            (f . a) = ( 1_ (F2 ./. F1)) by A10, GROUP_6: 41

            .= ( carr F1) by GROUP_6: 24;

            then a9 in F1 by A14, GROUP_2: 113;

            hence thesis by A13, GROUP_2: 82;

          end;

          thus x in (H /\ F1) implies x in L

          proof

            reconsider F19 = F1 as Subgroup of G;

            

             A15: (the carrier of H /\ the carrier of F1) = (( carr H) /\ ( carr F19))

            .= the carrier of (H /\ F1) by GROUP_2:def 10;

            assume x in (H /\ F1);

            then

             A16: x in ( carr (H /\ F1)) by STRUCT_0:def 5;

            the carrier of F1 c= the carrier of F2 by GROUP_2:def 5;

            then the carrier of (H /\ F1) c= the carrier of (H /\ F2) by A8, A15, XBOOLE_1: 26;

            then

            reconsider a = x as Element of (H /\ F2) by A16;

            x in the carrier of F1 by A16, A15, XBOOLE_0:def 4;

            then

             A17: a in F1 by STRUCT_0:def 5;

            

             A18: the carrier of (H /\ F2) = (( carr H) /\ ( carr F2)) by GROUP_2:def 10;

            then

            reconsider a9 = a as Element of F2 by XBOOLE_0:def 4;

            a in ( carr H) by A18, XBOOLE_0:def 4;

            then ((( nat_hom F1) | the carrier of H) . a) = (( nat_hom F1) . a) by FUNCT_1: 49;

            

            then (f . a) = (a9 * F1) by A1, GROUP_6:def 8

            .= ( carr F1) by A17, GROUP_2: 113

            .= ( 1_ (F2 ./. F1)) by GROUP_6: 24;

            hence thesis by GROUP_6: 41;

          end;

        end;

        hence thesis by GROUP_2:def 6;

      end;

      reconsider G1 = ( Ker f) as normal Subgroup of G2;

      ((G2 ./. G1),( Image f)) are_isomorphic by GROUP_6: 78;

      hence thesis by A9;

    end;

    theorem :: GRSOLV_1:4

    

     Th4: for G be Group holds for H,F2 be Subgroup of G holds for F1 be normal Subgroup of F2 holds for G2 be Subgroup of G st G2 = (F2 /\ H) holds for G1 be normal Subgroup of G2 st G1 = (F1 /\ H) holds ex G3 be Subgroup of (F2 ./. F1) st ((G2 ./. G1),G3) are_isomorphic

    proof

      let G be Group;

      let H,F2 be Subgroup of G;

      let F1 be normal Subgroup of F2;

      reconsider G2 = (F2 /\ H) as strict Subgroup of G;

      consider f be Function such that

       A1: f = (( nat_hom F1) | the carrier of H);

      reconsider f1 = ( nat_hom F1) as Function of the carrier of F2, the carrier of (F2 ./. F1);

      

       A2: the carrier of F2 = ( carr F2) & the carrier of H = ( carr H);

      ( dom f1) = the carrier of F2 by FUNCT_2:def 1;

      

      then

       A3: ( dom f) = (the carrier of F2 /\ the carrier of H) by A1, RELAT_1: 61

      .= the carrier of (F2 /\ H) by A2, GROUP_2:def 10;

      ( rng (( nat_hom F1) | the carrier of H)) c= ( rng ( nat_hom F1)) by RELAT_1: 70;

      then

      reconsider f as Function of the carrier of (F2 /\ H), the carrier of (F2 ./. F1) by A1, A3, FUNCT_2: 2;

      for a,b be Element of (F2 /\ H) holds (f . (a * b)) = ((f . a) * (f . b))

      proof

        let a,b be Element of (F2 /\ H);

        

         A4: the carrier of (F2 /\ H) = (( carr H) /\ ( carr F2)) by GROUP_2:def 10;

        then

        reconsider a9 = a, b9 = b as Element of F2 by XBOOLE_0:def 4;

        b in ( carr H) by A4, XBOOLE_0:def 4;

        then

         A5: ((( nat_hom F1) | the carrier of H) . b) = (( nat_hom F1) . b) by FUNCT_1: 49;

        (a * b) in ( carr H) by A4, XBOOLE_0:def 4;

        then

         A6: ((( nat_hom F1) | the carrier of H) . (a * b)) = (( nat_hom F1) . (a * b)) by FUNCT_1: 49;

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

        then

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

        a in ( carr H) by A4, XBOOLE_0:def 4;

        then ((( nat_hom F1) | the carrier of H) . a) = (( nat_hom F1) . a) by FUNCT_1: 49;

        hence thesis by A1, A7, A5, A6, GROUP_6:def 6;

      end;

      then

      reconsider f as Homomorphism of (F2 /\ H), (F2 ./. F1) by GROUP_6:def 6;

      

       A8: (the carrier of H /\ the carrier of F2) = ( carr (F2 /\ H)) by A2, GROUP_2: 81

      .= the carrier of (F2 /\ H);

      

       A9: ( Ker f) = (F1 /\ H)

      proof

        reconsider L = ( Ker f) as Subgroup of G by GROUP_2: 56;

        for g be Element of G holds g in L iff g in (F1 /\ H)

        proof

          let x be Element of G;

          thus x in L implies x in (F1 /\ H)

          proof

            assume

             A10: x in L;

            then x in ( carr ( Ker f)) by STRUCT_0:def 5;

            then

            reconsider a = x as Element of (F2 /\ H);

            

             A11: the carrier of (F2 /\ H) = (( carr H) /\ ( carr F2)) by GROUP_2:def 10;

            then

            reconsider a9 = a as Element of F2 by XBOOLE_0:def 4;

            

             A12: a in ( carr H) by A11, XBOOLE_0:def 4;

            then

             A13: a in H by STRUCT_0:def 5;

            ((( nat_hom F1) | the carrier of H) . a) = (( nat_hom F1) . a) by A12, FUNCT_1: 49;

            then

             A14: (f . a) = (a9 * F1) by A1, GROUP_6:def 8;

            (f . a) = ( 1_ (F2 ./. F1)) by A10, GROUP_6: 41

            .= ( carr F1) by GROUP_6: 24;

            then a9 in F1 by A14, GROUP_2: 113;

            hence thesis by A13, GROUP_2: 82;

          end;

          thus x in (F1 /\ H) implies x in L

          proof

            reconsider F19 = F1 as Subgroup of G;

            

             A15: (the carrier of H /\ the carrier of F1) = (( carr H) /\ ( carr F19))

            .= the carrier of (F1 /\ H) by GROUP_2:def 10;

            assume x in (F1 /\ H);

            then

             A16: x in ( carr (F1 /\ H)) by STRUCT_0:def 5;

            the carrier of F1 c= the carrier of F2 by GROUP_2:def 5;

            then the carrier of (F1 /\ H) c= the carrier of (F2 /\ H) by A8, A15, XBOOLE_1: 26;

            then

            reconsider a = x as Element of (F2 /\ H) by A16;

            x in the carrier of F1 by A16, A15, XBOOLE_0:def 4;

            then

             A17: a in F1 by STRUCT_0:def 5;

            

             A18: the carrier of (F2 /\ H) = (( carr H) /\ ( carr F2)) by GROUP_2:def 10;

            then

            reconsider a9 = a as Element of F2 by XBOOLE_0:def 4;

            a in ( carr H) by A18, XBOOLE_0:def 4;

            then ((( nat_hom F1) | the carrier of H) . a) = (( nat_hom F1) . a) by FUNCT_1: 49;

            

            then (f . a) = (a9 * F1) by A1, GROUP_6:def 8

            .= ( carr F1) by A17, GROUP_2: 113

            .= ( 1_ (F2 ./. F1)) by GROUP_6: 24;

            hence thesis by GROUP_6: 41;

          end;

        end;

        hence thesis by GROUP_2:def 6;

      end;

      reconsider G1 = ( Ker f) as normal Subgroup of G2;

      ((G2 ./. G1),( Image f)) are_isomorphic by GROUP_6: 78;

      hence thesis by A9;

    end;

    theorem :: GRSOLV_1:5

    for G be strict solvable Group, H be strict Subgroup of G holds H is solvable

    proof

      let G be strict solvable Group;

      let H be strict Subgroup of G;

      consider F be FinSequence of ( Subgroups 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 Subgroup of G st G1 = (F . i) & G2 = (F . (i + 1)) holds G2 is strict normal Subgroup of G1 & for N be normal Subgroup of G1 st N = G2 holds (G1 ./. N) is commutative by Def1;

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

      

       A5: for k be Nat st k in ( Seg ( len F)) holds ex x be Element of ( Subgroups 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 ( Subgroups G) by FINSEQ_2: 11;

        then

        reconsider I = (F . k) as strict Subgroup of G by GROUP_3:def 1;

        reconsider x = (I /\ H) as strict Subgroup of H by GROUP_2: 88;

        reconsider y = x as Element of ( Subgroups H) by GROUP_3:def 1;

        take y;

        take I;

        thus thesis;

      end;

      consider R be FinSequence of ( Subgroups H) such that

       A6: ( 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( A5);

      

       A7: for i st i in ( dom R) & (i + 1) in ( dom R) holds for H1,H2 be strict Subgroup of H 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 that

         A8: i in ( dom R) and

         A9: (i + 1) in ( dom R);

        consider J be strict Subgroup of G such that

         A10: J = (F . (i + 1)) and

         A11: (R . (i + 1)) = (J /\ H) by A6, A9;

        consider I be strict Subgroup of G such that

         A12: I = (F . i) and

         A13: (R . i) = (I /\ H) by A6, A8;

        let H1,H2 be strict Subgroup of H;

        assume that

         A14: H1 = (R . i) and

         A15: H2 = (R . (i + 1));

        

         A16: i in ( dom F) & (i + 1) in ( dom F) by A6, A8, A9, FINSEQ_1:def 3;

        then

        reconsider J1 = J as strict normal Subgroup of I by A4, A12, A10;

        

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

        proof

          let N be strict normal Subgroup of H1;

          assume N = H2;

          then

          consider G3 be Subgroup of (I ./. J1) such that

           A18: ((H1 ./. N),G3) are_isomorphic by A14, A15, A13, A11, Th4;

          consider h be Homomorphism of (H1 ./. N), G3 such that

           A19: h is bijective by A18, GROUP_6:def 11;

          

           A20: h is one-to-one by A19, FUNCT_2:def 4;

          

           A21: (I ./. J1) is commutative by A4, A12, A10, A16;

          now

            let a,b be Element of (H1 ./. N);

            consider a9 be Element of G3 such that

             A22: a9 = (h . a);

            consider b9 be Element of G3 such that

             A23: b9 = (h . b);

            the multF of G3 is commutative by A21, GROUP_3: 2;

            then

             A24: (a9 * b9) = (b9 * a9) by BINOP_1:def 2;

            

            thus (the multF of (H1 ./. N) . (a,b)) = ((h " ) . (h . (a * b))) by A20, FUNCT_2: 26

            .= ((h " ) . ((h . b) * (h . a))) by A22, A23, A24, GROUP_6:def 6

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

            .= (the multF of (H1 ./. N) . (b,a)) by A20, FUNCT_2: 26;

          end;

          then the multF of (H1 ./. N) is commutative by BINOP_1:def 2;

          hence thesis by GROUP_3: 2;

        end;

        H2 = (J1 /\ H) by A15, A11;

        hence thesis by A14, A13, A17, Th1;

      end;

      

       A25: ( len R) = ( len F) by A6, FINSEQ_1:def 3;

      

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

      

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

      proof

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

        then 1 in ( Seg ( len F)) by A25, FINSEQ_1: 1;

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

        hence thesis by A2, GROUP_2: 86;

      end;

      take R;

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

      proof

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

        

        hence (R . ( len R)) = ( (1). G) by A3, A25, GROUP_2: 85

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

      end;

      hence thesis by A1, A6, A27, A7, FINSEQ_1:def 3;

    end;

    theorem :: GRSOLV_1:6

    for G be Group st ex F be FinSequence of ( Subgroups 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 Subgroup of G st G1 = (F . i) & G2 = (F . (i + 1)) holds G2 is strict normal Subgroup of G1 & for N be normal Subgroup of G1 st N = G2 holds (G1 ./. N) is cyclic Group holds G is solvable

    proof

      let G be Group;

      given F be FinSequence of ( Subgroups 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 Subgroup of G st G1 = (F . i) & G2 = (F . (i + 1)) holds G2 is strict normal Subgroup of G1 & for N be normal Subgroup of G1 st N = G2 holds (G1 ./. N) is cyclic Group);

      take F;

      thus thesis by A1;

    end;

    theorem :: GRSOLV_1:7

    for G be strict commutative Group holds G is solvable

    proof

      let G be strict commutative Group;

      ( (Omega). G) in ( Subgroups G) & ( (1). G) in ( Subgroups G) by GROUP_3:def 1;

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

      then

      consider F be FinSequence of ( Subgroups G) such that

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

      

       A2: (F . 1) = ( (Omega). G) by A1, FINSEQ_1: 44;

      

       A3: ( len F) = 2 by A1, FINSEQ_1: 44;

      

       A4: (F . 2) = ( (1). G) by A1, FINSEQ_1: 44;

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

      proof

        let i;

        assume that

         A5: i in ( dom F) and

         A6: (i + 1) in ( dom F);

        now

          let G1,G2 be strict Subgroup of G;

          assume

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

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

          then

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

          

           A9: (i + 1) in {1, 2} by A3, A6, FINSEQ_1: 2, FINSEQ_1:def 3;

          for N be normal Subgroup of G1 st N = G2 holds (G1 ./. N) is commutative by A2, A4, A7, A9, A8, GROUP_6: 71, GROUP_6: 77, TARSKI:def 2;

          hence G2 is strict normal Subgroup of G1 & for N be normal Subgroup of G1 st N = G2 holds (G1 ./. N) is commutative by A1, A2, A7, A9, A8, FINSEQ_1: 44, TARSKI:def 2;

        end;

        hence thesis;

      end;

      hence thesis by A3, A2, A4;

    end;

    definition

      let G,H be Group;

      let g be Homomorphism of G, H;

      let A be Subgroup of G;

      :: GRSOLV_1:def2

      func g | A -> Homomorphism of A, H equals (g | the carrier of A);

      coherence

      proof

        

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

        then

        reconsider f = (g | the carrier of A) as Function of the carrier of A, the carrier of H by FUNCT_2: 32;

        now

          

           A2: for a,b be Element of G holds (the multF of H . ((g . a),(g . b))) = (g . (the multF of G . (a,b)))

          proof

            let a,b be Element of G;

            

            thus (the multF of H . ((g . a),(g . b))) = ((g . a) * (g . b))

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

            .= (g . (the multF of G . (a,b)));

          end;

          let a,b be Element of A;

          

           A3: (f . a) = (g . a) & (f . b) = (g . b) by FUNCT_1: 49;

          

           A4: (the multF of G . (a,b)) = (a * b)

          proof

            reconsider b9 = b as Element of G by A1;

            reconsider a9 = a as Element of G by A1;

            

            thus (the multF of G . (a,b)) = (a9 * b9)

            .= (a * b) by GROUP_2: 43;

          end;

          a is Element of G & b is Element of G by A1;

          

          hence ((f . a) * (f . b)) = (g . (the multF of G . (a,b))) by A3, A2

          .= (f . (a * b)) by A4, FUNCT_1: 49;

        end;

        hence thesis by GROUP_6:def 6;

      end;

    end

    definition

      let G,H be Group;

      let g be Homomorphism of G, H;

      let A be Subgroup of G;

      :: GRSOLV_1:def3

      func g .: A -> strict Subgroup of H equals ( Image (g | A));

      coherence ;

    end

    theorem :: GRSOLV_1:8

    

     Th8: for G,H be Group, g be Homomorphism of G, H holds for A be Subgroup of G holds the carrier of (g .: A) = (g .: the carrier of A)

    proof

      let G,H be Group;

      let g be Homomorphism of G, H;

      let A be Subgroup of G;

      

      thus the carrier of (g .: A) = ( rng (g | A)) by GROUP_6: 44

      .= (g .: the carrier of A) by RELAT_1: 115;

    end;

    theorem :: GRSOLV_1:9

    

     Th9: for G,H be Group, h be Homomorphism of G, H holds for A be strict Subgroup of G holds ( Image (h | A)) is strict Subgroup of ( Image h)

    proof

      let G,H be Group;

      let h be Homomorphism of G, H;

      let A be strict Subgroup of G;

      

       A1: the carrier of A c= the carrier of G & (h .: the carrier of G) = the carrier of ( Image h) by GROUP_2:def 5, GROUP_6:def 10;

      the carrier of ( Image (h | A)) = ( rng (h | A)) by GROUP_6: 44

      .= (h .: the carrier of A) by RELAT_1: 115;

      hence thesis by A1, GROUP_2: 57, RELAT_1: 123;

    end;

    theorem :: GRSOLV_1:10

    for G,H be Group, h be Homomorphism of G, H holds for A be strict Subgroup of G holds (h .: A) is strict Subgroup of ( Image h) by Th9;

    theorem :: GRSOLV_1:11

    

     Th11: for G,H be Group, h be Homomorphism of G, H holds (h .: ( (1). G)) = ( (1). H) & (h .: ( (Omega). G)) = ( (Omega). ( Image h))

    proof

      let G,H be Group;

      let h be Homomorphism of G, H;

      

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

      

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

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

      

      then the carrier of (h .: ( (1). G)) = ( Im (h,( 1_ G))) by Th8

      .= {(h . ( 1_ G))} by A1, FUNCT_1: 59

      .= the carrier of ( (1). H) by A2, GROUP_6: 31;

      hence (h .: ( (1). G)) = ( (1). H) by GROUP_2: 59;

      the carrier of (h .: ( (Omega). G)) = (h .: the carrier of G) by Th8

      .= the carrier of ( (Omega). ( Image h)) by GROUP_6:def 10;

      hence thesis by GROUP_2: 59;

    end;

    theorem :: GRSOLV_1:12

    

     Th12: for G,H be Group, h be Homomorphism of G, H holds for A,B be Subgroup of G holds A is Subgroup of B implies (h .: A) is Subgroup of (h .: B)

    proof

      let G,H be Group;

      let h be Homomorphism of G, H;

      let A,B be Subgroup of G;

      assume A is Subgroup of B;

      then the carrier of A c= the carrier of B by GROUP_2:def 5;

      then

       A1: (h .: the carrier of A) c= (h .: the carrier of B) by RELAT_1: 123;

      the carrier of (h .: B) = (h .: the carrier of B) by Th8;

      then the carrier of (h .: A) c= the carrier of (h .: B) by A1, Th8;

      hence thesis by GROUP_2: 57;

    end;

    theorem :: GRSOLV_1:13

    

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

    proof

      let G,H be strict Group;

      let h be Homomorphism of G, H;

      let A be strict Subgroup of G;

      let a be Element of G;

      now

        let x be object;

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

        then

        consider y be object such that

         A1: y in the carrier of G and

         A2: y in (a * A) and

         A3: x = (h . y) by FUNCT_2: 64;

        reconsider y as Element of G by A1;

        consider b be Element of G such that

         A4: y = (a * b) and

         A5: b in A by A2, GROUP_2: 103;

        b in the carrier of A by A5, STRUCT_0:def 5;

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

        then (h . b) in the carrier of (h .: A) by Th8;

        then

         A6: (h . b) in (h .: A) by STRUCT_0:def 5;

        x = ((h . a) * (h . b)) by A3, A4, GROUP_6:def 6;

        hence x in ((h . a) * (h .: A)) by A6, GROUP_2: 103;

      end;

      then

       A7: (h .: (a * A)) c= ((h . a) * (h .: A));

      now

        let x be object;

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

        then

        consider b1 be Element of H such that

         A8: x = ((h . a) * b1) and

         A9: b1 in (h .: A) by GROUP_2: 103;

        consider b be Element of A such that

         A10: b1 = ((h | A) . b) by A9, GROUP_6: 45;

        

         A11: b in A by STRUCT_0:def 5;

        reconsider b as Element of G by GROUP_2: 42;

        b1 = (h . b) by A10, FUNCT_1: 49;

        then

         A12: x = (h . (a * b)) by A8, GROUP_6:def 6;

        (a * b) in (a * A) by A11, GROUP_2: 103;

        hence x in (h .: (a * A)) by A12, FUNCT_2: 35;

      end;

      then ((h . a) * (h .: A)) c= (h .: (a * A));

      hence ((h . a) * (h .: A)) = (h .: (a * A)) by A7, XBOOLE_0:def 10;

      now

        let x be object;

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

        then

        consider y be object such that

         A13: y in the carrier of G and

         A14: y in (A * a) and

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

        reconsider y as Element of G by A13;

        consider b be Element of G such that

         A16: y = (b * a) and

         A17: b in A by A14, GROUP_2: 104;

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

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

        then (h . b) in the carrier of (h .: A) by Th8;

        then

         A18: (h . b) in (h .: A) by STRUCT_0:def 5;

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

        hence x in ((h .: A) * (h . a)) by A18, GROUP_2: 104;

      end;

      then

       A19: (h .: (A * a)) c= ((h .: A) * (h . a));

      now

        let x be object;

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

        then

        consider b1 be Element of H such that

         A20: x = (b1 * (h . a)) and

         A21: b1 in (h .: A) by GROUP_2: 104;

        consider b be Element of A such that

         A22: b1 = ((h | A) . b) by A21, GROUP_6: 45;

        

         A23: b in A by STRUCT_0:def 5;

        reconsider b as Element of G by GROUP_2: 42;

        b1 = (h . b) by A22, FUNCT_1: 49;

        then

         A24: x = (h . (b * a)) by A20, GROUP_6:def 6;

        (b * a) in (A * a) by A23, GROUP_2: 104;

        hence x in (h .: (A * a)) by A24, FUNCT_2: 35;

      end;

      then ((h .: A) * (h . a)) c= (h .: (A * a));

      hence thesis by A19, XBOOLE_0:def 10;

    end;

    theorem :: GRSOLV_1:14

    

     Th14: for G,H be strict Group, h be Homomorphism of G, H holds for A,B be Subset of G holds ((h .: A) * (h .: B)) = (h .: (A * B))

    proof

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

      let A,B be Subset of G;

      now

        let z be object;

        assume z in ((h .: A) * (h .: B));

        then

        consider z1,z2 be Element of H such that

         A1: z = (z1 * z2) and

         A2: z1 in (h .: A) and

         A3: z2 in (h .: B);

        consider z4 be object such that

         A4: z4 in the carrier of G and

         A5: z4 in B and

         A6: z2 = (h . z4) by A3, FUNCT_2: 64;

        reconsider z4 as Element of G by A4;

        consider z3 be object such that

         A7: z3 in the carrier of G and

         A8: z3 in A and

         A9: z1 = (h . z3) by A2, FUNCT_2: 64;

        reconsider z3 as Element of G by A7;

        

         A10: (z3 * z4) in (A * B) by A8, A5;

        z = (h . (z3 * z4)) by A1, A9, A6, GROUP_6:def 6;

        hence z in (h .: (A * B)) by A10, FUNCT_2: 35;

      end;

      then

       A11: ((h .: A) * (h .: B)) c= (h .: (A * B));

      now

        let z be object;

        assume z in (h .: (A * B));

        then

        consider x be object such that

         A12: x in the carrier of G and

         A13: x in (A * B) and

         A14: z = (h . x) by FUNCT_2: 64;

        reconsider x as Element of G by A12;

        consider z1,z2 be Element of G such that

         A15: x = (z1 * z2) and

         A16: z1 in A & z2 in B by A13;

        

         A17: (h . z1) in (h .: A) & (h . z2) in (h .: B) by A16, FUNCT_2: 35;

        z = ((h . z1) * (h . z2)) by A14, A15, GROUP_6:def 6;

        hence z in ((h .: A) * (h .: B)) by A17;

      end;

      then (h .: (A * B)) c= ((h .: A) * (h .: B));

      hence thesis by A11, XBOOLE_0:def 10;

    end;

    theorem :: GRSOLV_1:15

    

     Th15: for G,H be strict Group, h be Homomorphism of G, H holds for A,B be strict Subgroup of G holds A is strict normal Subgroup of B implies (h .: A) is strict normal Subgroup of (h .: B)

    proof

      let G,H be strict Group;

      let h be Homomorphism of G, H;

      let A,B be strict Subgroup of G;

      assume A is strict normal Subgroup of B;

      then

      reconsider A1 = A as strict normal Subgroup of B;

      reconsider C = (h .: A1) as strict Subgroup of (h .: B) by Th12;

      for b2 be Element of (h .: B) holds (b2 * C) c= (C * b2)

      proof

        let b2 be Element of (h .: B);

        

         A1: b2 in (h .: B) by STRUCT_0:def 5;

        now

          consider b1 be Element of B such that

           A2: b2 = ((h | B) . b1) by A1, GROUP_6: 45;

          reconsider b1 as Element of G by GROUP_2: 42;

          

           A3: b2 = (h . b1) by A2, FUNCT_1: 49;

          reconsider b = b1 as Element of B;

          let x be object;

          assume x in (b2 * C);

          then

          consider g be Element of (h .: B) such that

           A4: x = (b2 * g) and

           A5: g in C by GROUP_2: 103;

          consider g1 be Element of A1 such that

           A6: g = ((h | A1) . g1) by A5, GROUP_6: 45;

          reconsider g1 as Element of G by GROUP_2: 42;

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

          

          then

           A7: x = ((h . b1) * (h . g1)) by A3, A4, GROUP_2: 43

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

          g1 in A1 by STRUCT_0:def 5;

          then

           A8: (b1 * g1) in (b1 * A1) by GROUP_2: 103;

          

           A9: (h .: (A1 * b1)) = ((h .: A1) * (h . b1)) by Th13;

          (b1 * A1) = (b * A1) by GROUP_6: 2

          .= (A1 * b) by GROUP_3: 117

          .= (A1 * b1) by GROUP_6: 2;

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

          hence x in (C * b2) by A3, A9, GROUP_6: 2;

        end;

        hence thesis;

      end;

      hence thesis by GROUP_3: 118;

    end;

    theorem :: GRSOLV_1:16

    for G,H be strict Group, h be Homomorphism of G, H holds G is solvable Group implies ( Image h) is solvable

    proof

      let G,H be strict Group;

      let h be Homomorphism of G, H;

      assume G is solvable Group;

      then

      consider F be FinSequence of ( Subgroups 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 Subgroup of G st G1 = (F . i) & G2 = (F . (i + 1)) holds G2 is strict normal Subgroup of G1 & for N be normal Subgroup of G1 st N = G2 holds (G1 ./. N) is commutative by Def1;

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

      then

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

      defpred P[ set, set] means ex J be strict 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 ( Subgroups ( 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 ( Subgroups G) by FINSEQ_2: 11;

        then (F . k) is strict Subgroup of G by GROUP_3:def 1;

        then

        consider A be strict Subgroup of G such that

         A7: A = (F . k);

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

        then (h .: A) in ( Subgroups ( Image h)) by GROUP_3:def 1;

        hence thesis by A7;

      end;

      consider z be FinSequence of ( Subgroups ( 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 G1,G2 be strict Subgroup of ( Image h) st G1 = (z . i) & G2 = (z . (i + 1)) holds G2 is strict normal Subgroup of G1 & for N be normal Subgroup of G1 st N = G2 holds (G1 ./. N) is commutative

      proof

        let i;

        assume that

         A11: i in ( dom z) and

         A12: (i + 1) in ( dom z);

        let G1,G2 be strict Subgroup of ( Image h);

        assume that

         A13: G1 = (z . i) and

         A14: G2 = (z . (i + 1));

        consider A be strict Subgroup of G such that

         A15: A = (F . i) and

         A16: G1 = (h .: A) by A8, A11, A13;

        consider B be strict Subgroup of G such that

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

         A18: G2 = (h .: B) by A8, A12, A14;

        

         A19: for N be normal Subgroup of G1 st N = G2 holds (G1 ./. N) is commutative

        proof

          let N be normal Subgroup of G1;

          assume

           A20: N = G2;

          now

            let x,y be Element of (G1 ./. N);

            x in (G1 ./. N) by STRUCT_0:def 5;

            then

            consider a be Element of G1 such that

             A21: x = (a * N) and x = (N * a) by GROUP_6: 23;

            y in (G1 ./. N) by STRUCT_0:def 5;

            then

            consider b be Element of G1 such that

             A22: y = (b * N) and y = (N * b) by GROUP_6: 23;

            x in the carrier of (G1 ./. N);

            then

             A23: x in ( Cosets N) by GROUP_6: 17;

            then

            reconsider x1 = x as Subset of G1;

            b in (h .: A) by A16, STRUCT_0:def 5;

            then

            consider b1 be Element of A such that

             A24: b = ((h | A) . b1) by GROUP_6: 45;

            reconsider b1 as Element of G by GROUP_2: 42;

            b = (h . b1) by A24, FUNCT_1: 49;

            

            then

             A25: (b * N) = ((h . b1) * (h .: B)) by A18, A20, GROUP_6: 2

            .= (h .: (b1 * B)) by Th13;

            then

            reconsider y2 = (h .: (b1 * B)) as Subset of G1;

            a in (h .: A) by A16, STRUCT_0:def 5;

            then

            consider a1 be Element of A such that

             A26: a = ((h | A) . a1) by GROUP_6: 45;

            reconsider a1 as Element of G by GROUP_2: 42;

            a = (h . a1) by A26, FUNCT_1: 49;

            

            then

             A27: (a * N) = ((h . a1) * (h .: B)) by A18, A20, GROUP_6: 2

            .= (h .: (a1 * B)) by Th13;

            then

            reconsider x2 = (h .: (a1 * B)) as Subset of G1;

            now

              let z be object;

              assume z in (x2 * y2);

              then

              consider z1,z2 be Element of G1 such that

               A28: z = (z1 * z2) and

               A29: z1 in x2 and

               A30: z2 in y2;

              reconsider z22 = z2 as Element of H by A30;

              reconsider z11 = z1 as Element of H by A29;

              z = (z11 * z22) by A28, GROUP_2: 43;

              hence z in ((h .: (a1 * B)) * (h .: (b1 * B))) by A29, A30;

            end;

            then

             A31: (x2 * y2) c= ((h .: (a1 * B)) * (h .: (b1 * B)));

            

             A32: ((a1 * B) * (b1 * B)) = ((b1 * B) * (a1 * B))

            proof

              reconsider K = B as normal Subgroup of A by A4, A9, A11, A12, A15, A17;

              reconsider a2 = a1, b2 = b1 as Element of A;

              

               A33: (a1 * B) = (a2 * K) by GROUP_6: 2;

              then

              reconsider A1 = (a1 * B) as Subset of A;

              

               A34: (b1 * B) = (b2 * K) by GROUP_6: 2;

              then

              reconsider B1 = (b1 * B) as Subset of A;

              reconsider a12 = (a1 * B), b12 = (b1 * B) as Element of ( Cosets K) by A33, A34, GROUP_6: 14;

              (a2 * K) is Element of (A ./. K) by GROUP_6: 22;

              then

              reconsider a11 = a12 as Element of (A ./. K) by GROUP_6: 2;

              (b2 * K) is Element of (A ./. K) by GROUP_6: 22;

              then

              reconsider b11 = b12 as Element of (A ./. K) by GROUP_6: 2;

              now

                let x be object;

                assume x in ((a1 * B) * (b1 * B));

                then

                consider z1,z2 be Element of G such that

                 A35: x = (z1 * z2) and

                 A36: z1 in (a1 * B) & z2 in (b1 * B);

                z1 in A1 & z2 in B1 by A36;

                then

                reconsider z11 = z1, z22 = z2 as Element of A;

                (z1 * z2) = (z11 * z22) by GROUP_2: 43;

                hence x in (A1 * B1) by A35, A36;

              end;

              then

               A37: ((a1 * B) * (b1 * B)) c= (A1 * B1);

              now

                let x be object;

                assume x in ((b1 * B) * (a1 * B));

                then

                consider z1,z2 be Element of G such that

                 A38: x = (z1 * z2) and

                 A39: z1 in (b1 * B) & z2 in (a1 * B);

                z1 in B1 & z2 in A1 by A39;

                then

                reconsider z11 = z1, z22 = z2 as Element of A;

                (z1 * z2) = (z11 * z22) by GROUP_2: 43;

                hence x in (B1 * A1) by A38, A39;

              end;

              then

               A40: ((b1 * B) * (a1 * B)) c= (B1 * A1);

              now

                let x be object;

                assume x in (B1 * A1);

                then

                consider z1,z2 be Element of A such that

                 A41: x = (z1 * z2) and

                 A42: z1 in B1 & z2 in A1;

                reconsider z11 = z1, z22 = z2 as Element of G by A42;

                (z1 * z2) = (z11 * z22) by GROUP_2: 43;

                hence x in ((b1 * B) * (a1 * B)) by A41, A42;

              end;

              then

               A43: (B1 * A1) c= ((b1 * B) * (a1 * B));

              

               A44: (A ./. K) is commutative Group by A4, A9, A11, A12, A15, A17;

              

               A45: for a,b be Element of (A ./. K) holds (the multF of (A ./. K) . (a,b)) = (the multF of (A ./. K) . (b,a)) by A44, BINOP_1:def 2, GROUP_3: 2;

              

               A46: (A1 * B1) = (( CosOp K) . (a11,b11)) by GROUP_6:def 3

              .= (the multF of (A ./. K) . (a12,b12)) by GROUP_6: 18

              .= (the multF of (A ./. K) . (b11,a11)) by A45

              .= (( CosOp K) . (b12,a12)) by GROUP_6: 18

              .= (B1 * A1) by GROUP_6:def 3;

              now

                let x be object;

                assume x in (A1 * B1);

                then

                consider z1,z2 be Element of A such that

                 A47: x = (z1 * z2) and

                 A48: z1 in A1 & z2 in B1;

                reconsider z11 = z1, z22 = z2 as Element of G by A48;

                (z1 * z2) = (z11 * z22) by GROUP_2: 43;

                hence x in ((a1 * B) * (b1 * B)) by A47, A48;

              end;

              then (A1 * B1) c= ((a1 * B) * (b1 * B));

              then ((a1 * B) * (b1 * B)) = (A1 * B1) by A37, XBOOLE_0:def 10;

              hence thesis by A46, A40, A43, XBOOLE_0:def 10;

            end;

            now

              let z be object;

              assume z in (y2 * x2);

              then

              consider z1,z2 be Element of G1 such that

               A49: z = (z1 * z2) and

               A50: z1 in y2 and

               A51: z2 in x2;

              reconsider z22 = z2 as Element of H by A51;

              reconsider z11 = z1 as Element of H by A50;

              z = (z11 * z22) by A49, GROUP_2: 43;

              hence z in ((h .: (b1 * B)) * (h .: (a1 * B))) by A50, A51;

            end;

            then

             A52: (y2 * x2) c= ((h .: (b1 * B)) * (h .: (a1 * B)));

            

             A53: ((h .: (b1 * B)) * (h .: (a1 * B))) = (h .: ((b1 * B) * (a1 * B))) by Th14;

            now

              let z be object;

              assume z in ((h .: (b1 * B)) * (h .: (a1 * B)));

              then

              consider x be object such that

               A54: x in the carrier of G and

               A55: x in ((b1 * B) * (a1 * B)) and

               A56: z = (h . x) by A53, FUNCT_2: 64;

              reconsider x as Element of G by A54;

              consider z1,z2 be Element of G such that

               A57: x = (z1 * z2) and

               A58: z1 in (b1 * B) and

               A59: z2 in (a1 * B) by A55;

              

               A60: (h . z2) in x2 by A59, FUNCT_2: 35;

              then

              reconsider z22 = (h . z2) as Element of G1;

              

               A61: (h . z1) in y2 by A58, FUNCT_2: 35;

              then

              reconsider z11 = (h . z1) as Element of G1;

              z = ((h . z1) * (h . z2)) by A56, A57, GROUP_6:def 6

              .= (z11 * z22) by GROUP_2: 43;

              hence z in (y2 * x2) by A61, A60;

            end;

            then ((h .: (b1 * B)) * (h .: (a1 * B))) c= (y2 * x2);

            then

             A62: (y2 * x2) = ((h .: (b1 * B)) * (h .: (a1 * B))) by A52, XBOOLE_0:def 10;

            

             A63: ((h .: (a1 * B)) * (h .: (b1 * B))) = (h .: ((a1 * B) * (b1 * B))) by Th14;

            now

              let z be object;

              assume z in ((h .: (a1 * B)) * (h .: (b1 * B)));

              then

              consider x be object such that

               A64: x in the carrier of G and

               A65: x in ((a1 * B) * (b1 * B)) and

               A66: z = (h . x) by A63, FUNCT_2: 64;

              reconsider x as Element of G by A64;

              consider z1,z2 be Element of G such that

               A67: x = (z1 * z2) and

               A68: z1 in (a1 * B) and

               A69: z2 in (b1 * B) by A65;

              

               A70: (h . z2) in y2 by A69, FUNCT_2: 35;

              then

              reconsider z22 = (h . z2) as Element of G1;

              

               A71: (h . z1) in x2 by A68, FUNCT_2: 35;

              then

              reconsider z11 = (h . z1) as Element of G1;

              z = ((h . z1) * (h . z2)) by A66, A67, GROUP_6:def 6

              .= (z11 * z22) by GROUP_2: 43;

              hence z in (x2 * y2) by A71, A70;

            end;

            then ((h .: (a1 * B)) * (h .: (b1 * B))) c= (x2 * y2);

            then

             A72: (x2 * y2) = ((h .: (a1 * B)) * (h .: (b1 * B))) by A31, XBOOLE_0:def 10;

            y in the carrier of (G1 ./. N);

            then

             A73: y in ( Cosets N) by GROUP_6: 17;

            then

            reconsider y1 = y as Subset of G1;

            

            thus (x * y) = (( CosOp N) . (x,y)) by GROUP_6: 18

            .= (y1 * x1) by A23, A73, A21, A22, A27, A25, A63, A72, A53, A62, A32, GROUP_6:def 3

            .= (( CosOp N) . (y,x)) by A23, A73, GROUP_6:def 3

            .= (y * x) by GROUP_6: 18;

          end;

          hence thesis by GROUP_1:def 12;

        end;

        B is strict normal Subgroup of A by A4, A9, A11, A12, A15, A17;

        hence thesis by A16, A18, A19, Th15;

      end;

      take z;

      

       A74: ( len z) = ( len F) by A8, FINSEQ_1:def 3;

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

      proof

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

        hence (z . 1) = ( (Omega). ( Image h)) by A2, Th11;

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

        

        hence (z . ( len z)) = ( (1). H) by A3, A74, Th11

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

      end;

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

    end;