The Mizar article:

Lattice of Subgroups of a Group. Frattini Subgroup

by
Wojciech A. Trybulec

Received August 22, 1990

Copyright (c) 1990 Association of Mizar Users

MML identifier: GROUP_4
[ MML identifier index ]


environ

 vocabulary FINSEQ_1, ARYTM_1, REALSET1, GROUP_2, SETFAM_1, GROUP_1, BOOLE,
      RELAT_1, INT_1, GROUP_3, QC_LANG1, ABSVALUE, VECTSP_1, FINSOP_1, BINOP_1,
      SETWISEO, FUNCT_1, FINSEQ_2, FUNCT_2, RLSUB_1, TARSKI, LATTICES, NAT_1,
      SUBSET_1, RLSUB_2, GROUP_4, CARD_3, FINSEQ_4, ORDINAL2, ARYTM;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, XREAL_0, FINSOP_1,
      ORDINAL1, ORDINAL2, INT_1, SETWISEO, SETFAM_1, RELAT_1, FUNCT_1, FUNCT_2,
      FINSEQ_1, FINSEQ_3, FINSEQ_4, BINOP_1, STRUCT_0, RLVECT_1, VECTSP_1,
      GROUP_2, GROUP_3, LATTICES, GROUP_1, DOMAIN_1, NAT_1;
 constructors FINSOP_1, SETWISEO, FUNCSDOM, FINSEQ_3, GROUP_3, LATTICES,
      DOMAIN_1, NAT_1, FINSEQ_4, MEMBERED, XBOOLE_0, ORDINAL2, ORDINAL1;
 clusters SUBSET_1, FINSEQ_1, GROUP_3, INT_1, LATTICES, GROUP_1, RELSET_1,
      STRUCT_0, RLSUB_2, GROUP_2, XREAL_0, ZFMISC_1, XBOOLE_0, ORDINAL2,
      NUMBERS, ARYTM_3;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
 definitions TARSKI, XBOOLE_0;
 theorems AXIOMS, BINOP_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, FINSOP_1,
      FUNCT_1, FUNCT_2, GROUP_1, GROUP_2, GROUP_3, INT_1, LATTICES, NAT_1,
      ORDERS_1, REAL_1, RLSUB_2, RLVECT_1, SETFAM_1, SUBSET_1, TARSKI,
      ZFMISC_1, VECTSP_1, RELAT_1, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1;
 schemes BINOP_1, DOMAIN_1, FINSEQ_1, FINSEQ_2, NAT_1, ORDERS_2, XBOOLE_0;

begin

definition let D be non empty set; let F be FinSequence of D; let X be set;
 redefine func F - X -> FinSequence of D;
 coherence by FINSEQ_3:93;
end;

scheme MeetSbgEx{G() -> Group, P[set]}:
 ex H being strict Subgroup of G() st
  the carrier of H =
    meet{A where A is Subset of G() :
          ex K being strict Subgroup of G() st A = the carrier of K & P[K]}
 provided
  A1: ex H being strict Subgroup of G() st P[H]
 proof set X = {A where A is Subset of G():
                 ex K being strict Subgroup of G()
                   st A = the carrier of K & P[K]};
   consider T being strict Subgroup of G() such that A2: P[T] by A1;
      carr T = the carrier of T by GROUP_2:def 9;
    then A3: carr T in X by A2;
   then reconsider Y = meet X as Subset of G() by SETFAM_1:8;
      now let Z be set;
      assume Z in X;
       then consider A being Subset of G() such that
       A4: Z = A and
        A5: ex K being strict Subgroup of G() st A = the carrier of K & P[K];
       consider H being Subgroup of G() such that
        A6: A = the carrier of H & P[H] by A5;
          1.G() in H by GROUP_2:55;
     hence 1.G() in Z by A4,A6,RLVECT_1:def 1;
    end;
    then A7: Y <> {} by A3,SETFAM_1:def 1;
    A8: now let a,b be Element of G();
      assume A9: a in Y & b in Y;
         now let Z be set;
         assume A10: Z in X;
          then consider A being Subset of G() such that
          A11: A = Z and
           A12: ex H being strict Subgroup of G()
               st A = the carrier of H & P[H];
          consider H being Subgroup of G() such that
           A13: A = the carrier of H & P[H] by A12;
             a in the carrier of H & b in the carrier of H
                                             by A9,A10,A11,A13,SETFAM_1:def 1;
           then a in H & b in H by RLVECT_1:def 1;
           then a * b in H by GROUP_2:59;
        hence a * b in Z by A11,A13,RLVECT_1:def 1;
       end;
     hence a * b in Y by A3,SETFAM_1:def 1;
    end;
      now let a be Element of G();
      assume A14: a in Y;
         now let Z be set;
         assume A15: Z in X;
          then consider A being Subset of G() such that
          A16: A = Z and
           A17: ex H being strict Subgroup of G()
               st A = the carrier of H & P[H];
          consider H being Subgroup of G() such that
           A18: A = the carrier of H & P[H] by A17;
             a in the carrier of H by A14,A15,A16,A18,SETFAM_1:def 1;
           then a in H by RLVECT_1:def 1;
           then a" in H by GROUP_2:60;
        hence a" in Z by A16,A18,RLVECT_1:def 1;
       end;
     hence a" in Y by A3,SETFAM_1:def 1;
    end;
  hence thesis by A7,A8,GROUP_2:61;
 end;

reserve x,y,y1,y2,X,Y for set,
        k,l,m,n for Nat,
        i,i1,i2,i3,j for Integer,
        G for Group,
        a,b,c,d for Element of G,
        A,B,C for Subset of G,
        H,H1,H2,H3 for Subgroup of G,
        h for Element of H,
        F,F1,F2 for FinSequence of the carrier of G,
        I,I1,I2 for FinSequence of INT;

scheme SubgrSep{G() -> Group,P[set]}:
 ex X st X c= Subgroups G() &
  for H being strict Subgroup of G() holds H in X iff P[H]
 proof
   defpred R[set] means ex H being Subgroup of G() st $1 = H & P[H];
   consider X such that A1: x in X iff x in Subgroups G() &
   R[x] from Separation;
  take X;
  thus X c= Subgroups G()
   proof let x;
     assume x in X;
    hence x in Subgroups G() by A1;
   end;
  let H be strict Subgroup of G();
  thus H in X implies P[H]
   proof assume H in X;
     then ex H1 being Subgroup of G() st H = H1 & P[H1] by A1;
    hence thesis;
   end;
   assume A2: P[H];
      H in Subgroups G() by GROUP_3:def 1;
  hence thesis by A1,A2;
 end;

definition let i;
 canceled;

 func @i -> Element of INT equals
  :Def2:  i;
 coherence by INT_1:12;
end;

canceled 2;

theorem Th3:
 a = h implies a |^ n = h |^ n
  proof assume A1: a = h;
    defpred P[Nat] means a |^ $1 = h |^ $1;
    a |^ 0 = 1.G by GROUP_1:43
             .= 1.H by GROUP_2:53
             .= h |^ 0 by GROUP_1:43; then
    A2: P[0];
    A3: now let n;
     assume A4: P[n];
     a |^ (n + 1) = a |^ n * a by GROUP_1:49
                     .= h |^ n * h by A1,A4,GROUP_2:52
                     .= h |^ (n + 1) by GROUP_1:49;
     hence P[n+1];
    end;
    for n holds P[n] from Ind(A2,A3);
   hence thesis;
  end;

theorem
   a = h implies a |^ i = h |^ i
  proof assume A1: a = h;
      now per cases;
     suppose A2: i >= 0;
      hence a |^ i = a |^ abs( i ) by GROUP_1:55
                 .= h |^ abs( i ) by A1,Th3
                 .= h |^ i by A2,GROUP_1:55;
     suppose A3: i < 0;
       A4: a |^ abs( i ) = h |^ abs( i ) by A1,Th3;
      thus a |^ i = (a |^ abs( i ))" by A3,GROUP_1:56
                .= (h |^ abs( i ))" by A4,GROUP_2:57
                .= h |^ i by A3,GROUP_1:56;
    end;
   hence thesis;
  end;

theorem Th5:
 a in H implies a |^ n in H
  proof assume A1: a in H;
    defpred P[Nat] means a |^ $1 in H;
    a |^ 0 = 1.G by GROUP_1:43;
    then A2: P[0] by GROUP_2:55;
    A3: now let n;
      assume A4: P[n];
         a |^ (n + 1) = a |^ n * a by GROUP_1:49;
     hence P[n+1] by A1,A4,GROUP_2:59;
    end;
    for n holds P[n] from Ind(A2,A3);
   hence thesis;
  end;

theorem Th6:
 a in H implies a |^ i in H
  proof assume A1: a in H;
      now per cases;
     suppose i >= 0;
       then a |^ i = a |^ abs( i ) by GROUP_1:55;
      hence thesis by A1,Th5;
     suppose i < 0;
     then a |^ i = (a |^ abs( i ))" & a |^ abs( i ) in H by A1,Th5,GROUP_1:56;
      hence thesis by GROUP_2:60;
    end;
   hence thesis;
  end;

definition let G be non empty HGrStr;
 let F be FinSequence of the carrier of G;
 func Product F -> Element of G equals
  :Def3:  (the mult of G) "**" F;
 correctness;
end;

canceled;

theorem Th8:
 for G being associative unital (non empty HGrStr),
     F1,F2 being FinSequence of the carrier of G
 holds Product(F1 ^ F2) = Product(F1) * Product(F2)
  proof let G be associative unital (non empty HGrStr),
            F1,F2 be FinSequence of the carrier of G;
   set g = the mult of G;
    A1: g is associative & g has_a_unity by GROUP_1:31,34;
   thus Product(F1 ^ F2) = g "**" (F1 ^ F2) by Def3
                  .= g.(g "**" F1,g "**" F2)by A1,FINSOP_1:6
                  .= g.(Product(F1),g "**" F2) by Def3
                  .= g.(Product F1,Product F2) by Def3
                  .= Product F1 * Product F2 by VECTSP_1:def 10;
  end;

theorem Th9:
 for G being unital (non empty HGrStr),
     F being FinSequence of the carrier of G,
     a being Element of G
 holds Product(F ^ <* a *>) = Product(F) * a
  proof let G be unital (non empty HGrStr),
            F be FinSequence of the carrier of G,
            a be Element of G;
 set g = the mult of G;
    A1: g has_a_unity by GROUP_1:34;
   thus Product(F ^ <* a *>) = g "**" (F ^ <* a *>) by Def3
                      .= g.(g "**" F,a) by A1,FINSOP_1:5
                      .= (g "**" F) * a by VECTSP_1:def 10
                      .= Product F * a by Def3;
  end;

theorem Th10:
  for G being associative unital (non empty HGrStr),
     F being FinSequence of the carrier of G,
     a being Element of G
 holds Product(<* a *> ^ F) = a * Product(F)
  proof let G be associative unital (non empty HGrStr),
            F be FinSequence of the carrier of G,
            a be Element of G;
    set g = the mult of G;
    A1: g is associative & g has_a_unity by GROUP_1:31,34;
   thus Product(<* a *> ^ F) = g "**" (<* a *> ^ F) by Def3
                      .= g.(a,g "**" F) by A1,FINSOP_1:7
                      .= a * (g "**" F) by VECTSP_1:def 10
                      .= a * Product F by Def3;
  end;

theorem Th11:
 for G being unital (non empty HGrStr)
 holds Product <*> the carrier of G = 1.G
  proof let G be unital (non empty HGrStr);
   set g = the mult of G;
    A1: len <*> the carrier of G = 0 & g has_a_unity by FINSEQ_1:32,GROUP_1:34;
   thus Product <*> the carrier of G = g "**" (<*> the carrier of G) by Def3
                              .= the_unity_wrt g by A1,FINSOP_1:def 1
                              .= 1.G by GROUP_1:33;
  end;

theorem Th12:
for G being non empty HGrStr, a being Element of G holds
 Product<* a *> = a
  proof let G be non empty HGrStr, a be Element of G;
   thus Product<* a *> = (the mult of G) "**" <* a *> by Def3
                .= a by FINSOP_1:12;
  end;

theorem Th13:
for G being non empty HGrStr, a,b being Element of G holds
 Product<* a,b *> = a * b
  proof let G be non empty HGrStr, a,b be Element of G;
   thus Product<* a,b *> = (the mult of G) "**" <* a,b *> by Def3
                  .= (the mult of G).(a,b) by FINSOP_1:13
                  .= a * b by VECTSP_1:def 10;
  end;

theorem
   Product<* a,b,c *> = a * b * c & Product<* a,b,c *> = a * (b * c)
  proof <* a,b,c *> = <* a *> ^ <* b,c *> & <* a,b,c *> = <* a,b *> ^ <* c *>
&
        Product<* a *> = a & Product<* c *> = c & Product<* a,b *> = a * b &
        Product<* b,c *> = b * c by Th12,Th13,FINSEQ_1:60;
   hence thesis by Th8;
  end;

Lm1: now let G,a;
 thus Product(0 |-> a) = Product <*> the carrier of G by FINSEQ_2:72
                 .= 1.G by Th11
                 .= a |^ 0 by GROUP_1:43;
end;

Lm2: now let G,a; let n;
  assume A1: Product(n |-> a) = a |^ n;
 thus Product((n + 1) |-> a) = Product((n |-> a) ^ <* a *>) by FINSEQ_2:74
                    .= Product(n |-> a) * Product<* a *> by Th8
                    .= a |^ n * a by A1,Th12
                    .= a |^ (n + 1) by GROUP_1:49;
end;

theorem
   Product(n |-> a) = a |^ n
   proof
     defpred P[Nat] means Product($1 |-> a) = a |^ $1;
A1:  P[0] by Lm1;
A2:  for n being Nat st P[n] holds P[n+1] by Lm2;
     for n being Nat holds P[n] from Ind(A1,A2);
     hence thesis;
   end;

theorem
   Product(F - {1.G}) = Product(F)
  proof defpred P[FinSequence of the carrier of G] means
         Product($1 - {1.G}) = Product$1;
    A1: P[<*> the carrier of G] by FINSEQ_3:81;
    A2: for F,a st P[F] holds P[F ^ <* a *>]
     proof let F,a;
       assume A3: P[F];
        A4: Product((F ^ <* a *>) - {1.G}) =
                Product(((F - {1.G}) ^ (<* a *> - {1.G}))) by FINSEQ_3:80
             .= Product F * Product(<* a *> - {1.G}) by A3,Th8;
          now per cases;
         suppose A5: a = 1.G;
           then a in {1.G} by TARSKI:def 1;
           then <* a *> - {1.G} = <*> the carrier of G by FINSEQ_3:83;
           then Product(<* a *> - {1.G}) = 1.G by Th11;
          hence Product(F ^ <* a *> - {1.G}) = Product(F ^ <* a *>)
            by A4,A5,Th9;
         suppose a <> 1.G;
           then not a in {1.G} by TARSKI:def 1;
           then <* a *> - {1.G} = <* a *> by FINSEQ_3:82;
         hence Product(F ^ <* a *> - {1.G}) = Product(F ^ <* a *>) by A4,Th8;
        end;
      hence thesis;
     end;
      for F holds P[F] from IndSeqD(A1,A2);
   hence thesis;
  end;

Lm3: for F1 being FinSequence, y being Nat st y in dom F1 holds
 len F1 - y + 1 is Nat & len F1 - y + 1 >= 1 & len F1 - y + 1 <= len F1
 proof let F1 be FinSequence, y be Nat;
   assume A1: y in dom F1;
       now assume len F1 - y + 1 < 0;
       then 1 < 0 - (len F1 - y) by REAL_1:86;
       then 1 < - (len F1 - y) by XCMPLX_1:150;
       then 1 < y - len F1 by XCMPLX_1:143;
       then len F1 + 1 < y & y <= len F1 by A1,FINSEQ_3:27,REAL_1:86;
       hence contradiction by NAT_1:37;
      end;
    then reconsider n = len F1 - y + 1 as Nat by INT_1:16;
       y + 0 <= len F1 by A1,FINSEQ_3:27;
     then A2: 0 + 1 = 1 & 0 <= len F1 - y by REAL_1:84;
       n - 1 <= len F1 - y & y >= 1 by A1,FINSEQ_3:27,REAL_1:86;
     then n - 1 - y <= len F1 - y - 1 by REAL_1:92;
     then n - (y + 1) <= len F1 - y - 1 by XCMPLX_1:36;
     then n - (y + 1) <= len F1 - (y + 1) by XCMPLX_1:36;
  hence thesis by A2,AXIOMS:24,REAL_1:54;
 end;

theorem Th17:
 len F1 = len F2 &
  (for k st k in dom F1 holds F2.(len F1 - k + 1) = (F1/.k)") implies
   Product(F1) = Product(F2)"
 proof defpred P[Nat] means
        for F1,F2 st len F1 = $1 & len F1 = len F2 &
         (for k st k in dom F1 holds F2.(len F1 - k + 1) = (F1/.k)") holds
           Product(F1) = Product(F2)";
   A1: P[0]
    proof let F1,F2;
      assume len F1 = 0 & len F1 = len F2;
       then F1 = <*> the carrier of G & F2 = <*> the carrier of G
                                                           by FINSEQ_1:32;
       then Product F1 = 1.G & Product F2 = 1.G & 1.G = (1.G)"
         by Th11,GROUP_1:16;
     hence thesis;
    end;
   A2: for n st P[n] holds P[n + 1]
    proof let n;
      assume A3: P[n];
     let F1,F2;
      assume that A4: len F1 = n + 1 & len F1 = len F2 and
        A5: for k st k in dom F1 holds F2.(len F1 - k + 1) = (F1/.k)";
       reconsider p = F1 | Seg n
 as FinSequence of the carrier of G by FINSEQ_1:23;
          1 <= n + 1 by NAT_1:37;
        then n + 1 in dom F1 by A4,FINSEQ_3:27;
        then F1.(n + 1) in rng F1 & rng F1 c= the carrier of G
                                              by FINSEQ_1:def 4,FUNCT_1:def 5;
       then reconsider a = F1.(n + 1) as Element of G;
        A6: len p = n by A4,FINSEQ_3:59;
       deffunc F(Nat) = F2.($1 + 1);
       consider q being FinSequence such that A7: len q = len p and
        A8: for k st k in Seg len p holds q.k = F(k) from SeqLambda;
A9:     dom q = dom p by A7,FINSEQ_3:31;
A10:    Seg len p = dom p by FINSEQ_1:def 3;
          rng q c= the carrier of G
         proof let x;
           assume x in rng q;
            then consider y such that A11: y in dom q & x = q.y by FUNCT_1:def
5;
            reconsider y as Nat by A11;
             A12: x = F2.(y + 1) by A8,A9,A10,A11;
             A13: 1 <= y + 1 by NAT_1:37;
               y <= len p by A7,A11,FINSEQ_3:27;
             then y + 1 <= len F2 by A4,A6,REAL_1:55;
             then y + 1 in dom F2 by A13,FINSEQ_3:27;
             then x in rng F2 & rng F2 c= the carrier of G
                                          by A12,FINSEQ_1:def 4,FUNCT_1:def 5;
          hence thesis;
         end;
       then reconsider q as FinSequence of the carrier of G by FINSEQ_1:def 4;
        A14: len F2 = len<* a" *> + len q by A4,A6,A7,FINSEQ_1:56;
        A15: now let k;
          assume k in dom<* a" *>;
           then A16: k in {1} by FINSEQ_1:4,def 8;
             len F2 >= 1 by A4,NAT_1:37;
           then A17: len F2 in dom F1 by A4,FINSEQ_3:27;
           then F2.(len F1 - len F1 + 1) = (F1/.len F1)" by A4,A5;
           then (F1/.len F1)" = F2.(0 + 1) by XCMPLX_1:14
                             .= F2.k by A16,TARSKI:def 1;
           then F2.k = a" & k = 1 by A4,A16,A17,FINSEQ_4:def 4,TARSKI:def 1;
         hence <* a" *>.k = F2.k by FINSEQ_1:def 8;
        end;
          now let k;
          assume k in dom q;
           then k in dom q & len<* a" *> = 1 & k + 1 = 1 + k
                                      by FINSEQ_1:56;
         hence F2.(len<* a" *> + k) = q.k by A8,A9,A10;
        end;
        then A18: F2 = <* a" *> ^ q by A14,A15,FINSEQ_3:43;
          now let k;
          assume A19: k in dom p;
           then reconsider i = len p - k + 1 as Nat by Lm3;
              1 <= i & i <= len p by A19,Lm3;
            then i in dom p by FINSEQ_3:27;
            then A20: q.i = F2.(i + 1) by A8,A10;
              len p <= len F1 & k <= len p by A4,A6,A19,FINSEQ_3:27,NAT_1:37;
            then 1 <= k & k <= len F1 by A19,AXIOMS:22,FINSEQ_3:27;
            then A21: k in dom F1 by FINSEQ_3:27;
A22:            i + 1 = (len p + - k + 1) + 1 by XCMPLX_0:def 8
                 .= len F1 + - k + 1 by A4,A6,XCMPLX_1:1
                 .= len F1 - k + 1 by XCMPLX_0:def 8;
              F1/.k = F1.k by A21,FINSEQ_4:def 4
                   .= p.k by A19,FUNCT_1:70
                   .= p/.k by A19,FINSEQ_4:def 4;
         hence q.(len p - k + 1) = (p/.k)" by A5,A20,A21,A22;
        end;
        then A23: Product p = Product q" by A3,A6,A7;
          F1 = p ^ <* a *> by A4,FINSEQ_3:61;
        then A24: Product F1 = Product p * a by Th9;
          Product F2 = a" * Product q by A18,Th10
           .= a" * Product p" by A23,GROUP_1:19
           .= (Product p * a)" by GROUP_1:25;
     hence thesis by A24,GROUP_1:19;
    end;
     for k holds P[k] from Ind(A1,A2);
  hence thesis;
 end;

theorem
   G is commutative Group implies
  for P being Permutation of dom F1 st F2 = F1 * P holds
   Product(F1) = Product(F2)
 proof set g = the mult of G;
   assume G is commutative Group;
    then A1: g is commutative & g has_a_unity & g is associative
                                          by GROUP_1:31,34,GROUP_3:2;
  let P be Permutation of dom F1;
   assume A2: F2 = F1 * P;
  thus Product(F1) = g "**" F1 by Def3
            .= g "**" F2 by A1,A2,FINSOP_1:8
            .= Product(F2) by Def3;
 end;

theorem
   G is commutative Group & F1 is one-to-one & F2 is one-to-one & rng F1 = rng
F2
  implies Product(F1) = Product(F2)
 proof set g = the mult of G;
   assume G is commutative Group;
    then A1: g is commutative & g has_a_unity & g is associative
                                          by GROUP_1:31,34,GROUP_3:2;
   assume A2: F1 is one-to-one & F2 is one-to-one & rng F1 = rng F2;
  thus Product(F1) = g "**" F1 by Def3
            .= g "**" F2 by A1,A2,FINSOP_1:9
            .= Product(F2) by Def3;
 end;

theorem
   G is commutative Group & len F = len F1 & len F = len F2 &
  (for k st k in dom F holds F.k = (F1/.k) * (F2/.k)) implies
   Product(F) = Product(F1) * Product(F2)
 proof set g = the mult of G;
   assume G is commutative Group;
    then A1: g is commutative & g has_a_unity & g is associative
                                          by GROUP_1:31,34,GROUP_3:2;
   assume A2: len F = len F1 & len F = len F2;
   assume A3: for k st k in dom F holds F.k = (F1/.k) * (F2/.k);
    A4: now let k;
      assume A5: k in dom F;
A6:   dom F = Seg len F & dom F1 = Seg len F1 & dom F2 = Seg len F2
       by FINSEQ_1:def 3;
     thus F.k = (F1/.k) * (F2/.k) by A3,A5
             .= g.(F1/.k,F2/.k) by VECTSP_1:def 10
             .= g.(F1.k,F2/.k) by A2,A5,A6,FINSEQ_4:def 4
             .= g.(F1.k,F2.k) by A2,A5,A6,FINSEQ_4:def 4;
    end;
  thus Product(F) = g "**" F by Def3
           .= g.(g "**" F1,g "**" F2) by A1,A2,A4,FINSOP_1:10
           .= (g "**" F1) * (g "**" F2) by VECTSP_1:def 10
           .= Product(F1) * (g "**" F2) by Def3
           .= Product(F1) * Product(F2) by Def3;
 end;

theorem Th21:
 rng F c= carr H implies Product(F) in H
  proof
   defpred P[FinSequence of the carrier of G] means
     rng $1 c= carr H implies Product $1 in H;
    A1:  P[<*> the carrier of G]
    proof assume rng <*> the carrier of G c= carr H;
         1.G in H by GROUP_2:55;
     hence Product(<*> the carrier of G) in H by Th11;
    end;
    A2: now let F,d;
      assume A3: P[F];
      thus P[F^<*d*>]
      proof
      assume A4: rng(F ^ <* d *>) c= carr H;
         rng F c= rng(F ^ <* d *>) & rng<* d *> c= rng(F ^ <* d *>)
                                               by FINSEQ_1:42,43;
       then rng F c= carr H & rng<* d *> c= carr H & rng<* d *> = {d} &
            d in {d} by A4,FINSEQ_1:56,TARSKI:def 1,XBOOLE_1:1;
       then d in H & Product(F) in
 H & Product(F ^ <* d *>) = Product(F) * d by A3,Th9,GROUP_2:88;
     hence Product(F ^ <* d *>) in H by GROUP_2:59;
     end;
    end;
   for F holds P[F] from IndSeqD(A1,A2);
   hence thesis;
  end;

definition let G,I,F;
 func F |^ I -> FinSequence of the carrier of G means
  :Def4: len it = len F &
        for k st k in dom F holds it.k = (F/.k) |^ @(I/.k);
 existence
  proof
      deffunc F(Nat) = (F/.$1) |^ @(I/.$1);
      consider p being FinSequence such that A1: len p = len F and
      A2: for k st k in Seg len F holds p.k = F(k) from SeqLambda;
A3:   dom p = dom F by A1,FINSEQ_3:31;
A4:   dom F = Seg len F by FINSEQ_1:def 3;
        rng p c= the carrier of G
       proof let x;
         assume x in rng p;
          then consider y such that A5: y in dom p & p.y = x by FUNCT_1:def 5;
          reconsider y as Nat by A5;
             x = (F/.y) |^ @(I/.y) & (F/.y) |^ @(I/.y) in the carrier of G
                                                      by A2,A3,A4,A5;
        hence thesis;
       end;
     then reconsider p as FinSequence of the carrier of G by FINSEQ_1:def 4;
   take p;
   thus thesis by A1,A2,A4;
  end;
 uniqueness
  proof let F1,F2;
    assume that A6: len F1 = len F and
                A7: for k st k in dom F holds F1.k = (F/.k) |^ @(I/.k);
    assume that A8: len F2 = len F and
                A9: for k st k in dom F holds F2.k = (F/.k) |^ @(I/.k);
       now let k;
       assume k in Seg len F;
     then A10:  k in dom F by FINSEQ_1:def 3;
      hence F1.k = (F/.k) |^ @(I/.k) by A7
                .= F2.k by A9,A10;
     end;
   hence thesis by A6,A8,FINSEQ_2:10;
  end;
end;

canceled 3;

theorem Th25:
 len F1 = len I1 & len F2 = len I2 implies
  (F1 ^ F2) |^ (I1 ^ I2) = (F1 |^ I1) ^ (F2 |^ I2)
   proof assume A1: len F1 = len I1 & len F2 = len I2;
     set q = F1 |^ I1; set r = F2 |^ I2;
      A2: len(q ^ r) = len q + len r by FINSEQ_1:35
                   .= len F1 + len r by Def4
                   .= len F1 + len F2 by Def4
                   .= len(F1 ^ F2) by FINSEQ_1:35;
         len(F1 ^ F2) = len F1 + len F2 by FINSEQ_1:35
                     .= len(I1 ^ I2) by A1,FINSEQ_1:35;
then A3:   dom (F1 ^ F2) = dom (I1 ^ I2) by FINSEQ_3:31;
        now let k;
        assume A4: k in dom(F1 ^ F2);
           now per cases by A4,FINSEQ_1:38;
          suppose A5: k in dom F1;
            then A6: k in dom I1 by A1,FINSEQ_3:31;
           then A7: I1/.k = I1.k by FINSEQ_4:def 4;
            A8: (I1 ^ I2).k = (I1 ^ I2)/.k by A3,A4,FINSEQ_4:def 4;
              len q = len F1 by Def4;
            then k in dom q by A5,FINSEQ_3:31;
            then A9: (q ^ r).k = q.k by FINSEQ_1:def 7
                             .= (F1/.k) |^ @(I1/.k) by A5,Def4;
              F1/.k = F1.k by A5,FINSEQ_4:def 4
                 .= (F1 ^ F2).k by A5,FINSEQ_1:def 7
                 .= (F1 ^ F2)/.k by A4,FINSEQ_4:def 4;
           hence (q ^ r).k = ((F1 ^ F2)/.k) |^ @((I1 ^ I2)/.k)
             by A6,A7,A8,A9,FINSEQ_1:def 7;
          suppose ex n st n in dom F2 & k = len F1 + n;
            then consider n such that A10: n in dom F2 and A11: k = len F1 + n;
             A12: len r = len F2 & len q = len F1 by Def4;
             then A13: n in dom r & n in dom I2 by A1,A10,FINSEQ_3:31;
             then A14: (q ^ r).k = r.n &
                      (I1 ^ I2).k = I2.n & (F1 ^ F2).k = F2.n &
                      n in dom F2 & (F1 ^ F2).k = (F1 ^ F2)/.k &
                      F2.n = F2/.n
                        by A1,A4,A10,A11,A12,FINSEQ_1:def 7,FINSEQ_4:def 4;
             A15: (I1 ^ I2)/.k = (I1 ^ I2).k by A3,A4,FINSEQ_4:def 4;
               I2/.n = I2.n by A13,FINSEQ_4:def 4;
           hence (q ^ r).k = ((F1 ^ F2)/.k) |^ @((I1 ^ I2)/.k) by A14,A15,Def4
;
         end;
       hence (q ^ r).k = ((F1 ^ F2)/.k) |^ @((I1 ^ I2)/.k);
      end;
    hence thesis by A2,Def4;
   end;

theorem Th26:
 rng F c= carr H implies Product(F |^ I) in H
  proof assume that A1: rng F c= carr H;
      rng(F |^ I) c= carr H
     proof let x;
       assume x in rng(F |^ I);
        then consider y such that A2: y in dom(F |^ I) & x = (F |^ I).y
                                                              by FUNCT_1:def 5;
        reconsider y as Nat by A2;
           len(F |^ I) = len F by Def4;
         then A3: y in dom F by A2,FINSEQ_3:31;
         then A4: x = (F/.y) |^ @(I/.y) by A2,Def4;
           F.y in rng F & F.y = F/.y by A3,FINSEQ_4:def 4,FUNCT_1:def 5;
         then F/.y in H by A1,GROUP_2:88;
         then x in H by A4,Th6;
      hence thesis by GROUP_2:88;
     end;
   hence thesis by Th21;
  end;

theorem Th27:
 (<*> the carrier of G) |^ (<*> INT) = {}
  proof len <*> the carrier of G = 0 & len <*> INT = 0 by FINSEQ_1:32;
    then len((<*> the carrier of G) |^ (<*> INT)) = 0 by Def4;
   hence thesis by FINSEQ_1:25;
  end;

theorem Th28:
 <* a *> |^ <* @i *> = <* a |^ i *>
  proof
A1: len<* a *> = 1 & len<* @i *> = 1 & len<* a |^ i*> = 1 by FINSEQ_1:56;
      now let k;
      assume A2: k in dom <* a *>;
       A3: i = @i & @i = <* @i *>/.1 by Def2,FINSEQ_4:25;
         dom <* a *> = Seg len <* a *> by FINSEQ_1:def 3;
       then A4: k = 1 by A1,A2,FINSEQ_1:4,TARSKI:def 1;
     hence <* a |^ i *>.k = a |^ i by FINSEQ_1:57
                .= (<* a *>/.k) |^ @(<* @i *>/.k) by A3,A4,FINSEQ_4:25;
    end;
   hence thesis by A1,Def4;
  end;

theorem Th29:
 <* a,b *> |^ <* @i,@j *> = <* a |^ i,b |^ j *>
  proof len<* a *> = 1 & len<* b *> = 1 & len <* @i *> = 1 & len<* @j *> = 1 &
        <* a,b *> = <* a *> ^ <* b *> & <* @i,@j *> = <* @i *> ^ <* @j *>
                                                by FINSEQ_1:56,def 9;
   hence <* a,b *> |^ <* @i,@j *> =
                   (<* a *> |^ <* @i *>) ^ (<* b *> |^ <* @j *>) by Th25
                .= <* a |^ i *> ^ (<* b *> |^ <* @j *>) by Th28
                .= <* a |^ i *> ^ <* b |^ j *> by Th28
                .= <* a |^ i,b |^ j *> by FINSEQ_1:def 9;
  end;

theorem
   <* a,b,c *> |^ <* @i1,@i2,@i3 *> = <* a |^ i1,b |^ i2,c |^ i3 *>
  proof len<* a *> = 1 & len<* b,c *> = 2 &
        len <* @i1 *> = 1 & len<* @i2,@i3 *> = 2 &
        <* a,b,c *> = <* a *> ^ <* b,c *> &
        <* @i1,@i2,@i3 *> = <* @i1 *> ^ <* @i2,@i3 *>
                                    by FINSEQ_1:56,60,61;
   hence <* a,b,c *> |^ <* @i1,@i2,@i3 *> =
                (<* a *> |^ <* @i1 *>) ^ (<* b,c *> |^ <* @i2,@i3 *>) by Th25
             .= <* a |^ i1 *> ^ (<* b,c *> |^ <* @i2,@i3 *>) by Th28
             .= <* a |^ i1 *> ^ <* b |^ i2,c |^ i3 *> by Th29
             .= <* a |^ i1,b |^ i2,c |^ i3 *> by FINSEQ_1:60;
  end;

theorem
   F |^ (len F |-> @(1)) = F
  proof defpred P[FinSequence of the carrier of G] means
         $1 |^ (len $1 |-> @(1)) = $1;
    A1: P[<*> the carrier of G]
     proof set A = <*> the carrier of G;
      thus A |^ (len A |-> @(1)) = A |^ (0 |-> @(1)) by FINSEQ_1:32
                                  .= A |^ (<*> INT) by FINSEQ_2:72
                                  .= A by Th27;
     end;
    A2: for F,a st P[F] holds P[F ^ <* a *>]
     proof let F,a; set A = F ^ <* a *>;
       assume A3: P[F];
        A4: len A = len F + len<* a *> by FINSEQ_1:35;
        A5: len<* a *> = 1 by FINSEQ_1:57;
        A6: len<* @(1) *> = 1 by FINSEQ_1:57;
        A7: len(len F |-> @(1)) = len F by FINSEQ_2:69;
      thus A |^ (len A |-> @(1)) = A |^ ((len F |-> @(1)) ^ <* @(1) *>)
                                                           by A4,A5,FINSEQ_2:74
         .= (F |^ (len F |-> @(1))) ^ (<* a *> |^ <* @(1) *>)
                                                           by A5,A6,A7,Th25
         .= F ^ <* a |^ 1 *> by A3,Th28
         .= F ^ <* a *> by GROUP_1:44;
     end;
      for F holds P[F] from IndSeqD(A1,A2);
   hence thesis;
  end;

theorem
   F |^ (len F |-> @(0)) = len F |-> 1.G
  proof defpred P[FinSequence of the carrier of G] means
         $1 |^ (len $1 |-> @(0)) = len $1 |-> 1.G;
    A1: P[<*> the carrier of G]
     proof set A = <*> the carrier of G;
       A2: len A = 0 by FINSEQ_1:32;
      thus A |^ (len A |-> @(0)) = A |^ (0 |-> @(0)) by FINSEQ_1:32
                                  .= A |^ (<*> INT) by FINSEQ_2:72
                                  .= {} by Th27
                                  .= len A |-> 1.G by A2,FINSEQ_2:72;
     end;
    A3: for F,a st P[F] holds P[F ^ <* a *>]
     proof let F,a; set A = F ^ <* a *>;
       assume A4: P[F];
        A5: len A = len F + len<* a *> by FINSEQ_1:35;
        A6: len<* a *> = 1 by FINSEQ_1:57;
        A7: len<* @(0) *> = 1 by FINSEQ_1:57;
        A8: len(len F |-> @(0)) = len F by FINSEQ_2:69;
      thus A |^ (len A |-> @(0)) = A |^ ((len F |-> @(0)) ^ <* @(0) *>)
                                                           by A5,A6,FINSEQ_2:74
         .= (F |^ (len F |-> @(0))) ^ (<* a *> |^ <* @(0) *>)
                                                           by A6,A7,A8,Th25
         .= (len F |-> 1.G) ^ <* a |^ 0 *> by A4,Th28
         .= (len F |-> 1.G) ^ <* 1.G *> by GROUP_1:43
         .= (len A |-> 1.G) by A5,A6,FINSEQ_2:74;
     end;
      for F holds P[F] from IndSeqD(A1,A3);
   hence thesis;
  end;

theorem
   len I = n implies (n |-> 1.G) |^ I = n |-> 1.G
  proof defpred P[Nat] means
         for I st len I = $1 holds ($1 |-> 1.G) |^ I = $1 |-> 1.G;
    A1: P[0]
     proof let I;
       assume len I = 0;
        then I = <*> INT & (0 |-> 1.G) = {} & {} = <*> the carrier of G
                                     by FINSEQ_1:32,FINSEQ_2:72;
      hence (0 |-> 1.G) |^ I = 0 |-> 1.G by Th27;
     end;
    A2: for k st P[k] holds P[k + 1]
     proof let k;
       assume A3: P[k];
      let I;
       assume A4: len I = k + 1;
        reconsider J = I | Seg k as FinSequence of INT by FINSEQ_1:23;
         A5: len J = k by A4,FINSEQ_3:59;
         then A6: (k |-> 1.G) |^ J = k |-> 1.G by A3;
           1 <= k + 1 by NAT_1:37;
         then k + 1 in dom I by A4,FINSEQ_3:27;
         then I.(k + 1) in
 rng I & rng I c= INT by FINSEQ_1:def 4,FUNCT_1:def 5;

         then reconsider i = I.(k + 1) as Integer by INT_1:12;
         A7: I = J ^ <* i *> by A4,FINSEQ_3:61
              .= J ^ <* @i *> by Def2;
         A8: (k + 1) |-> 1.G = (k |-> 1.G) ^ <* 1.G *> by FINSEQ_2:74;
           len(k |-> 1.G) = k & len<* 1.G *> = 1 & len<* @i *> = 1
                                            by FINSEQ_1:57,FINSEQ_2:69;
         then ((k + 1) |-> 1.G) |^ I =
                 ((k |-> 1.G) |^ J) ^ (<* 1.G *> |^ <* @i *>)
                                                        by A5,A7,A8,Th25
           .= (k |-> 1.G) ^ <* (1.G) |^ i *> by A6,Th28
           .= (k |-> 1.G) ^ <* 1.G *> by GROUP_1:61;
      hence thesis by FINSEQ_2:74;
     end;
      for k holds P[k] from Ind(A1,A2);
   hence thesis;
  end;

definition let G,A;
 func gr A -> strict Subgroup of G means
  :Def5: A c= the carrier of it &
       (for H being strict Subgroup of G
         st A c= the carrier of H holds it is Subgroup of H);
 existence
  proof
    defpred P[set] means ex H st $1 = carr H & A c= $1;
    consider X such that A1: Y in X iff Y in bool the carrier of G &
         P[Y] from Separation;
    set M = meet X;
A2:     the carrier of G in bool the carrier of G &
     the carrier of the HGrStr of G = the carrier of (Omega).G &
     A c= the carrier of G &
     carr (Omega).G = the carrier of (Omega).
G by GROUP_2:def 8,def 9,ZFMISC_1:def 1;
     then A3: the carrier of G in X by A1;
     A4: X <> {} by A1,A2;
       now let Y;
       assume Y in X;
        then consider H such that A5: Y = carr H and A c= Y by A1;
           1.G in H by GROUP_2:55;
      hence 1.G in Y by A5,GROUP_2:88;
     end;
     then A6: M <> {} by A4,SETFAM_1:def 1;
       M c= the carrier of G
      proof consider x such that A7: x in X by A3;
       consider H such that A8: x = carr H and A c= x by A1,A7;
       let y;
       assume y in M;
       then y in carr H & carr H c= the carrier of G by A7,A8,SETFAM_1:def 1;
       hence thesis;
      end;
    then reconsider M as Subset of G;
     A9: now let a,b;
       assume A10: a in M & b in M;
          now let Y;
         assume A11: Y in X;
          then consider H such that A12: Y = carr H and A c= Y by A1;
             a in carr H & b in carr H by A10,A11,A12,SETFAM_1:def 1;
         hence a * b in Y by A12,GROUP_2:89;
        end;
      hence a * b in M by A4,SETFAM_1:def 1;
     end;
       now let a;
       assume A13: a in M;
          now let Y;
         assume A14: Y in X;
          then consider H such that A15: Y = carr H and A c= Y by A1;
             a in carr H by A13,A14,A15,SETFAM_1:def 1;
         hence a" in Y by A15,GROUP_2:90;
        end;
      hence a" in M by A4,SETFAM_1:def 1;
     end;
    then consider H being strict Subgroup of G such that
    A16: the carrier of H = M by A6,A9,GROUP_2:61;
   take H;
       now let Y;
       assume Y in X;
        then ex H st Y = carr H & A c= Y by A1;
      hence A c= Y;
     end;
   hence A c= the carrier of H by A4,A16,SETFAM_1:6;
   let H1 be strict Subgroup of G;
    assume A17: A c= the carrier of H1;
        the carrier of H1 = carr H1 by GROUP_2:def 9;
     then the carrier of H1 in X by A1,A17;
     then M c= the carrier of H1 by SETFAM_1:4;
   hence H is Subgroup of H1 by A16,GROUP_2:66;
  end;
 uniqueness
  proof let H1,H2 be strict Subgroup of G;
    assume A c= the carrier of H1 &
     (for H being strict Subgroup of G
       st A c= the carrier of H holds H1 is Subgroup of H) &
     A c= the carrier of H2 &
     (for H being strict Subgroup of G
       st A c= the carrier of H holds H2 is Subgroup of H);
     then H1 is Subgroup of H2 & H2 is Subgroup of H1;
   hence thesis by GROUP_2:64;
  end;
end;

canceled 3;

theorem Th37:
 a in gr A iff ex F,I st len F = len I & rng F c= A & Product(F |^ I) = a
  proof
   thus a in gr A implies ex F,I st len F = len I & rng F c= A &
     Product(F |^ I) = a
    proof assume A1: a in gr A;
      defpred P[set] means
        ex F,I st $1 = Product (F |^ I) & len F = len I & rng F c= A;
      reconsider B = {b : P[b]}
        as Subset of G from SubsetD;
         1.G = Product <*> the carrier of G & <*> the carrier of G = {} &
       (<*> the carrier of G) |^ (<*> INT) = {} &
       rng <*> the carrier of G = {} & {} c= A & len {} = 0 & len<*>INT = 0
        by Th11,Th27,FINSEQ_1:25,27,XBOOLE_1:2;
       then A2: 1.G in B;
       A3: now let c,d;
         assume that A4: c in B and A5: d in B;
 A6:          ex d1 being Element of G st c = d1 &
           ex F,I st d1 = Product(F |^ I) & len F = len I & rng F c= A by A4;
 A7:          ex d2 being Element of G st d = d2 &
           ex F,I st d2 = Product(F |^ I) & len F = len I & rng F c= A by A5;
          consider F1,I1 such that A8: c = Product(F1 |^ I1) and
                          A9: len F1 = len I1 and A10: rng F1 c= A by A6;
          consider F2,I2 such that A11: d = Product(F2 |^ I2) and
                                   A12: len F2 = len I2 and
                                   A13: rng F2 c= A by A7;
           A14: c * d = Product((F1 |^ I1) ^ (F2 |^ I2)) by A8,A11,Th8
                   .= Product((F1 ^ F2) |^ (I1 ^ I2)) by A9,A12,Th25;
             rng(F1 ^ F2) = rng F1 \/ rng F2 by FINSEQ_1:44;
           then A15: rng(F1 ^ F2) c= A by A10,A13,XBOOLE_1:8;
             len(F1 ^ F2) = len I1 + len I2 by A9,A12,FINSEQ_1:35
                       .= len(I1 ^ I2) by FINSEQ_1:35;
        hence c * d in B by A14,A15;
       end;
         now let c;
         assume c in B;
          then ex d1 being Element of G st c = d1 &
           ex F,I st d1 = Product(F |^ I) & len F = len I & rng F c= A;
          then consider F1,I1 such that A16: c = Product(F1 |^ I1) and
                                   A17: len F1 = len I1 and A18: rng F1 c= A;
A19:       dom F1 = dom I1 by A17,FINSEQ_3:31;
          deffunc F(Nat) = F1.(len F1 - $1 + 1);
          consider F2 being FinSequence such that A20: len F2 = len F1 and
           A21: for k st k in Seg len F1 holds F2.k = F(k) from SeqLambda;
A22:       dom F2 = dom F1 by A20,FINSEQ_3:31;
A23:       Seg len F1 = dom F1 by FINSEQ_1:def 3;
          defpred P[Nat,set] means ex i st i = I1.(len I1 - $1 + 1) & $2 = - i;
           A24: for k,y1,y2 st k in Seg len I1 & P[k,y1] & P[k,y2] holds
                   y1 = y2;
           A25: for k st k in Seg len I1 ex x st P[k,x]
            proof let k;
              assume k in Seg len I1;
            then A26: k in dom I1 by FINSEQ_1:def 3;
               then reconsider n = len I1 - k + 1 as Nat by Lm3;
                  1 <= n & n <= len I1 by A26,Lm3;
                then n in dom I1 by FINSEQ_3:27;
                then I1.n in
 rng I1 & rng I1 c= INT by FINSEQ_1:def 4,FUNCT_1:def 5;
               then reconsider i = I1.n as Element of INT qua non empty set;
               reconsider i as Integer;
               reconsider x = - i as set;
             take x,i;
             thus thesis;
            end;
          consider I2 being FinSequence such that A27: dom I2 = Seg len I1 and
           A28: for k st k in Seg len I1 holds P[k,I2.k] from SeqEx(A24,A25);
A29:        Seg len I1 = dom I1 by FINSEQ_1:def 3;
A30:        len F2 = len I2 by A17,A20,A27,FINSEQ_1:def 3;
A31:        dom F2 = dom I2 by A17,A20,A27,FINSEQ_1:def 3;
           A32: rng F2 c= rng F1
            proof let x;
              assume x in rng F2;
               then consider y such that A33: y in dom F2 & F2.y = x
                                                         by FUNCT_1:def 5;
               reconsider y as Nat by A33;
                A34: x = F1.(len F1 - y + 1) by A21,A22,A23,A33;
               reconsider n = len F1 - y + 1 as Nat by A20,A33,Lm3;
                A35: 1 <= n by A20,A33,Lm3;
                  n <= len F1 by A20,A33,Lm3;
                then n in dom F1 by A35,FINSEQ_3:27;
             hence thesis by A34,FUNCT_1:def 5;
            end;
           then A36: rng F2 c= A by A18,XBOOLE_1:1;
             rng F1 c= the carrier of G by FINSEQ_1:def 4;
           then rng F2 c= the carrier of G by A32,XBOOLE_1:1;
          then reconsider F2 as FinSequence of the carrier of G by FINSEQ_1:def
4;
             rng I2 c= INT
            proof let x;
              assume x in rng I2;
               then consider y such that A37: y in dom I2 and A38: x = I2.y
                                                              by FUNCT_1:def 5;
               reconsider y as Nat by A37;
                  ex i st i = I1.(len I1 - y + 1) & x = - i by A27,A28,A37,A38;
             hence thesis by INT_1:12;
            end;
          then reconsider I2 as FinSequence of INT by FINSEQ_1:def 4;
          set p = F1 |^ I1; set q = F2 |^ I2;
A39:       len p = len F1 & len q = len F2 by Def4;
then A40:       dom p = dom F1 & dom q = dom F2 by FINSEQ_3:31;
             now let k;
             assume A41: k in dom q;
              then reconsider n = len p - k + 1 as Nat by A20,A39,Lm3;
                 1 <= n & len p >= n by A20,A39,A41,Lm3;
then A42:            n in dom I2 & n in Seg len I2
                                     by A20,A30,A39,FINSEQ_1:3,FINSEQ_3:27;
                dom q = dom I1 by A17,A20,A39,FINSEQ_3:31;
              then consider i such that A43: i = I1.n & I2.k = - i by A17,A28,
A29,A39,A41;
                 I2.k = I2/.k & I2/.k = @(I2/.k)
                                   by A31,A40,A41,Def2,FINSEQ_4:def 4;
               then q.k = (F2/.k) |^ (- i) & F2/.k = F2.k & F2.k = F1.n &
               F1/.n= F1.n by A17,A21,A22,A23,A27,A39,A40,A41,A42,A43,Def4,
FINSEQ_4:def 4;
               then A44: q.k = ((F1/.n) |^ i)" by GROUP_1:70;
                 I1.n = I1/.n & I1/.n = @(I1/.n)
                              by A27,A29,A42,Def2,FINSEQ_4:def 4;
               then p.n = (F1/.n) |^ i by A19,A27,A29,A42,A43,Def4;
               then (p/.n)" = ((F1/.n) |^ i)" & q/.k = q.k
                              by A19,A27,A29,A40,A41,A42,FINSEQ_4:def 4;
               then p/.n = (q/.k)" by A44,GROUP_1:19;
            hence (q/.k)" = p.(len p - k + 1)
                 by A19,A27,A29,A40,A42,FINSEQ_4:def 4;
           end;
           then Product p" = Product q by A20,A39,Th17;
        hence c" in B by A16,A30,A36;
       end;
      then consider H being strict Subgroup of G such that
      A45: the carrier of H = B by A2,A3,GROUP_2:61;
         A c= B
        proof let x;
          assume A46: x in A;
           then reconsider a = x as Element of G;
           reconsider p = 1 as Integer;
            A47: len<* a *> = 1 & len<* @p *> = 1 by FINSEQ_1:56;
            A48: Product(<* a *> |^ <* @p *>) = Product<* a |^ 1 *> by Th28
                                     .= a |^ 1 by Th12
                                     .= a by GROUP_1:44;
              rng<* a *> = {a} & {a} c= A by A46,FINSEQ_1:56,ZFMISC_1:37;
         hence thesis by A47,A48;
        end;
       then gr A is Subgroup of H by A45,Def5;
       then a in H by A1,GROUP_2:49;
       then a in B by A45,RLVECT_1:def 1;
      then ex b st
 b = a & ex F,I st b = Product(F |^ I) & len F = len I & rng F c= A;
     hence thesis;
    end;
    given F,I such that len F = len I and A49: rng F c= A and
                        A50: Product(F |^ I) = a;
       A c= the carrier of gr A by Def5;
     then A c= carr gr A by GROUP_2:def 9;
     then rng F c= carr gr A by A49,XBOOLE_1:1;
   hence thesis by A50,Th26;
  end;

theorem Th38:
 a in A implies a in gr A
  proof assume A1: a in A;
      A c= the carrier of gr A by Def5;
    hence thesis by A1,RLVECT_1:def 1;
  end;

theorem
   gr {} the carrier of G = (1).G
  proof
    A1: {} the carrier of G c= the carrier of (1).G by XBOOLE_1:2;
      for H being strict Subgroup of G
      st {} the carrier of G c= the carrier of H holds
     (1).G is Subgroup of H by GROUP_2:77;
   hence thesis by A1,Def5;
  end;

theorem Th40:
 for H being strict Subgroup of G holds gr carr H = H
  proof let H be strict Subgroup of G;
   A1: carr H = the carrier of H by GROUP_2:def 9;
      now let H1 be strict Subgroup of G;
      assume carr H c= the carrier of H1;
       then the carrier of H c= the carrier of H1 by GROUP_2:def 9;
     hence H is Subgroup of H1 by GROUP_2:66;
    end;
   hence thesis by A1,Def5;
  end;

theorem Th41:
 A c= B implies gr A is Subgroup of gr B
  proof assume A1: A c= B;
      now let a;
      assume a in gr A;
       then consider F,I such that
        A2: len F = len I & rng F c= A & Product(F |^ I) = a by Th37;
          rng F c= B by A1,A2,XBOOLE_1:1;
     hence a in gr B by A2,Th37;
    end;
   hence thesis by GROUP_2:67;
  end;

theorem
   gr(A /\ B) is Subgroup of gr A /\ gr B
  proof
      now let a;
      assume a in gr(A /\ B);
       then consider F,I such that
        A1: len F = len I & rng F c= A /\ B & Product(F |^ I) = a by Th37;
          A /\ B c= A & A /\ B c= B by XBOOLE_1:17;
        then rng F c= A & rng F c= B by A1,XBOOLE_1:1;
        then a in gr A & a in gr B by A1,Th37;
     hence a in gr A /\ gr B by GROUP_2:99;
    end;
   hence thesis by GROUP_2:67;
  end;

theorem Th43:
 the carrier of gr A =
  meet{B : ex H being strict Subgroup of G
   st B = the carrier of H & A c= carr H}
  proof
    defpred P[Subgroup of G] means A c= carr $1;
  A1: A c= the carrier of G & the carrier of (Omega).G = carr (Omega).G &
           (Omega).G = the HGrStr of G by GROUP_2:def 8,def 9;
     then A2: ex H being strict Subgroup of G st P[H];
    consider H being strict Subgroup of G such that A3: the carrier of H =
     meet{B : ex H being strict Subgroup of G
            st B = the carrier of H & P[H]} from MeetSbgEx(A2);
    set X = {B :ex H being strict Subgroup of G
                st B = the carrier of H & A c= carr H};
A4:     carr (Omega).G in X by A1;
       now let Y;
       assume Y in X;
        then ex B st Y = B & ex H being strict Subgroup of G
              st B = the carrier of H & A c= carr H;
      hence A c= Y by GROUP_2:def 9;
     end;
     then A5: A c= the carrier of H by A3,A4,SETFAM_1:6;
       now let H1 be strict Subgroup of G;
       assume A6: A c= the carrier of H1;
          the carrier of H1 = carr H1 by GROUP_2:def 9;
        then the carrier of H1 in X by A6;
        then the carrier of H c= the carrier of H1 by A3,SETFAM_1:4;
      hence H is Subgroup of H1 by GROUP_2:66;
     end;
   hence thesis by A3,A5,Def5;
  end;

theorem Th44:
 gr A = gr(A \ {1.G})
  proof
    set X = {B : ex H being strict Subgroup of G
                   st B = the carrier of H & A c= carr H};
    set Y = {C : ex H being strict Subgroup of G
                   st C = the carrier of H & A \ {1.G} c= carr H};
     A1: X = Y
      proof
       thus X c= Y
        proof let x;
          assume x in X;
           then consider B such that A2: x = B and
            A3: ex H being strict Subgroup of G
                st B = the carrier of H & A c= carr H;
           consider H being strict Subgroup of G such that
            A4: B = the carrier of H and A5: A c= carr H
                                                                          by A3
;
              A \ {1.G} c= A by XBOOLE_1:36;
            then A \ {1.G} c= carr H by A5,XBOOLE_1:1;
         hence thesis by A2,A4;
        end;
       let x;
        assume x in Y;
         then consider B such that A6: x = B and
          A7: ex H being strict Subgroup of G
               st B = the carrier of H & A \ {1.G} c= carr H;
         consider H being strict Subgroup of G such that
           A8: B = the carrier of H and
           A9: A \ {1.G} c= carr H by A7;
            1.G in H by GROUP_2:55;
          then 1.G in carr H by GROUP_2:88;
          then {1.G} c= carr H by ZFMISC_1:37;
          then A10: (A \ {1.G}) \/ {1.G} c= carr H by A9,XBOOLE_1:8;
             now per cases;
            suppose 1.G in A;
               then {1.G} c= A by ZFMISC_1:37;
             hence A c= carr H by A10,XBOOLE_1:45;
            suppose not 1.G in A;
             hence A c= carr H by A9,ZFMISC_1:65;
           end;
       hence thesis by A6,A8;
      end;
       the carrier of gr A = meet X by Th43
                        .= the carrier of gr(A \ {1.G}) by A1,Th43;
   hence thesis by GROUP_2:68;
  end;

definition let G,a;
 attr a is generating means
  :Def6:
   not for A st gr A = the HGrStr of G holds gr(A \ {a}) = the HGrStr of G;
end;

canceled;

theorem
   1.G is non generating
  proof let A;
    assume gr A = the HGrStr of G;
   hence thesis by Th44;
  end;

definition let G, H;
 attr H is maximal means
  :Def7: the HGrStr of H <> the HGrStr of G &
   for K being strict Subgroup of G st
    the HGrStr of H <> K & H is Subgroup of K
     holds K = the HGrStr of G;
end;

canceled;

theorem Th48:
 for G being strict Group, H being strict Subgroup of G,
    a being Element of G holds
 H is maximal & not a in H implies gr(carr H \/ {a}) = G
  proof let G be strict Group, H be strict Subgroup of G,
            a be Element of G;
   assume that A1: H is maximal and A2: not a in H;
      a in {a} by TARSKI:def 1;
    then carr H c= carr H \/ {a} & a in carr H \/ {a}
                                              by XBOOLE_0:def 2,XBOOLE_1:7;
    then gr carr H is Subgroup of gr(carr H \/ {a}) &
         a in gr(carr H \/ {a}) by Th38,Th41;
    then H is Subgroup of gr(carr H \/ {a}) & H <> gr(carr H \/ {a})
                                                                 by A2,Th40;
   hence thesis by A1,Def7;
  end;

::
::  Frattini subgroup.
::

definition let G be Group;
 func Phi(G) -> strict Subgroup of G means
  :Def8: the carrier of it =
              meet{A where A is Subset of G :
                 ex H being strict Subgroup of G
                 st A = the carrier of H & H is maximal} if
               ex H being strict Subgroup of G st H is maximal otherwise
             it = the HGrStr of G;
 existence
  proof
     defpred P[Subgroup of G] means $1 is maximal;
      now per cases;
     suppose A1: ex H being strict Subgroup of G st P[H];
          ex H being strict Subgroup of G st the carrier of H =
            meet{A where A is Subset of
            G: ex K being strict Subgroup of G
             st A = the carrier of K & P[K]} from MeetSbgEx(A1);
      hence thesis by A1;
     suppose A2: for H being strict Subgroup of G holds H is not maximal;
         (Omega).G = the HGrStr of G &
       (Omega).G is Subgroup of G by GROUP_2:def 8;
      hence thesis by A2;
    end;
   hence thesis;
  end;
 uniqueness by GROUP_2:68;
 correctness;
end;

canceled 3;

theorem Th52:
 for G being Group holds
 (ex H being strict Subgroup of G st H is maximal) implies
  (a in Phi(G) iff
    for H being strict Subgroup of G st H is maximal holds a in H)
 proof let G be Group;
  assume A1: ex H being strict Subgroup of G st H is maximal;
   set X = {A where A is Subset of
   G: ex K being strict Subgroup of G
       st A = the carrier of K & K is maximal};
  thus a in Phi(G) implies
   for H being strict Subgroup of G st H is maximal holds a in H
   proof assume a in Phi(G);
      then a in the carrier of Phi(G) by RLVECT_1:def 1;
      then A2: a in meet X by A1,Def8;
    let H be strict Subgroup of G;
     assume A3: H is maximal;
        the carrier of H = carr H by GROUP_2:def 9;
      then carr H in X by A3;
      then a in carr H by A2,SETFAM_1:def 1;
    hence thesis by GROUP_2:88;
   end;
    consider H being strict Subgroup of G such that A4: H is maximal by A1;
       carr H = the carrier of H by GROUP_2:def 9;
     then A5: carr H in X by A4;
   assume A6: for H being strict Subgroup of G st H is maximal holds a in H;
      now let Y;
      assume Y in X;
       then consider A being Subset of G such that A7: Y = A and
        A8: ex H being strict Subgroup of G
            st A = the carrier of H & H is maximal;
       consider H being strict Subgroup of G such that
       A9: A = the carrier of H & H is maximal by A8;
          A = carr H & a in H by A6,A9,GROUP_2:def 9;
     hence a in Y by A7,GROUP_2:88;
    end;
    then a in meet X by A5,SETFAM_1:def 1;
    then a in the carrier of Phi(G) by A1,Def8;
  hence thesis by RLVECT_1:def 1;
 end;

theorem
   for G being Group, a being Element of G holds
 (for H being strict Subgroup of G holds H is not maximal) implies a in Phi(G)
  proof let G be Group, a be Element of G;
   assume for H being strict Subgroup of G holds H is not maximal;
    then Phi(G) = the HGrStr of G by Def8;
   hence thesis by RLVECT_1:def 1;
  end;

theorem Th54:
 for G being Group, H being strict Subgroup of G holds
 H is maximal implies Phi(G) is Subgroup of H
  proof let G be Group, H be strict Subgroup of G;
   assume H is maximal;
    then for a be Element of G
    holds a in Phi(G) implies a in H by Th52;
   hence thesis by GROUP_2:67;
  end;

theorem Th55:
 for G being strict Group holds
 the carrier of Phi(G) = {a where a is Element of
 G: a is non generating}
  proof let G be strict Group;
    set A = {a where a is Element of G: a is non generating};
   thus the carrier of Phi(G) c= A
    proof let x;
      assume A1: x in the carrier of Phi(G);
      assume A2: not x in A;
          x in Phi(G) by A1,RLVECT_1:def 1;
        then x in G by GROUP_2:49;
       then reconsider a = x as Element of G by RLVECT_1:def 1;
          a is generating by A2;
       then consider B being Subset of G such that
       A3: gr B = G and A4: gr(B \ {a}) <> G by Def6;
       set M = B \ {a};
       defpred P[Subgroup of G] means M c= carr $1 & not a in $1;
       consider X such that A5: X c= Subgroups G and
        A6: for H being strict Subgroup of G holds
         H in X iff P[H] from SubgrSep;
          M c= the carrier of gr M by Def5;
        then A7: M c= carr gr M by GROUP_2:def 9;
          now assume A8: a in gr M;
            now let b be Element of G;
               b in gr B by A3,RLVECT_1:def 1;
            then consider F being FinSequence of the carrier of G,
                   I such that len I = len F and
             A9: rng F c= B and A10: b = Product(F |^ I) by Th37;
               rng(F |^ I) c= carr gr M
              proof let x;
                assume x in rng(F |^ I);
                 then consider y such that A11: y in dom(F |^ I) and
                                    A12: (F |^ I).y = x by FUNCT_1:def 5;
                 reconsider y as Nat by A11;
                    len(F |^ I) = len F by Def4;
                  then A13: y in dom F by A11,FINSEQ_3:31;
                  then A14: x = (F/.y) |^ @(I/.y) by A12,Def4;
                    now per cases;
                   suppose F/.y = a;
                     then x in gr M by A8,A14,Th6;
                    hence thesis by GROUP_2:88;
                   suppose A15: F/.y <> a;
                       F/.y = F.y & F.y in rng F
                        by A13,FINSEQ_4:def 4,FUNCT_1:def 5;
                     then F/.y in B & not F/.y in {a}
                                             by A9,A15,TARSKI:def 1;
                     then F/.y in M by XBOOLE_0:def 4;
                     then F/.y in gr M by Th38;
                     then x in gr M by A14,Th6;
                    hence thesis by GROUP_2:88;
                  end;
               hence thesis;
              end;
           hence b in gr M by A10,Th21;
          end;
         hence contradiction by A4,GROUP_2:71;
        end;
       then reconsider X as non empty set by A6,A7;
       defpred P[set,set] means
        ex H1,H2 being strict Subgroup of G st
         $1 = H1 & $2 = H2 & H1 is Subgroup of H2;
        A16: now let x be Element of X;
            x in Subgroups G by A5,TARSKI:def 3;
         hence x is strict Subgroup of G by GROUP_3:def 1;
        end;
        A17: for x being Element of X holds P[x,x]
         proof let x be Element of X;
           reconsider H = x as strict Subgroup of G by A16;
              H is Subgroup of H by GROUP_2:63;
          hence thesis;
         end;
        A18: for x,y being Element of X st P[x,y] & P[y,x]
            holds x = y by GROUP_2:64;
        A19: for x,y,z being Element of X st P[x,y] & P[y,z]
            holds P[x,z]
         proof let x,y,z be Element of X;
           given H1,H2 being strict Subgroup of G such that
           A20: x = H1 & y = H2 & H1 is Subgroup of H2;
           given H3,H4 being strict Subgroup of G such that
           A21: y = H3 & z = H4 & H3 is Subgroup of H4;
              H1 is Subgroup of H4 by A20,A21,GROUP_2:65;
          hence thesis by A20,A21;
         end;
        A22: for Y st Y c= X &
              (for x,y being Element of X st x in Y & y in Y holds
                P[x,y] or P[y,x])
              ex y being Element of X st
               for x being Element of X st x in Y holds P[x,y]
         proof let Y;
           assume A23: Y c= X;
           assume A24: for x,y being Element of X
              st x in Y & y in Y holds
                       P[x,y] or P[y,x];
            set C = {D where D is Subset of G :
             ex H being strict Subgroup of G st H in Y & D = carr H};
               now let Z be set;
               assume Z in C;
                then ex D being Subset of G st Z = D &
                 ex H being strict Subgroup of G st H in Y & D = carr H;
              hence Z c= the carrier of G;
             end;
            then reconsider E = union C as Subset of G
            by ZFMISC_1:94;
               now per cases;
              suppose A25: Y = {};
                consider y being Element of X;
               take y;
               let x be Element of X;
                assume x in Y;
               hence P[x,y] by A25;
              suppose A26: Y <> {};
                consider s being Element of Y;
                 A27: s in X by A23,A26,TARSKI:def 3;
                 then reconsider s as strict Subgroup of G by A5,GROUP_3:def 1;
                 A28: carr s in C by A26;
                 then carr s c= E & M c= carr s by A6,A27,ZFMISC_1:92;
                 then A29: M c= E by XBOOLE_1:1;
                   carr s <> {} by GROUP_2:87;
                 then A30: E <> {} by A28,ORDERS_1:91;
                 A31: now let a,b be Element of G;
                   assume that A32: a in E and A33: b in E;
                    consider Z being set such that A34: a in Z and A35: Z in C
                                                               by A32,TARSKI:
def 4;
                    consider D being Subset of G such that
                    A36: Z = D and
                     A37: ex H being strict Subgroup of G
                          st H in Y & D = carr H by A35;
                    consider H1 being Subgroup of G such that
                    A38: H1 in Y & D = carr H1 by A37;
                    consider Z1 being set such that A39: b in Z1 and
                    A40: Z1 in C by A33,TARSKI:def 4;
                    consider B being Subset of G such that
                    A41: Z1 = B and
                   A42: ex H being strict Subgroup of G
                   st H in Y & B = carr H by A40;
                    consider H2 being Subgroup of G such that
                    A43: H2 in Y & B = carr H2 by A42;
                       now per cases by A23,A24,A38,A43;
                      suppose P[H1,H2];
                         then the carrier of H1 c= the carrier of H2
                                                 by GROUP_2:def 5;
                         then carr H1 c= the carrier of H2 by GROUP_2:def 9;
                         then carr H1 c= carr H2 by GROUP_2:def 9;
                         then a * b in carr H2 by A34,A36,A38,A39,A41,A43,
GROUP_2:89;
                       hence a * b in E by A40,A41,A43,TARSKI:def 4;
                      suppose P[H2,H1];
                         then the carrier of H2 c= the carrier of H1
                                                 by GROUP_2:def 5;
                         then carr H2 c= the carrier of H1 by GROUP_2:def 9;
                         then carr H2 c= carr H1 by GROUP_2:def 9;
                         then a * b in carr H1 by A34,A36,A38,A39,A41,A43,
GROUP_2:89;
                       hence a * b in E by A35,A36,A38,TARSKI:def 4;
                     end;
                  hence a * b in E;
                 end;
                   now let a be Element of G;
                   assume a in E;
                    then consider Z being set such that A44: a in Z and
                    A45: Z in C by TARSKI:def 4;
                    consider D being Subset of G such that
                    A46: Z = D and
                    A47: ex H being strict Subgroup of G
                         st H in Y & D = carr H by A45;
                    consider H1 being Subgroup of G such that
                    A48: H1 in Y & D = carr H1 by A47;
                       a" in carr H1 by A44,A46,A48,GROUP_2:90;
                  hence a" in E by A45,A46,A48,TARSKI:def 4;
                 end;
                then consider H being strict Subgroup of G such that
                A49: the carrier of H = E by A30,A31,GROUP_2:61;
                 A50: now assume a in H;
                    then a in E by A49,RLVECT_1:def 1;
                   then consider Z being set such that A51: a in Z and
                   A52: Z in C by TARSKI:def 4;
                   consider D being Subset of G such that
                   A53: Z = D and
                   A54: ex H being strict Subgroup of G
                         st H in Y & D = carr H by A52;
                   consider H1 being strict Subgroup of G such that
                   A55: H1 in Y & D = carr H1 by A54;
                      not a in H1 by A6,A23,A55;
                  hence contradiction by A51,A53,A55,GROUP_2:88;
                 end;
                   the carrier of H = carr H by GROUP_2:def 9;
                then reconsider y = H as Element of X
                by A6,A29,A49,A50;
              take y;
              let x be Element of X;
               assume A56: x in Y;
                   x in Subgroups G by A5,TARSKI:def 3;
                then reconsider K = x as strict Subgroup of G by GROUP_3:def 1;
              take K,H;
              thus x = K & y = H;
                  carr K = the carrier of K by GROUP_2:def 9;
                then the carrier of K in C by A56;
                then the carrier of K c= E by ZFMISC_1:92;
              hence K is Subgroup of H by A49,GROUP_2:66;
             end;
          hence thesis;
         end;
       consider s being Element of X such that
        A57: for y being Element of X st s <> y holds not P[s,y]
                                                from Zorn_Max(A17,A18,A19,A22);
       reconsider H = s as strict Subgroup of G by A16;
          H is maximal
         proof
             not a in H by A6;
          hence the HGrStr of H <> the HGrStr of G by RLVECT_1:def 1;
          let K be strict Subgroup of G;
           assume that A58: K <> the HGrStr of H and
                       A59: H is Subgroup of K and
                       A60: K <> the HGrStr of G;
               the carrier of H = carr H & the carrier of K = carr K &
             the carrier of H c= the carrier of K & M c= carr H
                                     by A6,A59,GROUP_2:def 5,def 9;
             then A61: M c= carr K by XBOOLE_1:1;
               now assume a in K;
               then a in carr K by GROUP_2:88;
               then {a} c= carr K by ZFMISC_1:37;
               then A62: M \/ {a} c= carr K by A61,XBOOLE_1:8;
                 B c= M \/ {a}
                proof let x;
                  assume A63: x in B;
                     now per cases;
                    suppose x = a;
                      then x in {a} by TARSKI:def 1;
                     hence thesis by XBOOLE_0:def 2;
                    suppose x <> a;
                      then not x in {a} by TARSKI:def 1;
                      then x in M by A63,XBOOLE_0:def 4;
                     hence thesis by XBOOLE_0:def 2;
                   end;
                 hence thesis;
                end;
               then B c= carr K by A62,XBOOLE_1:1;
               then gr B is Subgroup of gr carr K by Th41;
               then G is Subgroup of K by A3,Th40;
              hence contradiction by A60,GROUP_2:64;
             end;
           then reconsider v = K as Element of X by A6,A61;
              not P[s,v] by A57,A58;
          hence thesis by A59;
         end;
        then Phi(G) is Subgroup of H by Th54;
        then the carrier of Phi(G) c= the carrier of H by GROUP_2:def 5;
        then x in H & not a in H by A1,A6,RLVECT_1:def 1;
     hence thesis;
    end;
   let x;
    assume x in A;
     then consider a being Element of G such that
     A64: x = a and A65: a is non generating;
        now per cases;
       suppose for H being strict Subgroup of G holds H is not maximal;
         then Phi(G) = G by Def8;
        hence thesis by A64;
       suppose A66: ex H being strict Subgroup of G st H is maximal;
           now let H be strict Subgroup of G;
          assume A67: H is maximal;
             now assume A68: not a in H;
             then A69: gr(carr H \/ {a}) = G by A67,Th48;
             A70: carr H misses {a}
              proof
               thus carr H /\ {a} c= {}
                proof let x;
                  assume x in carr H /\ {a};
                   then x in carr H & x in {a} by XBOOLE_0:def 3;
                   then x in carr H & x = a by TARSKI:def 1;
                 hence thesis by A68,GROUP_2:88;
                end;
               thus {} c= carr H /\ {a} by XBOOLE_1:2;
              end;
               (carr H \/ {a}) \ {a} = carr H \ {a} by XBOOLE_1:40
                                  .= carr H by A70,XBOOLE_1:83;
             then gr((carr H \/ {a}) \ {a}) = H & H <> G by A67,Def7,Th40;
            hence contradiction by A65,A69,Def6;
           end;
          hence a in H;
         end;
         then a in Phi(G) by A66,Th52;
       hence thesis by A64,RLVECT_1:def 1;
      end;
   hence thesis;
  end;

theorem
   for G being strict Group, a being Element of G holds
  a in Phi(G) iff a is non generating
  proof let G be strict Group, a be Element of G;
   thus a in Phi(G) implies a is non generating
    proof assume a in Phi(G);
       then a in the carrier of Phi(G) by RLVECT_1:def 1;
       then a in {b where b is Element of
       G: b is non generating} by Th55;
      then ex b being Element of G
      st a = b & b is non generating;
     hence thesis;
    end;
    assume a is non generating;
     then a in
 {b where b is Element of G : b is non generating};
     then a in the carrier of Phi(G) by Th55;
   hence thesis by RLVECT_1:def 1;
  end;

definition let G,H1,H2;
 func H1 * H2 -> Subset of G equals
  :Def9:  carr H1 * carr H2;
 correctness;
end;

theorem Th57:
 H1 * H2 = carr H1 * carr H2 & H1 * H2 = H1 * carr H2 &
  H1 * H2 = carr H1 * H2
 proof
  thus H1 * H2 = carr H1 * carr H2 by Def9;
  hence thesis by GROUP_2:def 11,def 12;
 end;

theorem
   H * H = carr H
  proof
   thus H * H = carr H * carr H by Def9
             .= carr H by GROUP_2:91;
  end;

theorem
   H1 * H2 * H3 = H1 * (H2 * H3)
  proof
   thus H1 * H2 * H3 = carr H1 * carr H2 * H3 by Def9
                    .= carr H1 * (carr H2 * H3) by GROUP_2:116
                    .= carr H1 * (H2 * H3) by Th57
                    .= H1 * (H2 * H3) by GROUP_2:def 12;
  end;

theorem
   a * H1 * H2 = a * (H1 * H2)
  proof
   thus a * H1 * H2 = a * carr H1 * H2 by GROUP_2:def 13
                   .= a * (carr H1 * H2) by GROUP_3:9
                   .= a * (H1 * H2) by Th57;
  end;

theorem
   H1 * H2 * a = H1 * (H2 * a)
  proof
   thus H1 * H2 * a = H1 * carr H2 * a by Th57
                   .= H1 * (carr H2 * a) by GROUP_3:14
                   .= H1 * (H2 * a) by GROUP_2:def 14;
  end;

theorem
   A * H1 * H2 = A * (H1 * H2)
  proof
   thus A * H1 * H2 = A * (H1 * carr H2) by GROUP_2:119
                   .= A * (H1 * H2) by Th57;
  end;

theorem
   H1 * H2 * A = H1 * (H2 * A)
  proof
   thus H1 * H2 * A = H1 * carr H2 * A by Th57
                   .= H1 * (carr H2 * A) by GROUP_2:118
                   .= H1 * (H2 * A) by GROUP_2:def 12;
  end;

theorem Th64:
 for N1,N2 being strict normal Subgroup of G
 holds N1 * N2 = N2 * N1
  proof let N1,N2 be strict normal Subgroup of G;
     carr N1 * carr N2 = carr N2 * carr N1 by GROUP_3:148;
    then N1 * N2 = carr N2 * carr N1 by Def9;
   hence thesis by Def9;
  end;

theorem Th65:
 G is commutative Group implies H1 * H2 = H2 * H1
  proof assume G is commutative Group;
    then carr H1 * carr H2 = carr H2 * carr H1 by GROUP_2:29;
    then H1 * H2 = carr H2 * carr H1 by Def9;
   hence thesis by Def9;
  end;

definition let G,H1,H2;
 func H1 "\/" H2 -> strict Subgroup of G equals
  :Def10:  gr(carr H1 \/ carr H2);
 correctness;
end;

canceled;

theorem Th67:
 a in H1 "\/" H2 iff
  ex F,I st len F = len I & rng F c= carr H1 \/ carr H2 & a = Product(F |^ I)
 proof
  thus a in H1 "\/" H2 implies
   ex F,I st len F = len I & rng F c= carr H1 \/ carr H2 & a = Product(F |^ I)
    proof assume a in H1 "\/" H2;
      then a in gr(carr H1 \/ carr H2) by Def10;
     hence thesis by Th37;
    end;
   assume
      ex F,I st len F = len I & rng F c= carr H1 \/ carr H2 &
      a = Product(F |^ I);
     then a in gr(carr H1 \/ carr H2) by Th37;
  hence thesis by Def10;
 end;

Lm4: for n being natural number holds n mod 2 = 0 or n mod 2 = 1
 proof 
  let n be natural number;
  assume A1: n mod 2 <> 0;
   2 = 1 + 1 & n mod 2 < 2 by NAT_1:46;
   then n mod 2 <= 1 & n mod 2 >= 1 by A1,NAT_1:38,RLVECT_1:98;
  hence n mod 2 = 1 by AXIOMS:21;
 end;

Lm5: 
 for k, n being Nat holds (k * n) mod k = 0
 proof
  let k, n be Nat;
    now per cases;
    suppose k = 0;
     hence thesis by NAT_1:def 2;
    suppose k <> 0;
      then k * n = k * n + 0 & 0 < k by NAT_1:18;
     hence thesis by NAT_1:def 2;
   end;
  hence thesis;
 end;

Lm6: 
  for k, l being natural number holds k > 1 implies 1 mod k = 1
 proof 
  let k, l be natural number;
  assume A1: k > 1;
     1 = k * 0 + 1;
  hence thesis by A1,NAT_1:def 2;
 end;

Lm7: 
 for k, l, n, m being natural number holds
k mod n = 0 & l = k - m * n implies l mod n = 0
 proof 
  let k, l, n, m be natural number;
  assume that A1: k mod n = 0 and A2: l = k - m * n;
     now per cases;
    suppose n = 0;
     hence thesis by A1,A2;
    suppose n <> 0;
      then consider t being Nat such that
A3:    k = n * t + 0 and A4: 0 < n by A1,NAT_1:def 2;
       A5: l = n * (t - m) + 0 by A2,A3,XCMPLX_1:40;
         now assume t - m < 0;
         then l < n * 0 by A4,A5,REAL_1:70;
        hence contradiction by NAT_1:18;
       end;
       then t - m is Nat by INT_1:16;
    hence thesis by A4,A5,NAT_1:def 2;
   end;
  hence thesis;
 end;

Lm8: n <> 0 & k mod n = 0 & l < n implies k + l mod n = l
 proof assume that A1: n <> 0 and A2: k mod n = 0 and A3: l < n;
   consider t being Nat such that A4: k = n * t + 0 and 0 < n
                                                       by A1,A2,NAT_1:def 2;
  thus thesis by A3,A4,NAT_1:def 2;
 end;

Lm9: k mod n = 0 implies k + l mod n = l mod n
 proof assume that A1: k mod n = 0;
     now per cases;
    suppose
A2:     n = 0;
     hence k + l mod n = 0 by NAT_1:def 2
          .= l mod n by A2,NAT_1:def 2;
    suppose A3: n <> 0;
      then consider m such that A4: k = n * m + 0 & 0 < n by A1,NAT_1:def 2;
      consider t being Nat such that
A5:    l = n * t + (l mod n) & l mod n < n by A3,NAT_1:def 2;
         k + l = n * m + n * t + (l mod n) by A4,A5,XCMPLX_1:1
            .= n * (m + t) + (l mod n) by XCMPLX_1:8;
    hence thesis by A5,NAT_1:def 2;
   end;
  hence thesis;
 end;

Lm10: k <> 0 implies (k * n) div k = n
 proof assume k <> 0;
   then k * n = k * n + 0 & 0 < k by NAT_1:18;
  hence thesis by NAT_1:def 1;
 end;

Lm11: n <> 0 & k mod n = 0 implies
  (k + l) div n = (k div n) + (l div n)
 proof assume that A1:n <> 0 and A2: k mod n = 0;
    A3: 0 <= n by NAT_1:18;
   then A4: k = n * (k div n) + 0 by A1,A2,NAT_1:47;
A5: ex t being Nat st l = n * t + (l mod n) & l mod n < n by A1,NAT_1:def 2;
     l = n * (l div n) + (l mod n) by A1,A3,NAT_1:47;
   then k + l = n * (k div n) + n * (l div n) + (l mod n) by A4,XCMPLX_1:1
        .= n * ((k div n) + (l div n)) + (l mod n) by XCMPLX_1:8;
  hence thesis by A5,NAT_1:def 1;
 end;

theorem
   H1 "\/" H2 = gr(H1 * H2)
  proof set H = gr(carr H1 * carr H2);
    A1: carr H1 * carr H2 = H1 * H2 by Def9;
    A2: H1 "\/" H2 = gr(carr H1 \/ carr H2) by Def10;
       carr H1 \/ carr H2 c= carr H1 * carr H2
     proof let x;
       assume A3: x in carr H1 \/ carr H2;
        then reconsider a = x as Element of G;
           now per cases by A3,XBOOLE_0:def 2;
          suppose A4: x in carr H1;
              1.G in H2 by GROUP_2:55;
            then 1.G in carr H2 & a * 1.G = a by GROUP_1:def 4,GROUP_2:88;
           hence thesis by A4,GROUP_2:12;
          suppose A5: x in carr H2;
              1.G in H1 by GROUP_2:55;
            then 1.G in carr H1 & 1.G * a = a by GROUP_1:def 4,GROUP_2:88;
           hence thesis by A5,GROUP_2:12;
         end;
      hence thesis;
     end;
    then A6: H1 "\/" H2 is Subgroup of H by A2,Th41;
      now let a;
      assume a in H;
       then consider F,I such that A7: len F = len I and
        A8: rng F c= carr H1 * carr H2 and A9: a = Product(F |^ I) by Th37;
          rng(F |^ I) c= carr(H1 "\/" H2)
         proof let x; set f = F |^ I;
           assume x in rng f;
            then consider y such that A10: y in dom f and
                                      A11: f.y = x by FUNCT_1:def 5;
            reconsider y as Nat by A10;
A12:             len f = len F by Def4;
then A13:          y in dom I by A7,A10,FINSEQ_3:31;
             then I.y in rng I & rng I c= INT by FINSEQ_1:def 4,FUNCT_1:def 5;
             then reconsider i = I.y as Integer by INT_1:12;
             A14: y in dom F by A10,A12,FINSEQ_3:31;
               I/.y = I.y & @(I/.y) = I/.y by A13,Def2,FINSEQ_4:def 4;
             then A15: x = (F/.y) |^ i by A11,A14,Def4;
               y in dom F by A10,A12,FINSEQ_3:31;
             then F/.y = F.y & F.y in rng F by FINSEQ_4:def 4,FUNCT_1:def 5;
             then consider b,c such that A16: F/.y = b * c and
             A17: b in carr H1 and A18: c in carr H2 by A8,GROUP_2:12;
               now per cases;
              suppose i >= 0;
                then reconsider n = i as Nat by INT_1:16;
                defpred P[Nat,set] means ($1 mod 2 = 1 implies $2 = b) &
                                      ($1 mod 2 = 0 implies $2 = c);
                 A19: for k,y1,y2 st k in Seg(2 * n) & P[k,y1] & P[k,y2] holds
                     y1 = y2 by Lm4;
                 A20: for k st k in Seg(2 * n) ex x st P[k,x]
                  proof let k;
                    assume k in Seg(2 * n);
                       now per cases by Lm4;
                      suppose A21: k mod 2 = 1;
                        reconsider x = b as set;
                       take x;
                       thus (k mod 2 = 1 implies x = b) &
                            (k mod 2 = 0 implies x = c) by A21;
                      suppose A22: k mod 2 = 0;
                        reconsider x = c as set;
                       take x;
                       thus (k mod 2 = 1 implies x = b) &
                            (k mod 2 = 0 implies x = c) by A22;
                     end;
                   hence thesis;
                  end;
                consider p being FinSequence such that
                 A23: dom p = Seg(2 * n) and
                 A24: for k st k in
 Seg(2 * n) holds P[k,p.k] from SeqEx(A19,A20
);
                 A25: len p = 2 * n by A23,FINSEQ_1:def 3;
                 A26: rng p c= {b,c}
                  proof let x;
                    assume x in rng p;
                     then consider y such that A27: y in dom p and A28: p.y = x
                                                                by FUNCT_1:def
5;
                     reconsider y as Nat by A27;
                        now per cases by Lm4;
                       suppose y mod 2 = 0;
                         then x = c by A23,A24,A27,A28;
                        hence thesis by TARSKI:def 2;
                       suppose y mod 2 = 1;
                         then x = b by A23,A24,A27,A28;
                        hence thesis by TARSKI:def 2;
                      end;
                   hence thesis;
                  end;
                 then rng p c= the carrier of G by XBOOLE_1:1;
                then reconsider p as FinSequence of the carrier of G
                                                           by FINSEQ_1:def 4;
                 defpred Q[Nat] means $1 <= 2 * n & $1 mod 2 = 0 implies
                  for F1 st F1 = p | Seg $1 holds Product(F1) =
(F/.y) |^ ($1 div 2);
                 A29: for k st for l st l < k holds Q[l] holds Q[k]
                  proof let k;
                    assume A30: for l st l < k holds Q[l];
                    assume that A31: k <= 2 * n and A32: k mod 2 = 0;
                   let F1;
                    assume A33: F1 = p | Seg k;
                       now per cases;
                      suppose A34: k = 0;
                        then F1 = <*> the carrier of G by A33,FINSEQ_1:4,
RELAT_1:110;
                        then A35: Product F1 = 1.G by Th11;
                          2 * 0 = 0;
                        then 0 div 2 = 0 by Lm10;
                       hence thesis by A34,A35,GROUP_1:43;
                      suppose k <> 0;
                         then A36: k >= 1 by RLVECT_1:98;
                           k <> 1 by A32,Lm6;
                         then k > 1 by A36,REAL_1:def 5;
                         then k >= 1 + 1 by NAT_1:38;
                         then k - 2 >= 2 - 2 by REAL_1:49;
                        then reconsider m = k - 2 as Nat by INT_1:16;
                         A37: m + 2 = k by XCMPLX_1:27;
                         then A38: m < k by RLVECT_1:102;
                         then A39: m <= 2 * n by A31,AXIOMS:22;
                           1 * 2 = 2;
                         then A40: m mod 2 = 0 by A32,Lm7;
                        reconsider q = p | Seg m
 as FinSequence of the carrier of G by FINSEQ_1:23;
                         A41: Product q = (F/.y) |^ (m div 2)
                           by A30,A38,A39,A40;
A42:                        ex j being Nat st 2 * n = k + j by A31,NAT_1:28;
                           ex o being Nat st 2 * n = m + o by A39,NAT_1:28;
                         then A43: len F1 = k & len q = m
                                                 by A25,A33,A42,FINSEQ_3:59;
                         then A44: len F1 = m + 2 by XCMPLX_1:27
                                  .= len q + len<* b,c *> by A43,FINSEQ_1:61;
                         A45: now let l;
                           assume A46: l in dom q;
                            then 1 <= l & l <= len q & len q <= len F1
                                            by A37,A43,FINSEQ_3:27,RLVECT_1:102
;
                            then 1 <= l & l <= len F1 by AXIOMS:22;
                            then l in dom F1 by FINSEQ_3:27;
                            then F1.l = p.l & q.l = p.l by A33,A46,FUNCT_1:70;
                          hence F1.l = q.l;
                         end;
                           now let l;
                           assume l in dom<* b,c *>;
                            then A47: l in {1,2} by FINSEQ_1:4,FINSEQ_3:29;
                              now per cases by A47,TARSKI:def 2;
                             suppose A48: l = 1;
                               then A49: <* b,c *>.l = b by FINSEQ_1:61;
                                 m + 1 <= k & 1 <= m + 1
                                         by A38,NAT_1:37,38;
                               then A50: m + 1 in dom F1 by A43,FINSEQ_3:27;
                               then A51: F1.(len q + l) = p.(m + 1) by A33,A43,
A48,FUNCT_1:70;
                               A52: m + 1 mod 2 = 1 by A40,Lm8;
                                 dom F1 c= dom p by A33,FUNCT_1:76;
                               hence F1.(len q + l) = <* b,c *>.l by A23,A24,
A49,A50,A51,A52;
                             suppose A53: l = 2;
                               then A54: <* b,c *>.l = c by FINSEQ_1:61;
                                 1 <= m + (1 + 1) by NAT_1:37;
                               then A55: m + 2 in
 dom F1 by A37,A43,FINSEQ_3:27;
                               then A56: F1.(len q + l) = p.(m + 2) by A33,A43,
A53,FUNCT_1:70;
                                 2 * 1 = 2 & 2 * 1 mod 2 = 0 by Lm5;
                               then A57: m + 2 mod 2 = 0 by A40,Lm9;
                                 dom F1 c= dom p by A33,FUNCT_1:76;
                               hence F1.(len q + l) = <* b,c *>.l by A23,A24,
A54,A55,A56,A57;
                            end;
                          hence F1.(len q + l) = <* b,c *>.l;
                         end;
                         then F1 = q ^ <* b,c *> by A44,A45,FINSEQ_3:43;
                         then A58: Product F1 = Product q * Product<* b,c *>
                         by Th8
                                     .= Product q * (F/.y) by A16,Th13
                                     .= (F/.y) |^ ((m div 2) + 1)
                                                         by A41,GROUP_1:49;
                           m div 2*1 + 1 = (m div 2) + (2 div 2) by Lm10
                                         .= k div 2 by A37,A40,Lm11;
                       hence thesis by A58;
                     end;
                   hence thesis;
                  end;
                 A59: for k holds Q[k] from Comp_Ind(A29);
                 A60: 2 * n mod 2 = 0 by Lm5;
                 A61: 2 * n div 2 = n by Lm10;
                   len p = 2 * n by A23,FINSEQ_1:def 3;
                 then p = p | Seg(2 * n) by FINSEQ_3:55;
                 then A62: x = Product(p) by A15,A59,A60,A61;
                   b in carr H1 \/ carr H2 & c in carr H1 \/ carr H2
                                                             by A17,A18,
XBOOLE_0:def 2;
                 then {b,c} c= carr H1 \/ carr H2 by ZFMISC_1:38;
                 then A63: rng p c= carr H1 \/ carr H2 by A26,XBOOLE_1:1;
                   carr H1 \/ carr H2 c=
                  the carrier of gr(carr H1 \/ carr H2) &
                 carr gr(carr H1 \/ carr H2) =
                  the carrier of gr(carr H1 \/ carr H2) by Def5,GROUP_2:def 9;
                 then rng p c= carr gr(carr H1 \/ carr H2)
                                                         by A63,XBOOLE_1:1;
                 then x in gr(carr H1 \/ carr H2) by A62,Th21;
                 then x in H1 "\/" H2 by Def10;
               hence thesis by GROUP_2:88;
              suppose A64: i < 0;
                set n = abs( i );
                defpred P[Nat,set] means ($1 mod 2 = 1 implies $2 = c") &
                                      ($1 mod 2 = 0 implies $2 = b");
                 A65: for k,y1,y2 st k in Seg(2 * n) & P[k,y1] & P[k,y2] holds
                     y1 = y2 by Lm4;
                 A66: for k st k in Seg(2 * n) ex x st P[k,x]
                  proof let k;
                    assume k in Seg(2 * n);
                       now per cases by Lm4;
                      suppose A67: k mod 2 = 1;
                        reconsider x = c" as set;
                       take x;
                       thus (k mod 2 = 1 implies x = c") &
                            (k mod 2 = 0 implies x = b") by A67;
                      suppose A68: k mod 2 = 0;
                        reconsider x = b" as set;
                       take x;
                       thus (k mod 2 = 1 implies x = c") &
                            (k mod 2 = 0 implies x = b") by A68;
                     end;
                   hence thesis;
                  end;
                consider p being FinSequence such that
                 A69: dom p = Seg(2 * n) and
                 A70: for k st k in
 Seg(2 * n) holds P[k,p.k] from SeqEx(A65,A66);
                 A71: len p = 2 * n by A69,FINSEQ_1:def 3;
                 A72: rng p c= {b",c"}
                  proof let x;
                    assume x in rng p;
                     then consider y such that A73: y in dom p and A74: p.y = x
                                                           by FUNCT_1:def 5;
                     reconsider y as Nat by A73;
                        now per cases by Lm4;
                       suppose y mod 2 = 0;
                         then x = b" by A69,A70,A73,A74;
                        hence thesis by TARSKI:def 2;
                       suppose y mod 2 = 1;
                         then x = c" by A69,A70,A73,A74;
                        hence thesis by TARSKI:def 2;
                      end;
                   hence thesis;
                  end;
                 then rng p c= the carrier of G by XBOOLE_1:1;
                then reconsider p as FinSequence of the carrier of G
                                                     by FINSEQ_1:def 4;
                 defpred Q[Nat] means $1 <= 2 * n & $1 mod 2 = 0 implies
                  for F1 st F1 = p | Seg $1 holds
                   Product(F1) = ((F/.y) |^ ($1 div 2))";
                 A75: for k st for l st l < k holds Q[l] holds Q[k]
                  proof let k;
                    assume A76: for l st l < k holds Q[l];
                    assume that A77: k <= 2 * n and A78: k mod 2 = 0;
                   let F1;
                    assume A79: F1 = p | Seg k;
                       now per cases;
                      suppose A80: k = 0;
                        then F1 = <*> the carrier of G by A79,FINSEQ_1:4,
RELAT_1:110;
                        then A81: Product F1 = 1.G by Th11;
                          2 * 0 = 0;
                        then 0 div 2 = 0 by Lm10;
                        then (F/.y) |^ (k div 2) = 1.G by A80,GROUP_1:43;
                       hence thesis by A81,GROUP_1:16;
                      suppose k <> 0;
                         then A82: k >= 1 by RLVECT_1:98;
                           k <> 1 by A78,Lm6;
                         then k > 1 by A82,REAL_1:def 5;
                         then k >= 1 + 1 by NAT_1:38;
                         then k - 2 >= 2 - 2 by REAL_1:49;
                        then reconsider m = k - 2 as Nat by INT_1:16;
                         A83: m + 2 = k by XCMPLX_1:27;
                         then A84: m < k by RLVECT_1:102;
                         then A85: m <= 2 * n by A77,AXIOMS:22;
                           1 * 2 = 2;
                         then A86: m mod 2 = 0 by A78,Lm7;
                        reconsider q = p | Seg m
 as FinSequence of the carrier of G by FINSEQ_1:23;
                   A87: Product q = ((F/.y) |^ (m div 2))" by A76,A84,A85,A86;
 A88:                        ex j being Nat st 2 * n = k + j by A77,NAT_1:28;
                           ex o being Nat st 2 * n = m + o by A85,NAT_1:28;
                         then A89: len F1 = k & len q = m
                                                 by A71,A79,A88,FINSEQ_3:59;
                         then A90: len F1 = m + 2 by XCMPLX_1:27
                                  .= len q + len<* c",b" *> by A89,FINSEQ_1:61;
                         A91: now let l;
                           assume A92: l in dom q;
                            then 1 <= l & l <= len q & len q <= len F1
                                            by A83,A89,FINSEQ_3:27,RLVECT_1:102
;
                            then 1 <= l & l <= len F1 by AXIOMS:22;
                            then l in dom F1 by FINSEQ_3:27;
                            then F1.l = p.l & q.l = p.l by A79,A92,FUNCT_1:70;
                          hence F1.l = q.l;
                         end;
                           now let l;
                           assume l in dom<* c",b" *>;
                            then A93: l in {1,2} by FINSEQ_1:4,FINSEQ_3:29;
                              now per cases by A93,TARSKI:def 2;
                             suppose A94: l = 1;
                               then A95: <* c",b" *>.l = c" by FINSEQ_1:61;
                                 m + 1 <= k & 1 <= m + 1
                                         by A84,NAT_1:37,38;
                               then A96: m + 1 in dom F1 by A89,FINSEQ_3:27;
                               then A97: F1.(len q + l) = p.(m + 1) by A79,A89,
A94,FUNCT_1:70;
                               A98: m + 1 mod 2 = 1 by A86,Lm8;
                                 dom F1 c= dom p by A79,FUNCT_1:76;

hence F1.(len q + l) = <* c",b" *>.l by A69,A70,A95,A96,A97,A98;
                             suppose A99: l = 2;
                               then A100: <* c",b" *>.l = b" by FINSEQ_1:61;
                                 1 <= m + (1 + 1) by NAT_1:37;
                               then A101: m + 2 in
 dom F1 by A83,A89,FINSEQ_3:27
;
                               then A102: F1.(len q + l) = p.(m + 2) by A79,A89
,A99,FUNCT_1:70;
                                 2 * 1 = 2 & 2 * 1 mod 2 = 0 by Lm5;
                               then A103: m + 2 mod 2 = 0 by A86,Lm9;
                                 dom F1 c= dom p by A79,FUNCT_1:76;
hence F1.(len q + l) = <* c",b" *>.l by A69,A70,A100,A101,A102,A103;
                            end;
                          hence F1.(len q + l) = <* c",b" *>.l;
                         end;
                         then F1 = q ^ <* c",b" *> by A90,A91,FINSEQ_3:43;
                         then A104: Product F1 = Product q *
                          Product<* c",b" *> by Th8
                                     .= Product q * (c" * b") by Th13
                                     .= Product q * (F/.y)"
                                       by A16,GROUP_1:25
                                     .= ((F/.y) * ((F/.y) |^ (m div 2)))"
                                                           by A87,GROUP_1:25
                                     .= ((F/.y) |^ ((m div 2) + 1))"
                                                         by GROUP_1:49;
                           m div 2*1 + 1 = (m div 2) + (2 div 2) by Lm10
                                         .= k div 2 by A83,A86,Lm11;
                       hence thesis by A104;
                     end;
                   hence thesis;
                  end;
                 A105: for k holds Q[k] from Comp_Ind(A75);
                 A106: 2 * n mod 2 = 0 by Lm5;
                 A107: 2 * n div 2 = n by Lm10;
                   len p = 2 * n by A69,FINSEQ_1:def 3;
                 then A108: p = p | Seg(2 * n) by FINSEQ_3:55;
                   x = ((F/.y) |^ n)" by A15,A64,GROUP_1:56;
                 then A109: x = Product(p) by A105,A106,A107,A108;
                   b" in carr H1 & c" in carr H2 by A17,A18,GROUP_2:90;
                 then b" in carr H1 \/ carr H2 &
                      c" in carr H1 \/ carr H2 by XBOOLE_0:def 2;
                 then {b",c"} c= carr H1 \/ carr H2 by ZFMISC_1:38;
                 then A110: rng p c= carr H1 \/ carr H2 by A72,XBOOLE_1:1;
                   carr H1 \/ carr H2 c=
                  the carrier of gr(carr H1 \/ carr H2) &
                 carr gr(carr H1 \/ carr H2) =
                  the carrier of gr(carr H1 \/ carr H2) by Def5,GROUP_2:def 9;
                 then rng p c= carr gr(carr H1 \/ carr H2)
                                                         by A110,XBOOLE_1:1;
                 then x in gr(carr H1 \/ carr H2) by A109,Th21;
                 then x in H1 "\/" H2 by Def10;
               hence thesis by GROUP_2:88;
             end;
          hence thesis;
         end;
     hence a in H1 "\/" H2 by A9,Th21;
    end;
    then H is Subgroup of H1 "\/" H2 by GROUP_2:67;
   hence gr(H1 * H2) = H1 "\/" H2 by A1,A6,GROUP_2:64;
  end;

theorem Th69:
 H1 * H2 = H2 * H1 implies
  the carrier of H1 "\/" H2 = H1 * H2
 proof assume H1 * H2 = H2 * H1;
   then carr H1 * carr H2 = H2 * H1 by Def9;
   then carr H1 * carr H2 = carr H2 * carr H1 by Def9;
   then consider H being strict Subgroup of G such that
    A1: the carrier of H = carr H1 * carr H2 by GROUP_2:93;
    A2: H1 "\/" H2 = gr(carr H1 \/ carr H2) by Def10;
       carr H1 \/ carr H2 c= carr H1 * carr H2
     proof let x;
       assume A3: x in carr H1 \/ carr H2;
        then reconsider a = x as Element of G;
           now per cases by A3,XBOOLE_0:def 2;
          suppose A4: x in carr H1;
              1.G in H2 by GROUP_2:55;
            then 1.G in carr H2 & a * 1.G = a by GROUP_1:def 4,GROUP_2:88;
           hence thesis by A4,GROUP_2:12;
          suppose A5: x in carr H2;
              1.G in H1 by GROUP_2:55;
            then 1.G in carr H1 & 1.G * a = a by GROUP_1:def 4,GROUP_2:88;
           hence thesis by A5,GROUP_2:12;
         end;
      hence thesis;
     end;
    then A6: H1 "\/" H2 is Subgroup of H by A1,A2,Def5;
      now let a;
      assume a in H;
        then a in carr H1 * carr H2 by A1,RLVECT_1:def 1;
       then consider b,c such that A7: a = b * c and
        A8: b in carr H1 & c in carr H2 by GROUP_2:12;
       reconsider p = 1 as Integer;
        A9: len<* b,c *> = 2 & len<* @p,@p *> = 2 by FINSEQ_1:61;
        A10: rng<* b,c *> = {b,c} by FINSEQ_2:147;
          b in carr H1 \/ carr H2 & c in carr H1 \/ carr H2 by A8,XBOOLE_0:def
2
;
        then A11: {b,c} c= carr H1 \/ carr H2 by ZFMISC_1:38;
          a = Product<* b *> * c by A7,Th12
         .= Product<* b *> * Product<* c *> by Th12
         .= Product(<* b *> ^ <* c *>) by Th8
         .= Product<* b,c *> by FINSEQ_1:def 9
         .= Product<* b |^ p, c *> by GROUP_1:44
         .= Product<* b |^ p, c |^ p *> by GROUP_1:44
         .= Product(<* b,c *> |^ <* @p,@p *>) by Th29;
        then a in gr(carr H1 \/ carr H2) by A9,A10,A11,Th37;
     hence a in H1 "\/" H2 by Def10;
    end;
    then H is Subgroup of H1 "\/" H2 by GROUP_2:67;
    then H = H1 "\/" H2 & carr H1 * carr H2 = H1 * H2 by A6,Def9,GROUP_2:64;
  hence thesis by A1;
 end;

theorem
   G is commutative Group implies the carrier of H1 "\/" H2 = H1 * H2
  proof assume G is commutative Group;
    then H1 * H2 = H2 * H1 by Th65;
   hence thesis by Th69;
  end;

theorem Th71:
 for N1,N2 being strict normal Subgroup of G
 holds the carrier of N1 "\/" N2 = N1 * N2
  proof let N1,N2 be strict normal Subgroup of G;
      N1 * N2 = N2 * N1 by Th64;
   hence thesis by Th69;
  end;

theorem
   for N1,N2 being strict normal Subgroup of G
  holds N1 "\/" N2 is normal Subgroup of G
  proof let N1,N2 be strict normal Subgroup of G;
    consider N being strict normal Subgroup of G such that
    A1: the carrier of N = carr N1 * carr N2 by GROUP_3:149;
      the carrier of N1 "\/" N2 = N1 * N2 & N1 * N2 = carr N1 * carr N2
                                                                  by Th57,Th71;
   hence thesis by A1,GROUP_2:68;
  end;

theorem Th73:
 for H being strict Subgroup of G holds H "\/" H = H
  proof let H be strict Subgroup of G;
   thus H "\/" H = gr(carr H \/ carr H) by Def10
              .= H by Th40;
  end;

theorem Th74:
 H1 "\/" H2 = H2 "\/" H1
  proof
   thus H1 "\/" H2 = gr(carr H2 \/ carr H1) by Def10
                .= H2 "\/" H1 by Def10;
  end;

Lm12: H1 is Subgroup of H1 "\/" H2
 proof carr H1 c= carr H1 \/ carr H2 &
       carr H1 \/ carr H2 c= the carrier of gr(carr H1 \/ carr H2) &
       H1 "\/" H2 = gr(carr H1 \/ carr H2) &
       the carrier of H1 = carr H1 by Def5,Def10,GROUP_2:def 9,XBOOLE_1:7;
   then the carrier of H1 c= the carrier of H1 "\/" H2 by XBOOLE_1:1;
  hence thesis by GROUP_2:66;
 end;

Lm13: H1 "\/" H2 "\/" H3 is Subgroup of H1 "\/" (H2 "\/" H3)
 proof
    now let a;
    assume a in H1 "\/" H2 "\/" H3;
     then consider F,I such that A1: len F = len I and
                                 A2: rng F c= carr(H1 "\/" H2) \/ carr H3 and
                                 A3: a = Product(F |^ I) by Th67;
        rng F c= carr gr(carr H1 \/ carr(H2 "\/" H3))
       proof let x;
         assume
A4:       x in rng F;
            now per cases by A2,A4,XBOOLE_0:def 2;
           suppose A5: x in carr(H1 "\/" H2);
              then A6: x in H1 "\/" H2 by GROUP_2:88;
             reconsider b = x as Element of G by A5;
             consider F1,I1 such that A7: len F1 = len I1 and
              A8: rng F1 c= carr H1 \/ carr H2 and
              A9: b = Product(F1 |^ I1) by A6,Th67;
                H2 is Subgroup of H2 "\/" H3 by Lm12;
              then the carrier of H2 c= the carrier of H2 "\/" H3 &
                   the carrier of H2 = carr H2 &
                   the carrier of H3 = carr H3 &
                   H2 "\/" H3 = gr(carr H2 \/ carr H3)
                                   by Def10,GROUP_2:def 5,def 9;
              then carr H2 c= carr(H2 "\/" H3) by GROUP_2:def 9;
              then carr H1 \/ carr H2 c= carr H1 \/ carr(H2 "\/" H3)
                                                                 by XBOOLE_1:9;
              then rng F1 c= carr H1 \/ carr(H2 "\/" H3) by A8,XBOOLE_1:1;
              then b in H1 "\/" (H2 "\/" H3) by A7,A9,Th67;
              then x in gr(carr H1 \/ carr(H2 "\/" H3)) by Def10;
            hence thesis by GROUP_2:88;
           suppose x in carr H3;
             then x in H3 & H3 is Subgroup of H3 "\/" H2 by Lm12,GROUP_2:88;
             then x in H3 "\/" H2 by GROUP_2:49;
             then x in H2 "\/" H3 by Th74;
             then x in carr(H2 "\/" H3) by GROUP_2:88;
             then x in carr H1 \/ carr(H2 "\/" H3) &
                  carr H1 \/ carr(H2 "\/" H3)
                   c= the carrier of gr(carr H1 \/ carr(H2 "\/" H3))
                                                         by Def5,XBOOLE_0:def 2
;
             then x in the carrier of gr(carr H1 \/ carr(H2 "\/" H3));
            hence thesis by GROUP_2:def 9;
          end;
        hence thesis;
       end;
     then a in gr carr gr(carr H1 \/ carr(H2 "\/" H3)) by A1,A3,Th37;
     then a in gr(carr H1 \/ carr(H2 "\/" H3)) by Th40;
    hence a in H1 "\/" (H2 "\/" H3) by Def10;
   end;
  hence thesis by GROUP_2:67;
 end;

theorem Th75:
 H1 "\/" H2 "\/" H3 = H1 "\/" (H2 "\/" H3)
  proof A1: H1 "\/" H2 "\/" H3 is Subgroup of H1 "\/" (H2 "\/" H3) by Lm13;
      H2 "\/" H3 "\/" H1 is Subgroup of H2 "\/" (H3 "\/" H1) by Lm13;
    then H2 "\/" H3 "\/" H1 is Subgroup of H3 "\/" H1 "\/" H2 &
         H3 "\/" H1 "\/" H2 is Subgroup of H3 "\/" (H1 "\/" H2) by Lm13,Th74;
    then H2 "\/" H3 "\/" H1 is Subgroup of H3 "\/" (H1 "\/" H2) by GROUP_2:65;
    then H1 "\/" (H2 "\/" H3) is Subgroup of H3 "\/" (H1 "\/" H2) by Th74;
    then H1 "\/" (H2 "\/" H3) is Subgroup of H1 "\/" H2 "\/" H3 by Th74;
   hence thesis by A1,GROUP_2:64;
  end;

theorem
   for H being strict Subgroup of G holds
 (1).G "\/" H = H & H "\/" (1).G = H
  proof let H be strict Subgroup of G;
    A1: carr(1).G = the carrier of (1).G by GROUP_2:def 9
                       .= {1.G} by GROUP_2:def 7;
      1.G in H by GROUP_2:55;
    then 1.G in carr H by GROUP_2:88;
    then {1.G} c= carr H by ZFMISC_1:37;
    then A2: {1.G} \/ carr H = carr H by XBOOLE_1:12;
   thus (1).G "\/" H = gr(carr(1).G \/ carr H) by Def10
                  .= H by A1,A2,Th40;
   hence thesis by Th74;
  end;

theorem Th77:
 (Omega).G "\/" H = (Omega).G & H "\/" (Omega).G = (Omega).G
  proof
    A1: [#] the carrier of G = the carrier of the HGrStr of G by SUBSET_1:def 4
                         .= the carrier of (Omega).G by GROUP_2:def 8;
    A2: carr (Omega).G = the carrier of (Omega).G by GROUP_2:def 9;
       (the carrier of (Omega).
G) \/ carr H = [#] the carrier of G by A1,SUBSET_1:28;
   hence (Omega).G "\/" H = gr carr (Omega).G by A1,A2,Def10
                  .= (Omega).G by Th40;
   hence thesis by Th74;
  end;

theorem Th78:
 H1 is Subgroup of H1 "\/" H2 & H2 is Subgroup of H1 "\/" H2
  proof H1 "\/" H2 = H2 "\/" H1 by Th74;
   hence thesis by Lm12;
  end;

theorem Th79:
 for H2 being strict Subgroup of G holds
 H1 is Subgroup of H2 iff H1 "\/" H2 = H2
  proof let H2 be strict Subgroup of G;
   thus H1 is Subgroup of H2 implies H1 "\/" H2 = H2
    proof assume H1 is Subgroup of H2;
      then A1: the carrier of H1 c= the carrier of H2 &
              the carrier of H1 = carr H1 & carr H2 = the carrier of H2
                                                      by GROUP_2:def 5,def 9;
     thus H1 "\/" H2 = gr(carr H1 \/ carr H2) by Def10
                  .= gr carr H2 by A1,XBOOLE_1:12
                  .= H2 by Th40;
    end;
   thus thesis by Th78;
  end;

theorem
   H1 is Subgroup of H2 implies H1 is Subgroup of H2 "\/" H3
  proof H2 is Subgroup of H2 "\/" H3 by Th78;
   hence thesis by GROUP_2:65;
  end;

theorem
   for H3 being strict Subgroup of G holds
 H1 is Subgroup of H3 & H2 is Subgroup of H3 implies H1 "\/"
 H2 is Subgroup of H3
  proof let H3 be strict Subgroup of G;
   assume that A1: H1 is Subgroup of H3 and A2: H2 is Subgroup of H3;
      now let a;
      assume a in H1 "\/" H2;
       then consider F,I such that A3: len F = len I &
        rng F c= carr H1 \/ carr H2 & a = Product(F |^ I) by Th67;
          the carrier of H1 c= the carrier of H3 &
        the carrier of H2 c= the carrier of H3 &
        the carrier of H1 = carr H1 & the carrier of H2 = carr H2 &
        the carrier of H3 = carr H3 by A1,A2,GROUP_2:def 5,def 9;
        then carr H1 \/ carr H2 c= carr H3 by XBOOLE_1:8;
        then rng F c= carr H3 by A3,XBOOLE_1:1;
        then a in gr carr H3 by A3,Th37;
     hence a in H3 by Th40;
    end;
   hence thesis by GROUP_2:67;
  end;

theorem
   for H3,H2 being strict Subgroup of G holds
 H1 is Subgroup of H2 implies H1 "\/" H3 is Subgroup of H2 "\/" H3
  proof let H3,H2 be strict Subgroup of G;
   assume A1: H1 is Subgroup of H2;
      (H1 "\/" H3) "\/" (H2 "\/" H3) = H1 "\/" H3 "\/" H2 "\/" H3 by Th75
                            .= H1 "\/" (H3 "\/" H2) "\/" H3 by Th75
                            .= H1 "\/" (H2 "\/" H3) "\/" H3 by Th74
                            .= H1 "\/" H2 "\/" H3 "\/" H3 by Th75
                            .= H2 "\/" H3 "\/" H3 by A1,Th79
                            .= H2 "\/" (H3 "\/" H3) by Th75
                            .= H2 "\/" H3 by Th73;
   hence thesis by Th79;
  end;

theorem
   H1 /\ H2 is Subgroup of H1 "\/" H2
  proof H1 /\ H2 is Subgroup of H1 & H1 is Subgroup of H1 "\/" H2
                                                  by Th78,GROUP_2:106;
   hence thesis by GROUP_2:65;
  end;

theorem Th84:
 for H2 being strict Subgroup of G holds (H1 /\ H2) "\/" H2 = H2
  proof let H2 be strict Subgroup of G;
      H1 /\ H2 is Subgroup of H2 by GROUP_2:106;
   hence thesis by Th79;
  end;

theorem Th85:
 for H1 being strict Subgroup of G holds H1 /\ (H1 "\/" H2) = H1
  proof let H1 be strict Subgroup of G;
      H1 is Subgroup of H1 "\/" H2 by Th78;
   hence thesis by GROUP_2:107;
  end;

theorem
   for H1,H2 being strict Subgroup of G holds H1 "\/" H2 = H2 iff H1 /\ H2 = H1
  proof let H1,H2 be strict Subgroup of G;
     (H1 "\/" H2 = H2 iff H1 is Subgroup of H2) &
        (H1 /\ H2 = H1 iff H1 is Subgroup of H2) by Th79,GROUP_2:107;
   hence thesis;
  end;

reserve S1,S2 for Element of Subgroups G;

definition let G;
 func SubJoin G -> BinOp of Subgroups G means
  :Def11: for S1,S2,H1,H2 st S1 = H1 & S2 = H2 holds it.(S1,S2) = H1 "\/" H2;
 existence
  proof
    defpred P[set,set,set] means
      for H1,H2 st $1 = H1 & $2 = H2 holds $3 = H1 "\/" H2;
    A1: for S1,S2 ex B being Element of Subgroups G st P[S1,S2,B]
     proof let S1,S2;
       reconsider H1 = S1, H2 = S2 as Subgroup of G by GROUP_3:def 1;
       reconsider C = H1 "\/" H2 as Element of Subgroups(G)
       by GROUP_3:def 1;
      take C;
      thus thesis;
     end;
   ex o being BinOp of Subgroups G st
    for a,b being Element of Subgroups G holds P[a,b,o.(a,b)]
      from BinOpEx(A1);
   hence thesis;
  end;
 uniqueness
  proof let o1,o2 be BinOp of Subgroups(G);
    assume A2: for S1,S2,H1,H2 st S1 = H1 & S2 = H2 holds o1.(S1,S2) = H1 "\/"
H2;
    assume A3: for S1,S2,H1,H2 st S1 = H1 & S2 = H2 holds o2.(S1,S2) = H1 "\/"
H2;
       now let x,y be set;
       assume A4: x in Subgroups(G) & y in Subgroups(G);
        then reconsider A = x, B = y as Element of Subgroups(G);
        reconsider H1 = x, H2 = y as Subgroup of G by A4,GROUP_3:def 1;
           o1.(A,B) = H1 "\/" H2 & o2.(A,B) = H1 "\/" H2 by A2,A3;
         then o1.(x,y) = o2.(x,y) & o1.[x,y] = o1.(x,y) & o2.[x,y] = o2.(x,y)
                                                    by BINOP_1:def 1;
      hence o1.[x,y] = o2.[x,y];
     end;
   hence thesis by FUNCT_2:118;
  end;
end;

definition let G;
 func SubMeet G -> BinOp of Subgroups G means
  :Def12: for S1,S2,H1,H2 st S1 = H1 & S2 = H2 holds it.(S1,S2) = H1 /\ H2;
 existence
  proof
    defpred P[set,set,set] means
      for H1,H2 st $1 = H1 & $2 = H2 holds $3 = H1 /\ H2;
    A1: for S1,S2 ex B being Element of Subgroups G st P[S1,S2,B]
     proof let S1,S2;
       reconsider H1 = S1, H2 = S2 as Subgroup of G by GROUP_3:def 1;
       reconsider C = H1 /\ H2 as Element of Subgroups(G)
       by GROUP_3:def 1;
      take C;
      thus thesis;
     end;
   ex o being BinOp of Subgroups G st
    for a,b being Element of Subgroups G holds P[a,b,o.(a,b)]
      from BinOpEx(A1);
   hence thesis;
  end;
 uniqueness
  proof let o1,o2 be BinOp of Subgroups(G);
    assume A2: for S1,S2,H1,H2 st S1 = H1 & S2 = H2 holds o1.(S1,S2) = H1 /\
 H2;
    assume A3: for S1,S2,H1,H2 st S1 = H1 & S2 = H2 holds o2.(S1,S2) = H1 /\
 H2;
       now let x,y be set;
       assume A4: x in Subgroups(G) & y in Subgroups(G);
        then reconsider A = x, B = y as Element of Subgroups(G);
        reconsider H1 = x, H2 = y as Subgroup of G by A4,GROUP_3:def 1;
           o1.(A,B) = H1 /\ H2 & o2.(A,B) = H1 /\ H2 by A2,A3;
         then o1.(x,y) = o2.(x,y) & o1.[x,y] = o1.(x,y) & o2.[x,y] = o2.(x,y)
                                                         by BINOP_1:def 1;
      hence o1.[x,y] = o2.[x,y];
     end;
   hence thesis by FUNCT_2:118;
  end;
end;

Lm14: for G being Group holds
    LattStr (# Subgroups G, SubJoin G, SubMeet G #) is Lattice &
    LattStr (# Subgroups G, SubJoin G, SubMeet G #) is 0_Lattice &
    LattStr (# Subgroups G, SubJoin G, SubMeet G #) is 1_Lattice
 proof let G be Group;
  set L = LattStr (# Subgroups G, SubJoin G, SubMeet G #);
   A1: now let A,B be Element of L;
    let H1,H2 be Subgroup of G;
     assume A2: A = H1 & B = H2;
      reconsider A'= A, B'= B as Element of Subgroups G;
    thus A "/\" B = SubMeet(G).(A',B') by LATTICES:def 2
               .= H1 /\ H2 by A2,Def12;
   end;
   A3: now let A,B be Element of L;
    let H1,H2 be Subgroup of G;
     assume A4: A = H1 & B = H2;
      reconsider A'= A, B'= B as Element of Subgroups G;
    thus A "\/" B = SubJoin(G).(A',B') by LATTICES:def 1
               .= H1 "\/" H2 by A4,Def11;
   end;
   now let A,B,C be Element of L;
     reconsider H1 = A, H2 = B, H3 = C as strict Subgroup of G
      by GROUP_3:def 1;
    thus A "\/" B = H1 "\/" H2 by A3
               .= H2 "\/" H1 by Th74
               .= B "\/" A by A3;
     A5: H1 "\/" H2 = A "\/" B & H2 "\/" H3 = B "\/" C by A3;
    hence A "\/" B "\/" C = H1 "\/" H2 "\/" H3 by A3
                    .= H1 "\/" (H2 "\/" H3) by Th75
                    .= A "\/" (B "\/" C) by A3,A5;
     A6: H1 /\ H2 = A "/\" B by A1;
    hence (A "/\" B) "\/" B = (H1 /\ H2) "\/" H2 by A3
                       .= B by Th84;
    thus A "/\" B = H2 /\ H1 by A1
               .= B "/\" A by A1;
     A7: H2 /\ H3 = B "/\" C by A1;
    thus A "/\" B "/\" C = H1 /\ H2 /\ H3 by A1,A6
                    .= H1 /\ (H2 /\ H3) by GROUP_2:102
                    .= A "/\" (B "/\" C) by A1,A7;
    thus A "/\" (A "\/" B) = H1 /\ (H1 "\/" H2) by A1,A5
                      .= A by Th85;
   end;
  then A8: L is join-commutative join-associative meet-absorbing
          meet-commutative meet-associative join-absorbing
  by LATTICES:def 4,def 5,def 6,def 7,def 8,def 9;
  hence L is Lattice by LATTICES:def 10;
   reconsider L as Lattice by A8,LATTICES:def 10;
   reconsider E = (1).G as Element of L by GROUP_3:def 1;
       now let A be Element of L;
      reconsider H = A as Subgroup of G by GROUP_3:def 1;
     thus E "/\" A = (1).G /\ H by A1
                .= E by GROUP_2:103;
     hence A "/\" E = E;
    end;
  hence LattStr (# Subgroups G, SubJoin G, SubMeet G #) is 0_Lattice
                                                        by LATTICES:def 13;
   reconsider F = (Omega).G as Element of L by GROUP_3:def 1;
       now let A be Element of L;
      reconsider H = A as Subgroup of G by GROUP_3:def 1;
     thus F "\/" A = (Omega).G "\/" H by A3
                .= F by Th77;
     hence A "\/" F = F;
    end;
  hence LattStr (# Subgroups G, SubJoin G, SubMeet G #) is 1_Lattice
                                                           by LATTICES:def 14;
 end;

definition let G be Group;
 func lattice G -> strict Lattice equals
  :Def13:  LattStr (# Subgroups G, SubJoin G, SubMeet G #);
 coherence by Lm14;
end;

canceled 5;

theorem Th92:
 for G being Group holds
 the carrier of lattice G = Subgroups G
  proof let G be Group;
     lattice G = LattStr (# Subgroups G, SubJoin G, SubMeet G #) by Def13;
   hence thesis;
  end;

theorem Th93:
 for G being Group holds
 the L_join of lattice G = SubJoin G
  proof let G be Group;
      lattice G = LattStr (# Subgroups G, SubJoin G, SubMeet G #) by Def13;
   hence thesis;
  end;

theorem Th94:
 for G being Group holds
 the L_meet of lattice G = SubMeet G
  proof let G be Group;
      lattice G = LattStr (# Subgroups G, SubJoin G, SubMeet G #) by Def13;
   hence thesis;
  end;

definition let G be Group;
  cluster lattice G -> lower-bounded upper-bounded;
  coherence
  proof
A1: lattice G = LattStr (# Subgroups G, SubJoin G, SubMeet G #) by Def13;
   hence lattice G is lower-bounded by Lm14;
   thus lattice G is upper-bounded by A1,Lm14;
  end;
end;

canceled 3;

theorem
   for G being Group holds Bottom lattice G = (1).G
  proof let G be Group;
   A1: the carrier of lattice G = Subgroups G by Th92;
     set L = lattice G;
    reconsider E = (1).G as Element of L by A1,GROUP_3:def 1;
        now let A be Element of L;
       reconsider H = A as Subgroup of G by A1,GROUP_3:def 1;
      thus A "/\" E = (the L_meet of lattice G).(A,E) by LATTICES:def 2
                 .= SubMeet(G).(A,E) by Th94
                 .= H /\ (1).G by A1,Def12
                 .= E by GROUP_2:103;
     end;
   hence thesis by RLSUB_2:84;
  end;

theorem
   for G being Group holds Top lattice G = (Omega).G
  proof let G be Group;
    A1: the carrier of lattice G = Subgroups G by Th92;
     set L = lattice G;
    reconsider E = (Omega).
G as Element of L by A1,GROUP_3:def 1;
        now let A be Element of L;
       reconsider H = A as Subgroup of G by A1,GROUP_3:def 1;
      thus A "\/" E = (the L_join of lattice G).(A,E) by LATTICES:def 1
                 .= SubJoin(G).(A,E) by Th93
                 .= H "\/" (Omega).G by A1,Def11
                 .= E by Th77;
     end;
   hence thesis by RLSUB_2:85;
  end;

::
::  Auxiliary theorems.
::

 reserve k, l, m, n for natural number;

theorem
   n mod 2 = 0 or n mod 2 = 1 by Lm4;

theorem
  for k, n being Nat holds (k * n) mod k = 0 by Lm5;

theorem
   k > 1 implies 1 mod k = 1 by Lm6;

theorem
   k mod n = 0 & l = k - m * n implies l mod n = 0 by Lm7;

 reserve k, n, l, m for Nat;

theorem
    n <> 0 & k mod n = 0 & l < n implies k + l mod n = l by Lm8;

theorem
   k mod n = 0 implies k + l mod n = l mod n by Lm9;

theorem
   n <> 0 & k mod n = 0 implies
  (k + l) div n = (k div n) + (l div n) by Lm11;

theorem
   k <> 0 implies (k * n) div k = n by Lm10;

Back to top