:: Solvable Groups
::  by Katarzyna Zawadzka
::
:: Received October 23, 1994
:: Copyright (c) 1994-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, GROUP_1, FINSEQ_1, GROUP_3, XXREAL_0, CARD_1,
      FUNCT_1, RLSUB_1, GROUP_2, RELAT_1, ARYTM_3, STRUCT_0, PRE_TOPC, GROUP_6,
      BINOP_1, TARSKI, XBOOLE_0, QC_LANG1, WELLORD1, NAT_1, FUNCT_2, ALGSTR_0,
      GRAPH_1, GRSOLV_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, ORDINAL1, NAT_1, STRUCT_0,
      ALGSTR_0, BINOP_1, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, GR_CY_1,
      FINSEQ_1, GROUP_1, GROUP_2, GROUP_3, GROUP_6, XXREAL_0;
 constructors BINOP_1, FINSUB_1, REALSET1, GROUP_6, GR_CY_1, RELSET_1;
 registrations XBOOLE_0, FUNCT_1, RELSET_1, XREAL_0, FINSEQ_1, STRUCT_0,
      GROUP_2, GROUP_3, GROUP_6, GR_CY_1, ORDINAL1;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
 definitions GROUP_2, RELAT_1, TARSKI, ALGSTR_0;
 theorems FINSEQ_1, BINOP_1, GROUP_2, GROUP_3, TARSKI, GROUP_6, FINSEQ_2,
      FUNCT_1, FUNCT_2, RELAT_1, XBOOLE_0, XBOOLE_1, NAT_1, GROUP_1, STRUCT_0;
 schemes FINSEQ_1;

begin

reserve i for Element of NAT;

definition
  let IT be Group;
  attr IT is solvable means
  :Def1:
  ex F being 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 for G1,G2 being strict Subgroup of IT st G1=F.i & G2=F.(i+1) holds G2 is
strict normal Subgroup of G1 & for N being 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 set;
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 for G1,G2 being Subgroup of H st
G1=F.i & G2=F.(i+1) holds G2 is normal Subgroup of G1 & for N being 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,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 Th1:
  for G being strict Group, H,F1,F2 being strict Subgroup of G st
  F1 is normal Subgroup of F2 holds F1 /\ H is normal Subgroup of F2 /\ H
proof
  let G be strict 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
  for G being strict Group for F2 being strict Subgroup of G for F1
being strict normal Subgroup of F2 for a,b being Element of F2 holds (a*F1) *(b
  *F1)=a *b *F1
proof
  let G be strict Group;
  let F2 be strict Subgroup of G;
  let F1 be strict 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
  for G being strict Group for H,F2 being strict Subgroup of G for F1
  being strict normal Subgroup of F2 holds for G2 being strict Subgroup of G st
G2=H/\F2 for G1 being normal Subgroup of G2 st G1=H /\ F1 ex G3 being Subgroup
  of F2./.F1 st G2./.G1, G3 are_isomorphic
proof
  let G be strict Group;
  let H,F2 be strict Subgroup of G;
  let F1 be strict normal Subgroup of F2;
  reconsider G2=H /\ F2 as strict Subgroup of G;
  consider f being 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 being 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 strict 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 strict normal Subgroup of G2;
  G2 ./. G1,Image f are_isomorphic by GROUP_6:78;
  hence thesis by A9;
end;

theorem Th4:
  for G being strict Group for H,F2 being strict Subgroup of G for
  F1 being strict normal Subgroup of F2 holds for G2 being strict Subgroup of G
st G2=F2/\H for G1 being normal Subgroup of G2 st G1=F1/\H ex G3 being Subgroup
  of F2./.F1 st G2./.G1, G3 are_isomorphic
proof
  let G be strict Group;
  let H,F2 be strict Subgroup of G;
  let F1 be strict normal Subgroup of F2;
  reconsider G2=F2 /\ H as strict Subgroup of G;
  consider f being 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 being 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 strict 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 strict normal Subgroup of G2;
  G2 ./. G1,Image f are_isomorphic by GROUP_6:78;
  hence thesis by A9;
end;

theorem
  for G being solvable strict Group for H being strict Subgroup of G
  holds H is solvable
proof
  let G be solvable strict Group;
  let H be strict Subgroup of G;
  consider F being 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 for G1,G2 being strict Subgroup
  of G st G1=F.i & G2=F.(i+1) holds G2 is strict normal Subgroup of G1 & for N
  being normal Subgroup of G1 st N=G2 holds G1./.N is commutative by Def1;
  defpred P[set,set] means ex I being strict Subgroup of G st I=F.$1 & $2=I /\
  H;
A5: for k be Nat st k in Seg len F ex x being 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 being 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 for H1,H2 being strict Subgroup of H
  st H1=R.i & H2=R.(i+1) holds H2 is strict normal Subgroup of H1 & for N being
  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 being strict Subgroup of G such that
A10: J=F.(i+1) and
A11: R.(i+1)=J /\ H by A6,A9;
    consider I being 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 being 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 being Subgroup of I./.J1 such that
A18:  H1 ./. N, G3 are_isomorphic by A14,A15,A13,A11,Th4;
      consider h being 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 being Element of G3 such that
A22:    a9=h.a;
        consider b9 being 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 being 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 being 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
  for G being strict Group st ex F being 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
for G1,G2 being strict Subgroup of G st G1=F.i & G2=F.(i+1) holds G2 is strict
normal Subgroup of G1 & for N being normal Subgroup of G1 st N=G2 holds G1./.N
  is cyclic Group holds G is solvable
proof
  let G be strict Group;
  given F being 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 for G1,G2 being strict Subgroup of G st G1=F.i & G2=F.(i+1) holds
G2 is strict normal Subgroup of G1 & for N being normal Subgroup of G1 st N=G2
  holds G1./.N is cyclic Group );
  take F;
  thus thesis by A1;
end;

theorem
  for G being 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 being 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 for G1,G2 being strict Subgroup of G
  st G1=F.i & G2=F.(i+1) holds G2 is strict normal Subgroup of G1 & for N being
  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,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,def 3;
      for N being normal Subgroup of G1 st N=G2 holds G1./.N is commutative
      proof
        let N be normal Subgroup of G1;
        assume N=G2;
        then G1,G1./.N are_isomorphic by A2,A4,A7,A9,A8,GROUP_6:71,TARSKI:def 2
;
        hence thesis by GROUP_6:77;
      end;
      hence
      G2 is strict normal Subgroup of G1 & for N being 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,Def1;
end;

definition
  let G,H be Group;
  let g be Homomorphism of G,H;
  let A be Subgroup of G;
  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 being 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,TARSKI:def 3;
        reconsider a9=a as Element of G by A1,TARSKI:def 3;
        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,TARSKI:def 3;
      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 strict Group;
  let g be Homomorphism of G,H;
  let A be Subgroup of G;
  func g.:A -> strict Subgroup of H equals
  Image (g| A);
  coherence;
end;

theorem Th8:
  for G,H being strict Group, g being Homomorphism of G,H for A
  being strict Subgroup of G holds the carrier of (g.: A)=g.:(the carrier of A)
proof
  let G,H be strict Group;
  let g be Homomorphism of G,H;
  let A be strict 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 Th9:
  for G,H being strict Group, h being Homomorphism of G,H holds
for A being strict Subgroup of G holds Image(h|A) is strict Subgroup of Image h
proof
  let G,H be strict 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
  for G,H being strict Group, h being Homomorphism of G,H holds for A
  being strict Subgroup of G holds h.:A is strict Subgroup of Image h by Th9;

theorem Th11:
  for G,H being strict Group, h being Homomorphism of G,H holds h
  .:((1).G)=(1).H & h.:((Omega).G)=(Omega).(Image h)
proof
  let G,H be strict 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 Th12:
  for G,H being strict Group, h being Homomorphism of G,H for A,B
being strict Subgroup of G holds A is Subgroup of B implies h.:A is 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 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 Th13:
  for G,H being strict Group, h being Homomorphism of G,H for A
being strict Subgroup of G for a being 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 set;
    assume x in h.:(a *A);
    then consider y being set 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 being 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 by TARSKI:def 3;
  now
    let x be set;
    assume x in h.a *h.:A;
    then consider b1 being Element of H such that
A8: x = h.a * b1 and
A9: b1 in h.:A by GROUP_2:103;
    consider b being 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) by TARSKI:def 3;
  hence h.a *h.:A = h.:(a * A) by A7,XBOOLE_0:def 10;
  now
    let x be set;
    assume x in h.:(A* a);
    then consider y being set 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 being 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 by TARSKI:def 3;
  now
    let x be set;
    assume x in h.:A*h.a;
    then consider b1 being Element of H such that
A20: x = b1*h.a and
A21: b1 in h.:A by GROUP_2:104;
    consider b being 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) by TARSKI:def 3;
  hence thesis by A19,XBOOLE_0:def 10;
end;

theorem Th14:
  for G,H being strict Group, h being Homomorphism of G,H for A,B
  being 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 set;
    assume z in h.:(A)*h.:(B);
    then consider z1,z2 being Element of H such that
A1: z=z1 *z2 and
A2: z1 in h.:(A) and
A3: z2 in h.:(B);
    consider z4 being set 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 being set 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)) by TARSKI:def 3;
  now
    let z be set;
    assume z in h.:((A) *(B));
    then consider x being set 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 being 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) by TARSKI:def 3;
  hence thesis by A11,XBOOLE_0:def 10;
end;

theorem Th15:
  for G,H being strict Group, h being Homomorphism of G,H for A,B
being 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 being 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 being 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 set;
      assume x in b2* C;
      then consider g being Element of h.:B such that
A4:   x = b2 * g and
A5:   g in C by GROUP_2:103;
      consider g1 being 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 by TARSKI:def 3;
  end;
  hence thesis by GROUP_3:118;
end;

theorem
  for G,H being strict Group, h being 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 being 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 for G1,G2 being strict Subgroup
  of G st G1=F.i & G2=F.(i+1) holds G2 is strict normal Subgroup of G1 & for N
  being 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 being strict Subgroup of G st J= F.$1 & $2 =h
  .:(J);
A6: for k be Nat st k in Seg len F ex x being 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 being 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 being 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 for G1,G2 being strict Subgroup of
Image h st G1=z.i & G2=z.(i+1) holds G2 is strict normal Subgroup of G1 & for N
  being 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 being strict Subgroup of G such that
A15: A=F.i and
A16: G1=h.:A by A8,A11,A13;
    consider B being strict Subgroup of G such that
A17: B=F.(i+1) and
A18: G2=h.:B by A8,A12,A14;
A19: for N being 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 being 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 being 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 being 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 being 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 set;
          assume z in x2*y2;
          then consider z1,z2 being 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) by TARSKI:def 3;
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 set;
            assume x in (a1 *B) *(b1 * B);
            then consider z1,z2 being 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 by TARSKI:def 3;
          now
            let x be set;
            assume x in (b1 *B) *(a1 * B);
            then consider z1,z2 being 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 by TARSKI:def 3;
          now
            let x be set;
            assume x in B1*A1;
            then consider z1,z2 being 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) by TARSKI:def 3;
A44:      A ./. K is commutative Group by A4,A9,A11,A12,A15,A17;
A45:      for a,b being Element of A./.K holds (the multF of A./.K).(a,b)
          = (the multF of A./.K).(b,a)
          proof
            let a,b be Element of A./.K;
            (the multF of A./.K) is commutative by A44,GROUP_3:2;
            hence thesis by BINOP_1:def 2;
          end;
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 set;
            assume x in A1 * B1;
            then consider z1,z2 being 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) by TARSKI:def 3;
          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 set;
          assume z in y2*x2;
          then consider z1,z2 being 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) by TARSKI:def 3;
A53:    h.:(b1*B)*h.:(a1 * B)=h.:((b1 *B)*(a1 *B)) by Th14;
        now
          let z be set;
          assume z in h.:(b1 *B) *h.:(a1 * B);
          then consider x being set 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 being 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 by TARSKI:def 3;
        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 set;
          assume z in h.:(a1 *B) *h.:(b1 * B);
          then consider x being set 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 being 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 by TARSKI:def 3;
        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 being 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 being 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;