group_18.miz



    begin

    definition

      let G be finite Group;

      :: GROUP_18:def1

      func Ordset G -> Subset of NAT equals the set of all ( ord a) where a be Element of G;

      coherence

      proof

        set IT = the set of all ( ord a) where a be Element of G;

        IT c= NAT

        proof

          let a be object;

          assume a in IT;

          then

          consider n be Element of G such that

           A1: a = ( ord n);

          thus thesis by A1;

        end;

        hence thesis;

      end;

    end

    registration

      let G be finite Group;

      cluster ( Ordset G) -> finite non empty;

      coherence

      proof

        deffunc F( Element of G) = ( ord $1);

        

         GG: the carrier of G is finite;

        set A = { F(g) where g be Element of G : g in the carrier of G };

        

         T1: A = ( Ordset G)

        proof

          

           Y1: A c= ( Ordset G)

          proof

            let x be object;

            assume x in A;

            then

            consider g be Element of G such that

             Y2: x = F(g) & g in the carrier of G;

            thus thesis by Y2;

          end;

          ( Ordset G) c= A

          proof

            let x be object;

            assume x in ( Ordset G);

            then

            consider g be Element of G such that

             Y2: x = F(g);

            thus thesis by Y2;

          end;

          hence thesis by Y1, XBOOLE_0:def 10;

        end;

        

         P1: A is finite from FRAENKEL:sch 21( GG);

        ( ord ( 1_ G)) in A;

        hence thesis by P1, T1;

      end;

    end

    theorem :: GROUP_18:1

    

     LM202: for G be finite Group holds ex g be Element of G st ( ord g) = ( upper_bound ( Ordset G))

    proof

      let G be finite Group;

      set A = ( Ordset G);

      set l = ( upper_bound A);

      A <> {} & A c= REAL by NUMBERS: 19, XBOOLE_1: 1;

      then l in A by SEQ_4: 133;

      then

      consider g be Element of G such that

       A3: ( ord g) = l;

      take g;

      thus thesis by A3;

    end;

    theorem :: GROUP_18:2

    

     GROUP630: for G be strict Group, N be strict normal Subgroup of G st G is commutative holds (G ./. N) is commutative

    proof

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

      assume G is commutative;

      then (G ` ) = ( (1). G) by GROUP_5: 75;

      then (G ` ) = ( (1). N) by GROUP_2: 63;

      hence thesis by GROUP_6: 30;

    end;

    theorem :: GROUP_18:3

    

     GRCY26: for G be finite Group, a,b be Element of G holds b in ( gr {a}) iff ex p be Element of NAT st b = (a |^ p)

    proof

      let G be finite Group, a,b be Element of G;

      reconsider a0 = a as Element of ( gr {a}) by GR_CY_2: 2, STRUCT_0:def 5;

      

       X1: ( gr {a0}) = ( gr {a}) by GR_CY_2: 3;

      hereby

        assume b in ( gr {a});

        then

        reconsider b0 = b as Element of ( gr {a});

        consider p be Element of NAT such that

         A1: b0 = (a0 |^ p) by X1, GR_CY_2: 6;

        b = (a |^ p) by GROUP_4: 2, A1;

        hence ex p be Element of NAT st b = (a |^ p);

      end;

      given p be Element of NAT such that

       A1: b = (a |^ p);

      b = (a0 |^ p) by GROUP_4: 2, A1;

      hence thesis;

    end;

    theorem :: GROUP_18:4

    

     GRCY28: for G be finite Group, a be Element of G, n,p,s be Element of NAT st ( card ( gr {a})) = n & n = (p * s) holds ( ord (a |^ p)) = s

    proof

      let G be finite Group, a be Element of G, n,p,s be Element of NAT ;

      assume

       AS1: ( card ( gr {a})) = n & n = (p * s);

      reconsider a0 = a as Element of ( gr {a}) by GR_CY_2: 2, STRUCT_0:def 5;

      

       A0: ( gr {a0}) = ( gr {a}) by GR_CY_2: 3;

      ( ord (a0 |^ p)) = ( card ( gr {(a0 |^ p)})) by GR_CY_1: 7

      .= ( card ( gr {(a |^ p)})) by GROUP_4: 2, GR_CY_2: 3

      .= ( ord (a |^ p)) by GR_CY_1: 7;

      hence ( ord (a |^ p)) = s by A0, AS1, GR_CY_2: 8;

    end;

    theorem :: GROUP_18:5

    

     GRCY212: for k be Element of NAT , G be finite Group, a be Element of G holds ( gr {a}) = ( gr {(a |^ k)}) iff (k gcd ( ord a)) = 1

    proof

      let k be Element of NAT , G be finite Group, a be Element of G;

      set n = ( ord a);

      reconsider a0 = a as Element of ( gr {a}) by GR_CY_2: 2, STRUCT_0:def 5;

      

       A11: ( gr {a0}) = ( gr {a}) by GR_CY_2: 3;

      ( card ( gr {a})) = n by GR_CY_1: 7;

      then ( gr {a}) = ( gr {(a0 |^ k)}) iff (k gcd n) = 1 by A11, GR_CY_2: 12;

      hence thesis by GROUP_4: 2, GR_CY_2: 3;

    end;

    theorem :: GROUP_18:6

    

     GRCY212A: for k be Element of NAT , G be finite Group, a be Element of G st (k gcd ( ord a)) = 1 holds ( ord a) = ( ord (a |^ k))

    proof

      let k be Element of NAT , G be finite Group, a be Element of G;

      assume (k gcd ( ord a)) = 1;

      then

       A1: ( gr {a}) = ( gr {(a |^ k)}) by GRCY212;

      ( card ( gr {a})) = ( ord a) by GR_CY_1: 7;

      hence thesis by A1, GR_CY_1: 7;

    end;

    theorem :: GROUP_18:7

    

     GRCY211: for k be Element of NAT , G be finite Group, a be Element of G holds ( ord a) divides (k * ( ord (a |^ k)))

    proof

      let k be Element of NAT , G be finite Group, a be Element of G;

      a in ( gr {a}) by GR_CY_2: 2;

      then

      reconsider a0 = a as Element of ( gr {a});

      

       A11: ( gr {a0}) = ( gr {a}) by GR_CY_2: 3;

      

       A12: ( card ( gr {a})) = ( ord a) by GR_CY_1: 7;

      ( ord (a |^ k)) = ( card ( gr {(a |^ k)})) = ( card ( gr {(a0 |^ k)})) by GR_CY_1: 7, GROUP_4: 2, GR_CY_2: 3;

      hence thesis by A11, A12, GR_CY_2: 11;

    end;

    theorem :: GROUP_18:8

    

     GRCY212: for G be Group, a,b be Element of G st b in ( gr {a}) holds ( gr {b}) is strict Subgroup of ( gr {a})

    proof

      let G be Group, a,b be Element of G;

      assume b in ( gr {a});

      then

      reconsider b0 = b as Element of ( gr {a});

      ( gr {b0}) = ( gr {b}) by GR_CY_2: 3;

      hence thesis;

    end;

    definition

      let G be strict commutative Group, x be Element of ( Subgroups G);

      :: GROUP_18:def2

      func modetrans (x) -> normal strict Subgroup of G equals x;

      correctness

      proof

        x is strict Subgroup of G by GROUP_3:def 1;

        hence thesis by GROUP_3: 116;

      end;

    end

    theorem :: GROUP_18:9

    

     GROUP252INV: for G,H be Group, K be Subgroup of H, f be Homomorphism of G, H holds ex J be strict Subgroup of G st the carrier of J = (f " the carrier of K)

    proof

      let G,H be Group, K be Subgroup of H, f be Homomorphism of G, H;

      (f . ( 1_ G)) = ( 1_ H) by GROUP_6: 31;

      then (f . ( 1_ G)) in K by GROUP_2: 46;

      then

      reconsider Ivf = (f " the carrier of K) as non empty Subset of the carrier of G by FUNCT_2: 38;

      

       D191: for g1,g2 be Element of G st g1 in Ivf & g2 in Ivf holds (g1 * g2) in Ivf

      proof

        let g1,g2 be Element of G;

        

         D94: (f . (g1 * g2)) = ((f . g1) * (f . g2)) by GROUP_6:def 6;

        assume g1 in Ivf & g2 in Ivf;

        then (f . g1) in K & (f . g2) in K by FUNCT_2: 38;

        then ((f . g1) * (f . g2)) in K by GROUP_2: 50;

        hence (g1 * g2) in Ivf by D94, FUNCT_2: 38;

      end;

      for g be Element of G st g in Ivf holds (g " ) in Ivf

      proof

        let g be Element of G;

        assume g in Ivf;

        then (f . g) in K by FUNCT_2: 38;

        then ((f . g) " ) in K by GROUP_2: 51;

        then (f . (g " )) in the carrier of K by GROUP_6: 32;

        hence (g " ) in Ivf by FUNCT_2: 38;

      end;

      then

      consider J be strict Subgroup of G such that

       D19: the carrier of J = (f " the carrier of K) by GROUP_2: 52, D191;

      take J;

      thus thesis by D19;

    end;

    theorem :: GROUP_18:10

    

     GRCY112: for p be Nat, G be finite Group, x,d be Element of G st ( ord d) = p & p is prime & x in ( gr {d}) holds x = ( 1_ G) or ( gr {x}) = ( gr {d})

    proof

      let p be Nat, G be finite Group, x,d be Element of G;

      assume

       A1: ( ord d) = p & p is prime;

      assume x in ( gr {d});

      then

       X1: ( gr {x}) is strict Subgroup of ( gr {d}) by GRCY212;

      

       X2: ( card ( gr {d})) = p by A1, GR_CY_1: 7;

      ( gr {x}) = ( (1). ( gr {d})) implies x = ( 1_ G)

      proof

        assume

         X3: ( gr {x}) = ( (1). ( gr {d}));

        x in the carrier of ( gr {x}) by GR_CY_2: 2, STRUCT_0:def 5;

        then x in {( 1_ ( gr {d}))} by X3, GROUP_2:def 7;

        then x = ( 1_ ( gr {d})) by TARSKI:def 1;

        hence x = ( 1_ G) by GROUP_2: 44;

      end;

      hence thesis by GR_CY_1: 12, A1, X1, X2;

    end;

    theorem :: GROUP_18:11

    

     LM204D: for G be Group, H,K be normal Subgroup of G st (the carrier of H /\ the carrier of K) = {( 1_ G)} holds (( nat_hom H) | the carrier of K) is one-to-one

    proof

      let G be Group, H,K be normal Subgroup of G;

      assume

       AS1: (the carrier of H /\ the carrier of K) = {( 1_ G)};

      set f = ( nat_hom H);

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

      for x1,x2 be object st x1 in ( dom g) & x2 in ( dom g) & (g . x1) = (g . x2) holds x1 = x2

      proof

        let x1,x2 be object;

        assume

         AS2: x1 in ( dom g) & x2 in ( dom g) & (g . x1) = (g . x2);

        then

         A1: x1 in the carrier of K & x1 in ( dom f) by RELAT_1: 57;

        reconsider y1 = x1 as Element of G by AS2;

        

         A2: x2 in the carrier of K & x2 in ( dom f) by AS2, RELAT_1: 57;

        reconsider y2 = x2 as Element of G by AS2;

        

         A3: (y1 * H) = (f . y1) by GROUP_6:def 8

        .= (g . x1) by A1, FUNCT_1: 49

        .= (f . y2) by AS2, A2, FUNCT_1: 49

        .= (y2 * H) by GROUP_6:def 8;

        (y1 * ( 1_ G)) in (y1 * H) by GROUP_2: 46, GROUP_2: 103;

        then y1 in (y2 * H) by A3, GROUP_1:def 4;

        then

        consider h be Element of G such that

         A4: y1 = (y2 * h) & h in H by GROUP_2: 103;

        y1 in K & y2 in K by AS2, RELAT_1: 57;

        then y1 in K & (y2 " ) in K by GROUP_2: 51;

        then

         A6: ((y2 " ) * y1) in K by GROUP_2: 50;

        ((y2 " ) * y1) in the carrier of H by A4, GROUP_1: 13;

        then ((y2 " ) * y1) in {( 1_ G)} by AS1, XBOOLE_0:def 4, A6;

        then ((y2 " ) * y1) = ( 1_ G) by TARSKI:def 1;

        then (y2 " ) = (y1 " ) by GROUP_1: 12;

        hence thesis by GROUP_1: 9;

      end;

      hence thesis by FUNCT_1:def 4;

    end;

    theorem :: GROUP_18:12

    

     LM204L: for G,F be finite commutative Group, a be Element of G, f be Homomorphism of G, F holds the carrier of ( gr {(f . a)}) = (f .: the carrier of ( gr {a}))

    proof

      let G,F be finite commutative Group, a be Element of G, f be Homomorphism of G, F;

      for y be object holds y in the carrier of ( gr {(f . a)}) iff y in (f .: the carrier of ( gr {a}))

      proof

        let y be object;

        hereby

          assume

           AA1: y in the carrier of ( gr {(f . a)});

          then

          reconsider y0 = y as Element of F by TARSKI:def 3, GROUP_2:def 5;

          y0 in ( gr {(f . a)}) by AA1;

          then

          consider i be Element of NAT such that

           AA2: y0 = ((f . a) |^ i) by GRCY26;

          

           AA3: y0 = (f . (a |^ i)) by AA2, GROUP_6: 37;

          (a |^ i) in ( gr {a}) by GRCY26;

          hence y in (f .: the carrier of ( gr {a})) by AA3, FUNCT_2: 35;

        end;

        assume y in (f .: the carrier of ( gr {a}));

        then

        consider x be object such that

         AA2: x in ( dom f) & x in the carrier of ( gr {a}) & y = (f . x) by FUNCT_1:def 6;

        reconsider x0 = x as Element of G by AA2;

        x0 in ( gr {a}) by AA2;

        then

        consider i be Element of NAT such that

         AA3: x0 = (a |^ i) by GRCY26;

        (f . x0) = ((f . a) |^ i) by AA3, GROUP_6: 37;

        then (f . x0) in ( gr {(f . a)}) by GRCY26;

        hence y in the carrier of ( gr {(f . a)}) by AA2;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: GROUP_18:13

    

     LM204E: for G,F be finite commutative Group, a be Element of G, f be Homomorphism of G, F holds ( ord (f . a)) <= ( ord a)

    proof

      let G,F be finite commutative Group, a be Element of G, f be Homomorphism of G, F;

      

       P1: the carrier of ( gr {(f . a)}) = (f .: the carrier of ( gr {a})) by LM204L;

      

       P2: ( card ( gr {a})) = ( ord a) by GR_CY_1: 7;

      

       P3: ( card ( gr {(f . a)})) = ( ord (f . a)) by GR_CY_1: 7;

      ( Segm ( card the carrier of ( gr {(f . a)}))) c= ( Segm ( card the carrier of ( gr {a}))) by P1, CARD_1: 67;

      hence thesis by P2, P3, NAT_1: 39;

    end;

    theorem :: GROUP_18:14

    

     LM204F: for G,F be finite commutative Group, a be Element of G, f be Homomorphism of G, F st f is one-to-one holds ( ord (f . a)) = ( ord a)

    proof

      let G,F be finite commutative Group, a be Element of G, f be Homomorphism of G, F;

      assume

       AS: f is one-to-one;

      

       P1: the carrier of ( gr {(f . a)}) = (f .: the carrier of ( gr {a})) by LM204L;

      

       P2: ( card ( gr {a})) = ( ord a) by GR_CY_1: 7;

      

       P3: ( card ( gr {(f . a)})) = ( ord (f . a)) by GR_CY_1: 7;

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

      then (the carrier of ( gr {a}),the carrier of ( gr {(f . a)})) are_equipotent by P1, AS, CARD_1: 33, GROUP_2:def 5;

      hence thesis by P2, P3, CARD_1: 5;

    end;

    theorem :: GROUP_18:15

    

     LM204G: for G,F be Group, H be Subgroup of G, f be Homomorphism of G, F holds (f | the carrier of H) is Homomorphism of H, F

    proof

      let G,F be Group, H be Subgroup of G, f be Homomorphism of G, F;

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

      then

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

      for a,b be Element of H holds (g . (a * b)) = ((g . a) * (g . b))

      proof

        let a,b be Element of H;

        a in G & b in G by STRUCT_0:def 5, GROUP_2: 40;

        then

        reconsider a0 = a, b0 = b as Element of G;

        

         A4: (f . a0) = (g . a) by FUNCT_1: 49;

        

         A5: (f . b0) = (g . b) by FUNCT_1: 49;

        (a * b) = (a0 * b0) by GROUP_2: 43;

        

        hence (g . (a * b)) = (f . (a0 * b0)) by FUNCT_1: 49

        .= ((g . a) * (g . b)) by GROUP_6:def 6, A4, A5;

      end;

      hence thesis by GROUP_6:def 6;

    end;

    theorem :: GROUP_18:16

    

     LM204H: for G,F be finite commutative Group, a be Element of G, f be Homomorphism of G, F st (f | the carrier of ( gr {a})) is one-to-one holds ( ord (f . a)) = ( ord a)

    proof

      let G,F be finite commutative Group, a be Element of G, f be Homomorphism of G, F;

      assume

       AS: (f | the carrier of ( gr {a})) is one-to-one;

      reconsider H = (f | the carrier of ( gr {a})) as Homomorphism of ( gr {a}), F by LM204G;

      a in ( gr {a}) by GR_CY_2: 2;

      then

      reconsider a0 = a as Element of ( gr {a});

      (f . a) = (H . a0) by FUNCT_1: 49;

      

      hence ( ord (f . a)) = ( ord a0) by AS, LM204F

      .= ( card ( gr {a0})) by GR_CY_1: 7

      .= ( card ( gr {a})) by GR_CY_2: 3

      .= ( ord a) by GR_CY_1: 7;

    end;

    theorem :: GROUP_18:17

    

     LM204I: for G be finite commutative Group, p be Prime, m be Nat, a be Element of G st ( card G) = (p |^ m) & a <> ( 1_ G) holds ex n be Nat st ( ord a) = (p |^ (n + 1))

    proof

      let G be finite commutative Group, p be Prime, m be Nat, a be Element of G;

      assume

       A1: ( card G) = (p |^ m) & a <> ( 1_ G);

      reconsider Gra = ( gr {a}) as normal strict Subgroup of G by GROUP_3: 116;

      consider n1 be Nat such that

       A8: ( card Gra) = (p |^ n1) & n1 <= m by GROUPP_1: 2, A1, GROUP_2: 148;

      ( ord a) = (p |^ n1) by A8, GR_CY_1: 7;

      then n1 <> 0 by A1, GROUP_1: 43, NEWTON: 4;

      then 1 <= n1 by NAT_1: 14;

      then (n1 - 1) in NAT by INT_1: 3, XREAL_1: 48;

      then

      reconsider n = (n1 - 1) as Nat;

      take n;

      thus ( ord a) = (p |^ (n + 1)) by A8, GR_CY_1: 7;

    end;

    

     LM204K1: for p be Prime, m,k be Nat st m divides (p |^ k) & m <> 1 holds ex j be Nat st m = (p |^ (j + 1))

    proof

      let p be Prime, m,k be Nat;

      assume

       AS1: m divides (p |^ k) & m <> 1;

      then

      consider r be Nat such that

       P1: m = (p |^ r) & r <= k by GROUPP_1: 2;

      r <> 0 by P1, AS1, NEWTON: 4;

      then 1 <= r by NAT_1: 14;

      then (r - 1) in NAT by INT_1: 3, XREAL_1: 48;

      then

      reconsider j = (r - 1) as Nat;

      take j;

      thus m = (p |^ (j + 1)) by P1;

    end;

    theorem :: GROUP_18:18

    

     LM204K: for p be Prime, j,m,k be Nat st m = (p |^ k) & not p divides j holds (j gcd m) = 1

    proof

      let p be Prime, j,m,k be Nat;

      assume

       AS: m = (p |^ k) & not p divides j;

      assume

       A1: (j gcd m) <> 1;

      set q = (j gcd m);

      q divides j by NAT_D:def 5;

      then

       A4: j = (q * (j div q)) by NAT_D: 3;

      q divides m by NAT_D:def 5;

      then

      consider n be Nat such that

       A5: q = (p |^ (n + 1)) by A1, LM204K1, AS;

      j = (((p |^ n) * p) * (j div q)) by A4, A5, NEWTON: 6

      .= (((p |^ n) * (j div q)) * p);

      hence contradiction by AS, INT_1:def 3;

    end;

    

     LM204A: for G be strict finite commutative Group, p be Prime, m be Nat, g be Element of G st ( card G) = (p |^ m) & ( ord g) = ( upper_bound ( Ordset G)) holds ex K be normal strict Subgroup of G st (the carrier of K /\ the carrier of ( gr {g})) = {( 1_ G)} & for x be Element of G holds ex b1,a1 be Element of G st b1 in K & a1 in ( gr {g}) & x = (b1 * a1)

    proof

      defpred P[ Nat] means for G be strict finite commutative Group, p be Prime, g be Element of G st ( card G) = (p |^ $1) & ( ord g) = ( upper_bound ( Ordset G)) holds ex K be normal strict Subgroup of G st (the carrier of K /\ the carrier of ( gr {g})) = {( 1_ G)} & for x be Element of G holds ex b1,a1 be Element of G st b1 in K & a1 in ( gr {g}) & x = (b1 * a1);

      

       P0: P[ 0 ]

      proof

        let G be strict finite commutative Group, p be Prime, g be Element of G;

        assume

         AS1: ( card G) = (p |^ 0 ) & ( ord g) = ( upper_bound ( Ordset G));

        reconsider H = G as strict finite Subgroup of G by GROUP_2: 54;

        ( card H) = 1 by AS1, NEWTON: 4;

        then

         A1: ( (1). G) = G by GROUP_2: 70;

        reconsider K = ( (1). G) as normal strict Subgroup of G;

        g in the carrier of ( (1). G) by A1;

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

        then

         A2: g = ( 1_ G) by TARSKI:def 1;

        for x be object holds x in the carrier of ( gr {g}) iff x in {( 1_ G)}

        proof

          let x be object;

          hereby

            assume

             AA1: x in the carrier of ( gr {g});

            then

            reconsider x0 = x as Element of G by TARSKI:def 3, GROUP_2:def 5;

            x0 in ( gr {g}) by AA1;

            then

            consider i be Element of NAT such that

             AA2: x0 = (g |^ i) by GRCY26;

            x0 = ( 1_ G) by AA2, A2, GROUP_1: 31;

            hence x in {( 1_ G)} by TARSKI:def 1;

          end;

          assume x in {( 1_ G)};

          then x = ( 1_ G) by TARSKI:def 1;

          hence thesis by GROUP_2: 46, STRUCT_0:def 5;

        end;

        then

         X1: the carrier of ( gr {g}) = {( 1_ G)} by TARSKI: 2;

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

        then

         X2: (the carrier of K /\ the carrier of ( gr {g})) = {( 1_ G)} by X1;

        for x be Element of G holds ex b1,a1 be Element of G st b1 in K & a1 in ( gr {g}) & x = (b1 * a1)

        proof

          let x be Element of G;

          x in the carrier of ( (1). G) by A1;

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

          then x = ( 1_ G) by TARSKI:def 1;

          then

           X3: x = (( 1_ G) * ( 1_ G)) by GROUP_1:def 4;

          ( 1_ G) in ( gr {g}) & ( 1_ G) in K by GROUP_2: 46;

          hence thesis by X3;

        end;

        hence thesis by X2;

      end;

      

       PN: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         AS1: P[k];

        let G be strict finite commutative Group, p be Prime, a be Element of G;

        assume

         A1: ( card G) = (p |^ (k + 1)) & ( ord a) = ( upper_bound ( Ordset G));

        deffunc ordset( finite Group) = ( Ordset $1);

        per cases ;

          suppose

           CA1: ( card ( gr {a})) = ( card G);

          then

           P1: ( gr {a}) = G by GROUP_2: 73;

          reconsider K = ( (1). G) as normal strict Subgroup of G;

          

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

          

           P3: the carrier of ( gr {a}) = the carrier of G by CA1, GROUP_2: 73;

          

           X1: (the carrier of K /\ the carrier of ( gr {a})) = {( 1_ G)} by P2, P3, XBOOLE_1: 28;

          for x be Element of G holds ex b1,a1 be Element of G st b1 in K & a1 in ( gr {a}) & x = (b1 * a1)

          proof

            let x be Element of G;

            

             X2: x in ( gr {a}) by P1;

            

             X3: x = (( 1_ G) * x) by GROUP_1:def 4;

            ( 1_ G) in K by GROUP_2: 46;

            hence thesis by X3, X2;

          end;

          hence thesis by X1;

        end;

          suppose

           B2: ( card ( gr {a})) <> ( card G);

          reconsider Gra = ( gr {a}) as normal strict Subgroup of G by GROUP_3: 116;

          reconsider G1 = (G ./. Gra) as strict finite commutative Group by GROUP630;

          

           A5: ( ord a) = ( card ( gr {a})) by GR_CY_1: 7;

          

           A6: ( card G) = (( ord a) * ( index Gra)) by A5, GROUP_2: 147;

          consider n1 be Nat such that

           A8: ( card Gra) = (p |^ n1) & n1 <= (k + 1) by GROUPP_1: 2, GROUP_2: 148, A1;

          ((k + 1) - n1) in NAT by A8, XREAL_1: 48, INT_1: 3;

          then

          reconsider mn1 = ((k + 1) - n1) as Nat;

          

           A9: ( ord a) = (p |^ n1) by A8, GR_CY_1: 7;

          

           A10: ( ord a) <> 0 by A8, GR_CY_1: 7;

          

           A10A: 0 < ( ord a) by A8, GR_CY_1: 7;

          ( index Gra) = ((p |^ (mn1 + n1)) / (p |^ n1)) by A6, XCMPLX_1: 89, A1, A9

          .= (((p |^ mn1) * (p |^ n1)) / (p |^ n1)) by NEWTON: 8

          .= (p |^ mn1) by XCMPLX_1: 89;

          then

           A11: ( card (G ./. Gra)) = (p |^ mn1) by GROUP_6: 27;

          consider b be Element of G such that

           A20: not b in Gra by B2, GROUPP_1: 12;

          reconsider bga = (b * Gra) as Element of G1 by GROUP_2:def 15;

          reconsider Grbga = ( gr {bga}) as normal strict Subgroup of G1 by GROUP_3: 116;

          consider s be Nat such that

           A18: ( card Grbga) = (p |^ s) & s <= mn1 by GROUPP_1: 2, GROUP_2: 148, A11;

          

           A19: ( ord bga) = (p |^ s) by A18, GR_CY_1: 7;

          ( ord bga) <> 1

          proof

            assume ( ord bga) = 1;

            then bga = ( 1_ G1) by GROUP_1: 43;

            then

             A191: (b * Gra) = the carrier of Gra by GROUP_6: 24;

            (b * ( 1_ G)) in (b * Gra) by GROUP_2: 46, GROUP_2: 103;

            hence contradiction by A20, A191, GROUP_1:def 4;

          end;

          then s <> 0 by A19, NEWTON: 4;

          then 0 <= (s - 1) by NAT_1: 14, XREAL_1: 48;

          then (s - 1) in NAT by INT_1: 3;

          then

          reconsider s1 = (s - 1) as Nat;

          reconsider c = (b |^ (p |^ s1)) as Element of G;

          reconsider cga = (c * Gra) as Element of G1 by GROUP_2:def 15;

          

           A21: ((p |^ s1) * p) = (p |^ (s1 + 1)) by NEWTON: 6

          .= (p |^ s);

          

           XN1: (p |^ s) is Element of NAT & (p |^ s1) is Element of NAT & p is Element of NAT by ORDINAL1:def 12;

          

           A24: ( ord (bga |^ (p |^ s1))) = p by XN1, GRCY28, A21, A18;

          

           A23: ( ord cga) = p by A24, GROUPP_1: 8;

          

           A26: not c in Gra

          proof

            assume

             A261: c in Gra;

            cga = ( carr Gra) by A261, GROUP_2: 113

            .= ( 1_ G1) by GROUP_6: 24;

            then ( ord cga) = 1 by GROUP_1: 42;

            hence contradiction by A23, INT_2:def 4;

          end;

          

           A24: (cga |^ p) = ( 1_ G1) by A23, GROUP_1: 41;

          

           A25: (cga |^ p) = ((c |^ p) * Gra) by GROUPP_1: 8;

          ((c |^ p) * ( 1_ G)) in ((c |^ p) * Gra) by GROUP_2: 46, GROUP_2: 103;

          then (c |^ p) in ((c |^ p) * Gra) by GROUP_1:def 4;

          then (c |^ p) in ( gr {a}) by A24, A25, GROUP_6: 24;

          then

          consider j be Element of NAT such that

           A26B: (c |^ p) = (a |^ j) by GRCY26;

          p divides j

          proof

            assume not p divides j;

            then

             A27Z: (j gcd ( ord a)) = 1 by A8, LM204K, GR_CY_1: 7;

            

             A272: ( ord (c |^ p)) = ( ord a) by A26B, A27Z, GRCY212A;

            

             A273: ( ord c) = (p * ( ord (c |^ p)))

            proof

              ( ord (c |^ p)) <> 0 by A10, A26B, A27Z, GRCY212A;

              then

               A274: ( ord c) <= (p * ( ord (c |^ p))) by XN1, GRCY211, NAT_D: 7;

              c <> ( 1_ G) by A26, GROUP_2: 46;

              then

              consider k be Nat such that

               A2750: ( ord c) = (p |^ (k + 1)) by A1, LM204I;

              

               A275B: (p * (p |^ k)) = ( ord c) by A2750, NEWTON: 6;

              

               A275: (( ord c) / p) = (p |^ k) by A275B, XCMPLX_1: 89;

              ((c |^ p) |^ (p |^ k)) = (c |^ (p * (p |^ k))) by GROUP_1: 35

              .= ( 1_ G) by A275B, GROUP_1: 41;

              then ( ord (c |^ p)) <= (( ord c) / p) by A275, NAT_D: 7, GROUP_1: 44;

              then (p * ( ord (c |^ p))) <= ( ord c) by XREAL_1: 83;

              hence thesis by A274, XXREAL_0: 1;

            end;

            

             XXX0: (1 * ( ord a)) < (p * ( ord a)) by A10A, XREAL_1: 68, INT_2:def 4;

            ( ord c) in ( Ordset G);

            hence contradiction by XXX0, A1, A272, A273, SEQ_4:def 1;

          end;

          then

          consider j1 be Nat such that

           A28: j = (p * j1) by NAT_D:def 3;

          

           A28A: j1 is Element of NAT by ORDINAL1:def 12;

          set d = (c * (a |^ ( - j1)));

          

           A30: (d |^ p) = ((c |^ p) * ((a |^ ( - j1)) |^ p)) by GROUP_1: 38

          .= ((c |^ p) * (a |^ (( - j1) * p))) by GROUP_1: 35

          .= ((c |^ p) * (a |^ ( - j))) by A28

          .= ((c |^ p) * ((a |^ j) " )) by GROUP_1: 36

          .= ( 1_ G) by A26B, GROUP_1:def 5;

          ( ord d) <> 1

          proof

            assume ( ord d) = 1;

            then (c * (a |^ ( - j1))) = ( 1_ G) by GROUP_1: 43;

            then (c " ) = (a |^ ( - j1)) by GROUP_1: 12;

            then (c " ) = ((a |^ j1) " ) by GROUP_1: 36;

            hence contradiction by A26, A28A, GRCY26, GROUP_1: 9;

          end;

          then

           A32: ( ord d) = p by A30, INT_2:def 4, GROUP_1: 44;

          

           A33: not d in ( gr {a})

          proof

            assume d in ( gr {a});

            then

            consider k be Element of NAT such that

             A331: (c * (a |^ ( - j1))) = (a |^ k) by GRCY26;

            (c * ((a |^ j1) " )) = (a |^ k) by GROUP_1: 36, A331;

            then c = ((a |^ k) * (a |^ j1)) by GROUP_1: 14;

            then c = (a |^ (j1 + k)) by GROUP_1: 33;

            hence contradiction by A26, GRCY26;

          end;

          

           A3Z: for x be object holds x in (the carrier of ( gr {d}) /\ the carrier of ( gr {a})) iff x in {( 1_ G)}

          proof

            let x0 be object;

            hereby

              assume

               A310: x0 in (the carrier of ( gr {d}) /\ the carrier of ( gr {a}));

              then x0 in the carrier of ( gr {d}) & x0 in the carrier of ( gr {a}) by XBOOLE_0:def 4;

              then

              reconsider x = x0 as Element of G by GROUP_2:def 5, TARSKI:def 3;

              x in ( gr {d}) by A310, XBOOLE_0:def 4;

              then

               A322: x = ( 1_ G) or ( gr {x}) = ( gr {d}) by GRCY112, A32;

              x in ( gr {a}) by A310, XBOOLE_0:def 4;

              then

               X1: ( gr {x}) is strict Subgroup of ( gr {a}) by GRCY212;

              ( gr {x}) <> ( gr {d})

              proof

                assume ( gr {x}) = ( gr {d});

                then

                 XX1: the carrier of ( gr {d}) c= the carrier of ( gr {a}) by X1, GROUP_2:def 5;

                d in ( gr {d}) by GR_CY_2: 2;

                hence contradiction by A33, XX1;

              end;

              hence x0 in {( 1_ G)} by A322, TARSKI:def 1;

            end;

            assume x0 in {( 1_ G)};

            then x0 = ( 1_ G) by TARSKI:def 1;

            then x0 in the carrier of ( gr {d}) & x0 in the carrier of ( gr {a}) by GROUP_2: 46, STRUCT_0:def 5;

            hence thesis by XBOOLE_0:def 4;

          end;

          then

           A33: (the carrier of ( gr {d}) /\ the carrier of ( gr {a})) = {( 1_ G)} by TARSKI: 2;

          reconsider Grd = ( gr {d}) as normal strict Subgroup of G by GROUP_3: 116;

          reconsider G2 = (G ./. Grd) as strict finite commutative Group by GROUP630;

          

           D5: ( ord d) = ( card ( gr {d})) by GR_CY_1: 7;

          

           D6: ( card G) = (( ord d) * ( index Grd)) by D5, GROUP_2: 147;

          ( index Grd) = (( card G) / ( ord d)) by A32, D6, XCMPLX_1: 89

          .= (((p |^ k) * p) / p) by A1, A32, NEWTON: 6

          .= (p |^ k) by XCMPLX_1: 89;

          then

           D11: ( card (G ./. Grd)) = (p |^ k) by GROUP_6: 27;

          set Ordset1 = ( Ordset G2);

          set Pd = ( nat_hom Grd);

          

           D130: Pd is onto by GROUP_6: 59;

          reconsider gd = (Pd . a) as Element of G2;

          set H = (Pd | the carrier of Gra);

          

           D14: H is one-to-one by A3Z, LM204D, TARSKI: 2;

          

           D14B: for r be Real st r in Ordset1 holds r <= ( ord gd)

          proof

            assume not for r be Real st r in Ordset1 holds r <= ( ord gd);

            then

            consider r be Real such that

             D141: r in Ordset1 & not r <= ( ord gd);

            

             D142: ( ord a) < r by D141, D14, LM204H;

            consider gx be Element of G2 such that

             D143: r = ( ord gx) by D141;

            ( rng Pd) = the carrier of G2 by D130, FUNCT_2:def 3;

            then

            consider a1 be Element of G such that

             D232: gx = (Pd . a1) by FUNCT_2: 113;

            ( ord gx) <= ( ord a1) by D232, LM204E;

            then

             X1: ( ord a) < ( ord a1) by XXREAL_0: 2, D143, D142;

            ( ord a1) in ( Ordset G);

            hence contradiction by X1, A1, SEQ_4:def 1;

          end;

          

           XU1: ( upper_bound Ordset1) <= ( ord gd) by SEQ_4: 45, D14B;

          ( ord gd) in Ordset1;

          then ( ord gd) <= ( upper_bound Ordset1) by SEQ_4:def 1;

          then ( ord gd) = ( upper_bound Ordset1) by XXREAL_0: 1, XU1;

          then

          consider K2 be normal strict Subgroup of G2 such that

           D17: (the carrier of K2 /\ the carrier of ( gr {gd})) = {( 1_ G2)} & for g2 be Element of G2 holds ex b2,a2 be Element of G2 st b2 in K2 & a2 in ( gr {gd}) & g2 = (b2 * a2) by AS1, D11;

          consider K be strict Subgroup of G such that

           D19: the carrier of K = (Pd " the carrier of K2) by GROUP252INV;

          reconsider K as normal strict Subgroup of G by GROUP_3: 116;

          

           D20: for x be Element of G st x in (the carrier of K /\ the carrier of ( gr {a})) holds (Pd . x) in (the carrier of K2 /\ the carrier of ( gr {(Pd . a)}))

          proof

            let x be Element of G;

            assume

             D20A: x in (the carrier of K /\ the carrier of ( gr {a}));

            then

             D20B: x in the carrier of ( gr {a}) & x in the carrier of K by XBOOLE_0:def 4;

            x in ( gr {a}) by D20A, XBOOLE_0:def 4;

            then

            consider k be Element of NAT such that

             D20C: x = (a |^ k) by GRCY26;

            

             XXX: (Pd . x) is Element of G2;

            (Pd . x) = ((Pd . a) |^ k) by D20C, GROUP_6: 37;

            then

             D233: (Pd . x) in ( gr {(Pd . a)}) by XXX, GRCY26;

            (Pd . x) in the carrier of K2 by D20B, D19, FUNCT_2: 38;

            hence thesis by D233, XBOOLE_0:def 4;

          end;

          

           D22: for x be Element of G st x in (the carrier of K /\ the carrier of ( gr {a})) holds x in (the carrier of ( Ker Pd) /\ the carrier of ( gr {a}))

          proof

            let x be Element of G;

            assume

             D22A: x in (the carrier of K /\ the carrier of ( gr {a}));

            then (Pd . x) in {( 1_ G2)} by D17, D20;

            then (Pd . x) = ( 1_ G2) by TARSKI:def 1;

            then x in { s where s be Element of G : (Pd . s) = ( 1_ G2) };

            then

             D22B: x in the carrier of ( Ker Pd) by GROUP_6:def 9;

            x in the carrier of ( gr {a}) by D22A, XBOOLE_0:def 4;

            hence thesis by D22B, XBOOLE_0:def 4;

          end;

          

           D23A: (the carrier of K /\ the carrier of ( gr {a})) c= {( 1_ G)}

          proof

            let x be object;

            assume

             D221: x in (the carrier of K /\ the carrier of ( gr {a}));

            then x in the carrier of K by XBOOLE_0:def 4;

            then

            reconsider x0 = x as Element of G by TARSKI:def 3, GROUP_2:def 5;

            x0 in (the carrier of ( Ker Pd) /\ the carrier of ( gr {a})) by D22, D221;

            then

             D222: x0 in the carrier of ( gr {a}) & x0 in the carrier of ( Ker Pd) by XBOOLE_0:def 4;

            then x0 in the carrier of ( gr {d}) by GROUP_6: 43;

            hence x in {( 1_ G)} by A33, D222, XBOOLE_0:def 4;

          end;

          ( 1_ G) in the carrier of ( gr {a}) & ( 1_ G) in the carrier of K by STRUCT_0:def 5, GROUP_2: 46;

          then ( 1_ G) in (the carrier of K /\ the carrier of ( gr {a})) by XBOOLE_0:def 4;

          then

           D23B: {( 1_ G)} c= (the carrier of K /\ the carrier of ( gr {a})) by ZFMISC_1: 31;

          for g be Element of G holds ex b1,a1 be Element of G st b1 in K & a1 in ( gr {a}) & g = (b1 * a1)

          proof

            let g be Element of G;

            reconsider g2 = (Pd . g) as Element of G2;

            consider b2,a2 be Element of G2 such that

             D231: b2 in K2 & a2 in ( gr {gd}) & g2 = (b2 * a2) by D17;

            consider i be Element of NAT such that

             D231A: a2 = (gd |^ i) by GRCY26, D231;

            ( rng Pd) = the carrier of G2 by D130, FUNCT_2:def 3;

            then

            consider b1 be Element of the carrier of G such that

             D232: b2 = (Pd . b1) by FUNCT_2: 113;

            

             D234: (Pd . ((a |^ i) * b1)) = ((Pd . (a |^ i)) * (Pd . b1)) by GROUP_6:def 6

            .= (Pd . g) by D231A, D231, D232, GROUP_6: 37;

            

             D235: (((a |^ i) * b1) * ( gr {d})) = (Pd . ((a |^ i) * b1)) by GROUP_6:def 8

            .= (g * ( gr {d})) by D234, GROUP_6:def 8;

            (g * ( 1_ G)) in (g * ( gr {d})) by GROUP_2: 46, GROUP_2: 103;

            then g in (((a |^ i) * b1) * ( gr {d})) by D235, GROUP_1:def 4;

            then

            consider y be Element of G such that

             D236: g = (((a |^ i) * b1) * y) & y in ( gr {d}) by GROUP_2: 103;

            

             D236A: g = ((a |^ i) * (b1 * y)) by D236, GROUP_1:def 3;

            consider j be Element of NAT such that

             D237: y = (d |^ j) by GRCY26, D236;

            

             D238: (Pd . d) = (d * ( gr {d})) by GROUP_6:def 8

            .= ( carr ( gr {d})) by GR_CY_2: 2, GROUP_2: 113

            .= ( 1_ G2) by GROUP_6: 24;

            

             D239: (Pd . y) = ((Pd . d) |^ j) by D237, GROUP_6: 37

            .= ( 1_ G2) by D238, GROUP_1: 31;

            ( 1_ G2) in the carrier of K2 by GROUP_2: 46, STRUCT_0:def 5;

            then b1 in K & y in K by D19, D231, D232, D239, FUNCT_2: 38;

            then (b1 * y) in K by GROUP_2: 50;

            hence thesis by D236A, GRCY26;

          end;

          hence thesis by D23A, D23B, XBOOLE_0:def 10;

        end;

      end;

      for k be Nat holds P[k] from NAT_1:sch 2( P0, PN);

      hence thesis;

    end;

    begin

    theorem :: GROUP_18:19

    

     LM204: for G be strict finite commutative Group, p be Prime, m be Nat st ( card G) = (p |^ m) holds ex K be normal strict Subgroup of G, n,k be Nat, g be Element of G st ( ord g) = ( upper_bound ( Ordset G)) & K is finite commutative & (the carrier of K /\ the carrier of ( gr {g})) = {( 1_ G)} & (for x be Element of G holds ex b1,a1 be Element of G st b1 in K & a1 in ( gr {g}) & x = (b1 * a1)) & ( ord g) = (p |^ n) & k = (m - n) & n <= m & ( card K) = (p |^ k) & ex F be Homomorphism of ( product <*K, ( gr {g})*>), G st F is bijective & for a,b be Element of G st a in K & b in ( gr {g}) holds (F . <*a, b*>) = (a * b)

    proof

      let G be strict finite commutative Group, p be Prime, m be Nat;

      assume

       AS: ( card G) = (p |^ m);

      consider g be Element of G such that

       A0: ( ord g) = ( upper_bound ( Ordset G)) by LM202;

      consider K be normal strict Subgroup of G such that

       P1: (the carrier of K /\ the carrier of ( gr {g})) = {( 1_ G)} & for x be Element of G holds ex b1,a1 be Element of G st b1 in K & a1 in ( gr {g}) & x = (b1 * a1) by AS, A0, LM204A;

      consider n be Nat such that

       Q4: ( card ( gr {g})) = (p |^ n) & n <= m by AS, GROUPP_1: 2, GROUP_2: 148;

      (m - n) in NAT by Q4, INT_1: 3, XREAL_1: 48;

      then

      reconsider k = (m - n) as Nat;

      ( gr {g}) is normal Subgroup of G by GROUP_3: 116;

      then

      consider F be Homomorphism of ( product <*K, ( gr {g})*>), G such that

       P5: F is bijective & for a,b be Element of G st a in K & b in ( gr {g}) holds (F . <*a, b*>) = (a * b) by P1, GROUP_17: 12;

      set s = ( card K);

      set t = ( card ( gr {g}));

      F is one-to-one & ( dom F) = the carrier of ( product <*K, ( gr {g})*>) & ( rng F) = the carrier of G by P5, FUNCT_2:def 1, FUNCT_2:def 3;

      then

       X6: ( card ( product <*K, ( gr {g})*>)) = ( card G) by CARD_1: 5, WELLORD2:def 4;

      (( card K) * (p |^ n)) = (p |^ (k + n)) by X6, Q4, AS, GROUP_17: 17

      .= ((p |^ k) * (p |^ n)) by NEWTON: 8;

      then ( card K) = (p |^ k) by XCMPLX_1: 5;

      hence thesis by A0, P1, P5, Q4, GR_CY_1: 7;

    end;

    theorem :: GROUP_18:20

    

     LM205A: for G be strict finite commutative Group, p be Prime, m be Nat st ( card G) = (p |^ m) holds ex k be non zero Nat, a be k -element FinSequence of G, Inda be k -element FinSequence of NAT , F be associative Group-like commutative multMagma-Family of ( Seg k), HFG be Homomorphism of ( product F), G st (for i be Nat st i in ( Seg k) holds ex ai be Element of G st ai = (a . i) & (F . i) = ( gr {ai}) & ( ord ai) = (p |^ (Inda . i))) & (for i be Nat st 1 <= i & i <= (k - 1) holds (Inda . i) <= (Inda . (i + 1))) & (for p,q be Element of ( Seg k) st p <> q holds (the carrier of (F . p) /\ the carrier of (F . q)) = {( 1_ G)}) & HFG is bijective & for x be the carrier of G -valued total( Seg k) -defined Function st for p be Element of ( Seg k) holds (x . p) in (F . p) holds x in ( product F) & (HFG . x) = ( Product x)

    proof

      defpred P[ Nat] means for G be strict finite commutative Group, p be Prime st ( card G) = (p |^ $1) holds ex k be non zero Nat, a be k -element FinSequence of G, Inda be k -element FinSequence of NAT , F be associative Group-like commutative multMagma-Family of ( Seg k), HFG be Homomorphism of ( product F), G st (for i be Nat st i in ( Seg k) holds ex ai be Element of G st ai = (a . i) & (F . i) = ( gr {ai}) & ( ord ai) = (p |^ (Inda . i))) & (for i be Nat st 1 <= i & i <= (k - 1) holds (Inda . i) <= (Inda . (i + 1))) & (for i,j be Element of ( Seg k) st i <> j holds (the carrier of (F . i) /\ the carrier of (F . j)) = {( 1_ G)}) & HFG is bijective & for x be the carrier of G -valued total( Seg k) -defined Function st for p be Element of ( Seg k) holds (x . p) in (F . p) holds x in ( product F) & (HFG . x) = ( Product x);

      

       P1: for n be Nat st for k be Nat st k < n holds P[k] holds P[n]

      proof

        let n be Nat;

        assume

         APN: for k be Nat st k < n holds P[k];

        thus P[n]

        proof

          let G be strict finite commutative Group, p be Prime;

          assume

           AS1: ( card G) = (p |^ n);

          then

          consider H be normal strict Subgroup of G, n0,m0 be Nat, g0 be Element of G such that

           P8: ( ord g0) = ( upper_bound ( Ordset G)) & H is finite & H is commutative & (the carrier of H /\ the carrier of ( gr {g0})) = {( 1_ G)} & (for x be Element of G holds ex b1,a1 be Element of G st b1 in H & a1 in ( gr {g0}) & x = (b1 * a1)) & ( ord g0) = (p |^ n0) & m0 = (n - n0) & n0 <= n & ( card H) = (p |^ m0) & ex I0 be Homomorphism of ( product <*H, ( gr {g0})*>), G st I0 is bijective & for a,b be Element of G st a in H & b in ( gr {g0}) holds (I0 . <*a, b*>) = (a * b) by LM204;

          per cases ;

            suppose

             BBB: n = n0;

            reconsider q = 1 as non zero Nat;

            set K = ( gr {g0});

            set I = {q};

            set F = (I --> G);

            ( card G) = ( card ( gr {g0})) by AS1, BBB, P8, GR_CY_1: 7;

            then

             X10: G = ( gr {g0}) by GROUP_2: 73;

            reconsider a = <*g0*> as q -element FinSequence of G by FINSEQ_1: 74;

            

             VV1: n0 is Element of NAT by ORDINAL1:def 12;

            reconsider Inda = <*n0*> as q -element FinSequence of NAT by VV1, FINSEQ_1: 74;

            

             Z1: for i be Nat st i in ( Seg q) holds ex ai be Element of G st ai = (a . i) & (F . i) = ( gr {ai}) & ( ord ai) = (p |^ (Inda . i))

            proof

              let i be Nat;

              assume

               ASD1: i in ( Seg q);

              

               D57: i = 1 by TARSKI:def 1, ASD1, FINSEQ_1: 2;

              then

               D58: (Inda . i) = n0 by FINSEQ_1: 40;

              (a . i) = g0 by D57, FINSEQ_1: 40;

              hence thesis by ASD1, D58, P8, X10, FINSEQ_1: 2, FUNCOP_1: 7;

            end;

            

             Z2: for i be Nat st 1 <= i & i <= (q - 1) holds (Inda . i) <= (Inda . (i + 1))

            proof

              let i be Nat;

              assume 1 <= i & i <= (q - 1);

              then 1 <= i & i <= 0 ;

              hence thesis;

            end;

            for y be set st y in ( rng F) holds y is non empty multMagma

            proof

              let y be set;

              assume y in ( rng F);

              then

              consider x be object such that

               D4: x in ( dom F) & y = (F . x) by FUNCT_1:def 3;

              thus y is non empty multMagma by FUNCOP_1: 7, D4;

            end;

            then

            reconsider F as multMagma-Family of I by GROUP_7:def 1;

            

             GG1: for s,t be Element of I st s <> t holds (the carrier of (F . s) /\ the carrier of (F . t)) = {( 1_ G)}

            proof

              let s,t be Element of I;

              assume

               GG11: s <> t;

              s = q by TARSKI:def 1;

              hence thesis by GG11, TARSKI:def 1;

            end;

            

             AR1: for i be Element of I holds (F . i) is Group-like;

            

             AR2: for i be Element of I holds (F . i) is associative;

            for i be Element of I holds (F . i) is commutative;

            then

            reconsider F as associative Group-like commutative multMagma-Family of I by AR1, GROUP_7:def 6, AR2, GROUP_7:def 7, GROUP_7:def 8;

            F = (q .--> G);

            then

            consider HFG be Homomorphism of ( product F), G such that

             X4: HFG is bijective & for x be the carrier of G -valued total {q} -defined Function holds (HFG . x) = ( Product x) by GROUP_17: 26;

            F = (q .--> G);

            then for x be the carrier of G -valued totalI -defined Function st for p be Element of I holds (x . p) in (F . p) holds x in ( product F) & (HFG . x) = ( Product x) by X4, GROUP_17: 25;

            hence thesis by X4, GG1, Z1, Z2, FINSEQ_1: 2;

          end;

            suppose

             AAA: n <> n0;

             0 <> n0

            proof

              assume

               X0: n0 = 0 ;

              then

               X1: ( ord g0) = 1 by P8, NEWTON: 4;

              for z be object holds z in the carrier of G iff z in {( 1_ G)}

              proof

                let z be object;

                hereby

                  assume z in the carrier of G;

                  then

                  reconsider x = z as Element of G;

                  ( ord x) in ( Ordset G);

                  then

                   X2: ( ord x) <= 1 by X1, P8, SEQ_4:def 1;

                  ( ord x) = ( card ( gr {x})) by GR_CY_1: 7;

                  then 1 <= ( ord x) by GROUP_1: 45;

                  then x = ( 1_ G) by X2, XXREAL_0: 1, GROUP_1: 43;

                  hence z in {( 1_ G)} by TARSKI:def 1;

                end;

                assume z in {( 1_ G)};

                hence z in the carrier of G;

              end;

              then

               XX1: the carrier of G = {( 1_ G)} by TARSKI: 2;

              n = 0

              proof

                assume n <> 0 ;

                then 1 < (p to_power n) by POWER: 35, INT_2:def 4;

                hence contradiction by AS1, XX1, CARD_1: 30;

              end;

              hence contradiction by X0, AAA;

            end;

            then (n - n0) < (n - 0 qua Real) by XREAL_1: 15;

            then

            consider k0 be non zero Nat, a0 be k0 -element FinSequence of H, Inda0 be k0 -element FinSequence of NAT , F0 be associative Group-like commutative multMagma-Family of ( Seg k0), HFG0 be Homomorphism of ( product F0), H such that

             P12: (for i be Nat st i in ( Seg k0) holds ex ai be Element of H st ai = (a0 . i) & (F0 . i) = ( gr {ai}) & ( ord ai) = (p |^ (Inda0 . i))) & (for i be Nat st 1 <= i & i <= (k0 - 1) holds (Inda0 . i) <= (Inda0 . (i + 1))) & (for p,q be Element of ( Seg k0) st p <> q holds (the carrier of (F0 . p) /\ the carrier of (F0 . q)) = {( 1_ H)}) & HFG0 is bijective & for x be the carrier of H -valued total( Seg k0) -defined Function st for p be Element of ( Seg k0) holds (x . p) in (F0 . p) holds x in ( product F0) & (HFG0 . x) = ( Product x) by P8, APN;

            reconsider q = (k0 + 1) as non zero Nat;

            set K = ( gr {g0});

            set F = (F0 +* ( {q} --> K));

            set I0 = ( Seg k0);

            set I = ( Seg q);

            

             INDK1: (Inda0 . k0) <= n0

            proof

              assume

               K1: not (Inda0 . k0) <= n0;

              

               K2: 1 <= k0 by NAT_1: 14;

              1 < p by INT_2:def 4;

              then

               K3: (p to_power n0) < (p to_power (Inda0 . k0)) by K1, POWER: 39;

              k0 in ( Seg k0) by K2;

              then

              consider ai be Element of H such that

               C5: ai = (a0 . k0) & (F0 . k0) = ( gr {ai}) & ( ord ai) = (p |^ (Inda0 . k0)) by P12;

              reconsider aai = ai as Element of G by TARSKI:def 3, GROUP_2:def 5;

              

               D54: ( gr {aai}) = ( gr {ai}) by GR_CY_2: 3;

              

               D55: ( ord aai) = ( card ( gr {ai})) by D54, GR_CY_1: 7

              .= (p |^ (Inda0 . k0)) by C5, GR_CY_1: 7;

              ( ord aai) in ( Ordset G);

              hence contradiction by D55, K3, P8, SEQ_4:def 1;

            end;

            

             NU0: q is Element of I by FINSEQ_1: 4;

            

             DIQ1: for x be object holds x in I0 iff x in I & not x in {q}

            proof

              let x be object;

              hereby

                assume

                 X1: x in I0;

                then

                reconsider x1 = x as Nat;

                

                 X4: k0 < (k0 + 1) by NAT_1: 16;

                x1 <> (k0 + 1) by X1, NAT_1: 16, FINSEQ_1: 1;

                hence x in I & not x in {q} by X1, X4, FINSEQ_1: 5, TARSKI:def 1, TARSKI:def 3;

              end;

              assume

               X1: x in I & not x in {q};

              then

              reconsider x1 = x as Nat;

              

               X2: 1 <= x1 & x1 <= q by X1, FINSEQ_1: 1;

              x1 <> q by X1, TARSKI:def 1;

              then x1 < (k0 + 1) by X2, XXREAL_0: 1;

              then x1 <= k0 by NAT_1: 13;

              hence x in I0 by X2;

            end;

            then

             DIQ0: I0 = (I \ {q}) by XBOOLE_0:def 5;

            

             NU1: not q in I0

            proof

              assume q in I0;

              then q in I & not q in {q} by DIQ1;

              hence contradiction by TARSKI:def 1;

            end;

            

             XB1: {q} c= I by FINSEQ_1: 4, ZFMISC_1: 31;

            

             NU2: (I0 \/ {q}) = I by DIQ0, XB1, XBOOLE_1: 45;

             <*g0*> is FinSequence of G by FINSEQ_1: 74;

            then

             VV1: ( rng <*g0*>) c= the carrier of G by FINSEQ_1:def 4;

            n0 is Element of NAT by ORDINAL1:def 12;

            then <*n0*> is FinSequence of NAT by FINSEQ_1: 74;

            then

             VV2: ( rng <*n0*>) c= NAT by FINSEQ_1:def 4;

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

            then

             VV4: ( rng a0) c= the carrier of G by XBOOLE_1: 1;

            ( rng (a0 ^ <*g0*>)) = (( rng a0) \/ ( rng <*g0*>)) by FINSEQ_1: 31;

            then

            reconsider a = (a0 ^ <*g0*>) as q -element FinSequence of G by VV1, VV4, XBOOLE_1: 8, FINSEQ_1:def 4;

            ( rng (Inda0 ^ <*n0*>)) = (( rng Inda0) \/ ( rng <*n0*>)) by FINSEQ_1: 31;

            then

            reconsider Inda = (Inda0 ^ <*n0*>) as q -element FinSequence of NAT by VV2, XBOOLE_1: 8, FINSEQ_1:def 4;

            

             LL1: ( len a0) = k0 by CARD_1:def 7;

            

             LL2: ( len Inda0) = k0 by CARD_1:def 7;

            

             EX1: for i be Nat st 1 <= i & i <= (q - 1) holds (Inda . i) <= (Inda . (i + 1))

            proof

              let i be Nat;

              assume

               EX11: 1 <= i & i <= (q - 1);

              

               EX13: ( dom Inda0) = I0 by LL2, FINSEQ_1:def 3;

              1 <= k0 by NAT_1: 14;

              then (k0 - 1) in NAT by INT_1: 3, XREAL_1: 48;

              then

              reconsider k01 = (k0 - 1) as Nat;

              per cases ;

                suppose

                 C1: i <> (q - 1);

                then i < k0 by EX11, XXREAL_0: 1;

                then

                 C2: (i + 1) <= ((k0 - 1) + 1) by NAT_1: 13;

                i < (k01 + 1) by C1, EX11, XXREAL_0: 1;

                then

                 C6: i <= k01 by NAT_1: 13;

                i in ( Seg k0) by EX11;

                then

                 D56: (Inda . i) = (Inda0 . i) by EX13, FINSEQ_1:def 7;

                1 <= (i + 1) by NAT_1: 11;

                then (i + 1) in ( Seg k0) by C2;

                then (Inda . (i + 1)) = (Inda0 . (i + 1)) by EX13, FINSEQ_1:def 7;

                hence (Inda . i) <= (Inda . (i + 1)) by D56, P12, C6, EX11;

              end;

                suppose

                 C2: i = (q - 1);

                i in ( Seg k0) by EX11;

                then (Inda . i) = (Inda0 . i) by EX13, FINSEQ_1:def 7;

                hence (Inda . i) <= (Inda . (i + 1)) by C2, INDK1, LL2, FINSEQ_1: 42;

              end;

            end;

            

             D1: ( dom F) = (( dom F0) \/ ( dom ( {q} --> K))) by FUNCT_4:def 1

            .= (I0 \/ ( dom ( {q} --> K))) by PARTFUN1:def 2

            .= (I0 \/ {q});

            then

            reconsider F as I -defined Function by NU2, RELAT_1:def 18;

            reconsider F as ManySortedSet of I by NU2, PARTFUN1:def 2, D1;

            for y be set st y in ( rng F) holds y is non empty multMagma

            proof

              let y be set;

              assume y in ( rng F);

              then

              consider x be object such that

               D4: x in ( dom F) & y = (F . x) by FUNCT_1:def 3;

              

               F5: x in (( dom F0) \/ ( dom ( {q} --> K))) by D4, FUNCT_4:def 1;

              per cases by XBOOLE_0:def 3, D4, D1;

                suppose

                 D51: x in I0;

                then not x in ( dom ( {q} --> K)) by DIQ1;

                then

                 D52: (F . x) = (F0 . x) by FUNCT_4:def 1, F5;

                x in ( dom F0) by D51, PARTFUN1:def 2;

                then (F0 . x) in ( rng F0) by FUNCT_1: 3;

                hence y is non empty multMagma by D52, D4, GROUP_7:def 1;

              end;

                suppose

                 D52: x in {q};

                then (F . x) = (( {q} --> K) . x) by FUNCT_4:def 1, F5;

                hence y is non empty multMagma by D4, D52, FUNCOP_1: 7;

              end;

            end;

            then

            reconsider F as multMagma-Family of I by GROUP_7:def 1;

            

             P12A: for x be Element of I0 holds (F0 . x) is strict finite commutative Group & (F0 . x) is Subgroup of H

            proof

              let x be Element of I0;

              reconsider i = x as Nat;

              consider ai be Element of H such that

               X1: ai = (a0 . i) & (F0 . i) = ( gr {ai}) & ( ord ai) = (p |^ (Inda0 . i)) by P12;

              thus (F0 . x) is strict finite commutative Group & (F0 . x) is Subgroup of H by X1;

            end;

            

             XPF: for i be Nat st i in I holds ex ai be Element of G st ai = (a . i) & (F . i) = ( gr {ai}) & ( ord ai) = (p |^ (Inda . i))

            proof

              let i be Nat;

              assume

               DD: i in I;

              

               F5: i in (( dom F0) \/ ( dom ( {q} --> K))) by D1, DD, NU2, FUNCT_4:def 1;

              per cases by DD, NU2, XBOOLE_0:def 3;

                suppose

                 D51: i in I0;

                then not i in ( dom ( {q} --> K)) by DIQ1;

                then

                 D52: (F . i) = (F0 . i) by F5, FUNCT_4:def 1;

                consider ai be Element of H such that

                 D53: ai = (a0 . i) & (F0 . i) = ( gr {ai}) & ( ord ai) = (p |^ (Inda0 . i)) by P12, D51;

                ai in H;

                then

                reconsider aai = ai as Element of G by GROUP_2: 40, STRUCT_0:def 5;

                

                 D54: ( gr {aai}) = ( gr {ai}) by GR_CY_2: 3;

                

                 D55: ( ord aai) = ( card ( gr {aai})) by GR_CY_1: 7

                .= ( ord ai) by D54, GR_CY_1: 7;

                ( dom Inda0) = I0 by LL2, FINSEQ_1:def 3;

                then

                 D56: (Inda . i) = (Inda0 . i) by D51, FINSEQ_1:def 7;

                ( dom a0) = I0 by LL1, FINSEQ_1:def 3;

                then (a . i) = (a0 . i) by D51, FINSEQ_1:def 7;

                hence ex ai be Element of G st ai = (a . i) & (F . i) = ( gr {ai}) & ( ord ai) = (p |^ (Inda . i)) by D52, D53, D54, D55, D56;

              end;

                suppose

                 D52: i in {q};

                

                 D55: (F . i) = (( {q} --> K) . i) by FUNCT_4:def 1, F5, D52

                .= ( gr {g0}) by D52, FUNCOP_1: 7;

                

                 D56: i = q by TARSKI:def 1, D52;

                

                 D57: (a . i) = g0 by LL1, FINSEQ_1: 42, D56;

                ( ord g0) = (p |^ (Inda . i)) by P8, D56, LL2, FINSEQ_1: 42;

                hence ex ai be Element of G st ai = (a . i) & (F . i) = ( gr {ai}) & ( ord ai) = (p |^ (Inda . i)) by D55, D57;

              end;

            end;

            

             XPFA: for x be Element of I holds (F . x) is strict finite commutative Group & (F . x) is Subgroup of G

            proof

              let x be Element of I;

              reconsider i = x as Nat;

              consider ai be Element of G such that

               X1: ai = (a . i) & (F . i) = ( gr {ai}) & ( ord ai) = (p |^ (Inda . i)) by XPF;

              thus thesis by X1;

            end;

            

             AR1: for i be Element of I holds (F . i) is Group-like by XPFA;

            

             AR2: for i be Element of I holds (F . i) is associative by XPFA;

            for i be Element of I holds (F . i) is commutative by XPFA;

            then

            reconsider F as associative Group-like commutative multMagma-Family of I by AR1, GROUP_7:def 6, AR2, GROUP_7:def 7, GROUP_7:def 8;

            consider FHKG be Homomorphism of ( product <*H, K*>), G such that

             XX1: FHKG is bijective & for a,b be Element of G st a in H & b in K holds (FHKG . <*a, b*>) = (a * b) by P8;

            

             XF1: F = (F0 +* (q .--> K));

            then

            consider FHK be Homomorphism of ( product F), ( product <*H, K*>) such that

             D7: FHK is bijective & for x0 be Function, k be Element of K, h be Element of H st h = (HFG0 . x0) & x0 in ( product F0) holds (FHK . (x0 +* (q .--> k))) = <*h, k*> by GROUP_17: 28, P12, NU0, NU2, NU1;

            reconsider HFG = (FHKG * FHK) as Function of ( product F), G;

            

             XX2: HFG is onto by FUNCT_2: 27, XX1, D7;

            reconsider HFG as Homomorphism of ( product F), G;

            

             DX2: for x be the carrier of G -valued totalI -defined Function st for p be Element of I holds (x . p) in (F . p) holds x in ( product F) & (HFG . x) = ( Product x)

            proof

              let x be the carrier of G -valued totalI -defined Function;

              assume

               U1: for p be Element of I holds (x . p) in (F . p);

              then x in the carrier of ( product F) by GROUP_17: 29;

              then

              consider x0 be totalI0 -defined Function, k be Element of K such that

               U3: x0 in ( product F0) & x = (x0 +* (q .--> k)) & for p be Element of I0 holds (x0 . p) in (F0 . p) by XF1, GROUP_17: 30, NU2, NU1, NU0;

              reconsider h = (HFG0 . x0) as Element of H by FUNCT_2: 5, U3;

              reconsider hh = h, kk = k as Element of G by GROUP_2: 42;

              now

                let y be object;

                assume y in ( rng x0);

                then

                consider z be object such that

                 DX11: z in ( dom x0) & y = (x0 . z) by FUNCT_1:def 3;

                reconsider z as Element of I0 by DX11;

                

                 DX13: (x0 . z) in (F0 . z) by U3;

                (F0 . z) is Subgroup of H by P12A;

                hence y in the carrier of H by DX11, STRUCT_0:def 5, DX13, GROUP_2: 40;

              end;

              then

              reconsider x0 as the carrier of H -valued totalI0 -defined Function by RELAT_1:def 19, TARSKI:def 3;

              

               U5: (HFG0 . x0) = ( Product x0) by P12, U3;

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

              then ( rng x0) c= the carrier of G by XBOOLE_1: 1;

              then

              reconsider xx0 = x0 as the carrier of G -valued totalI0 -defined Function by RELAT_1:def 19;

              

               U50: ( Product x0) = ( Product xx0) by GROUP_17: 32;

              thus x in ( product F) by GROUP_17: 29, U1;

              

               U6: hh in H & kk in K;

              

              thus (HFG . x) = (FHKG . (FHK . x)) by FUNCT_2: 15, GROUP_17: 29, U1

              .= (FHKG . <*hh, kk*>) by D7, U3

              .= (hh * kk) by XX1, U6

              .= ( Product x) by U5, U50, NU0, NU2, NU1, GROUP_17: 33, U3;

            end;

            for s,t be Element of I st s <> t holds (the carrier of (F . s) /\ the carrier of (F . t)) = {( 1_ G)}

            proof

              let s,t be Element of I;

              assume

               AA1: s <> t;

              ( dom F) = I by PARTFUN1:def 2;

              then

               D4: s in ( dom F) & t in ( dom F);

              per cases ;

                suppose s in I0 & t in I0;

                then

                reconsider ss = s, tt = t as Element of I0;

                

                 F5: s in (( dom F0) \/ ( dom ( {q} --> K))) by D4, FUNCT_4:def 1;

                

                 K5: t in (( dom F0) \/ ( dom ( {q} --> K))) by D4, FUNCT_4:def 1;

                 not ss in ( dom ( {q} --> K)) by DIQ1;

                then

                 D52: (F . ss) = (F0 . ss) by FUNCT_4:def 1, F5;

                 not tt in ( dom ( {q} --> K)) by DIQ1;

                then

                 K52: (F . tt) = (F0 . tt) by FUNCT_4:def 1, K5;

                (the carrier of (F0 . ss) /\ the carrier of (F0 . tt)) = {( 1_ H)} by P12, AA1;

                hence (the carrier of (F . s) /\ the carrier of (F . t)) = {( 1_ G)} by D52, K52, GROUP_2: 44;

              end;

                suppose

                 AA3: not (s in I0 & t in I0);

                thus (the carrier of (F . s) /\ the carrier of (F . t)) = {( 1_ G)}

                proof

                  per cases by AA3;

                    suppose

                     AA31: not s in I0;

                    

                     F5: s in (( dom F0) \/ ( dom ( {q} --> K))) by D4, FUNCT_4:def 1;

                    

                     D52: s in {q} by AA31, DIQ1;

                    then (F . s) = (( {q} --> K) . s) by FUNCT_4:def 1, F5;

                    then

                     D55: (F . s) = K by D52, FUNCOP_1: 7;

                    t in I0

                    proof

                      assume not t in I0;

                      then not t in I or t in {q} by DIQ1;

                      then t = q by TARSKI:def 1;

                      hence contradiction by AA1, TARSKI:def 1, D52;

                    end;

                    then

                    reconsider tt = t as Element of I0;

                    

                     K5: tt in (( dom F0) \/ ( dom ( {q} --> K))) by D4, FUNCT_4:def 1;

                     not tt in ( dom ( {q} --> K)) by DIQ1;

                    then

                     K52: (F . tt) = (F0 . tt) by FUNCT_4:def 1, K5;

                    reconsider S1 = (F0 . tt) as Subgroup of H by P12A;

                    

                     K55: (the carrier of K /\ the carrier of S1) c= {( 1_ G)} by P8, XBOOLE_1: 26, GROUP_2:def 5;

                    

                     K56: ( 1_ G) in the carrier of K by GROUP_2: 46, STRUCT_0:def 5;

                    ( 1_ G) in the carrier of S1 by GROUP_2: 46, STRUCT_0:def 5;

                    then ( 1_ G) in (the carrier of K /\ the carrier of S1) by XBOOLE_0:def 4, K56;

                    then {( 1_ G)} c= (the carrier of K /\ the carrier of S1) by ZFMISC_1: 31;

                    hence (the carrier of (F . s) /\ the carrier of (F . t)) = {( 1_ G)} by D55, K52, K55, XBOOLE_0:def 10;

                  end;

                    suppose

                     AA32: not t in I0;

                    

                     F5: t in (( dom F0) \/ ( dom ( {q} --> K))) by D4, FUNCT_4:def 1;

                    

                     D52: t in {q} by AA32, DIQ1;

                    then (F . t) = (( {q} --> K) . t) by FUNCT_4:def 1, F5;

                    then

                     D55: (F . t) = K by D52, FUNCOP_1: 7;

                    s in I0

                    proof

                      assume not s in I0;

                      then not s in I or s in {q} by DIQ1;

                      then s = q by TARSKI:def 1;

                      hence contradiction by AA1, TARSKI:def 1, D52;

                    end;

                    then

                    reconsider ss = s as Element of I0;

                    

                     K5: ss in (( dom F0) \/ ( dom ( {q} --> K))) by D4, FUNCT_4:def 1;

                     not ss in ( dom ( {q} --> K)) by DIQ1;

                    then

                     K52: (F . ss) = (F0 . ss) by FUNCT_4:def 1, K5;

                    reconsider S1 = (F0 . ss) as Subgroup of H by P12A;

                    

                     K55: (the carrier of K /\ the carrier of S1) c= {( 1_ G)} by P8, XBOOLE_1: 26, GROUP_2:def 5;

                    

                     K56: ( 1_ G) in the carrier of K by GROUP_2: 46, STRUCT_0:def 5;

                    ( 1_ G) in the carrier of S1 by GROUP_2: 46, STRUCT_0:def 5;

                    then ( 1_ G) in (the carrier of K /\ the carrier of S1) by XBOOLE_0:def 4, K56;

                    then {( 1_ G)} c= (the carrier of K /\ the carrier of S1) by ZFMISC_1: 31;

                    hence (the carrier of (F . s) /\ the carrier of (F . t)) = {( 1_ G)} by D55, K52, K55, XBOOLE_0:def 10;

                  end;

                end;

              end;

            end;

            hence thesis by EX1, XPF, XX2, XX1, D7, DX2;

          end;

        end;

      end;

      for k be Nat holds P[k] from NAT_1:sch 4( P1);

      hence thesis;

    end;

    

     XLM18Th401: for I be non empty finite set, F be associative Group-like multMagma-Family of I, x be set st x in the carrier of ( product F) holds x is totalI -defined Function

    proof

      let I be non empty finite set, F be associative Group-like multMagma-Family of I, x be set;

      assume

       A1: x in the carrier of ( product F);

      

       D1: ( dom ( Carrier F)) = I by PARTFUN1:def 2;

      the carrier of ( product F) = ( product ( Carrier F)) by GROUP_7:def 2;

      then

      consider f be Function such that

       D2: x = f & ( dom f) = ( dom ( Carrier F)) & for y be object st y in ( dom ( Carrier F)) holds (f . y) in (( Carrier F) . y) by CARD_3:def 5, A1;

      thus thesis by D2, D1, RELAT_1:def 18, PARTFUN1:def 2;

    end;

    

     XLM18Th402: for I be non empty finite set, F be associative Group-like multMagma-Family of I, f be Function st f in the carrier of ( product F) holds for x be set st x in I holds ex R be non empty multMagma st R = (F . x) & (f . x) in the carrier of R

    proof

      let I be non empty finite set, F be associative Group-like multMagma-Family of I, f be Function;

      assume

       A1: f in the carrier of ( product F);

      

       D1: ( dom ( Carrier F)) = I by PARTFUN1:def 2;

      the carrier of ( product F) = ( product ( Carrier F)) by GROUP_7:def 2;

      then

      consider g be Function such that

       D2: f = g & ( dom g) = ( dom ( Carrier F)) & for y be object st y in ( dom ( Carrier F)) holds (g . y) in (( Carrier F) . y) by CARD_3:def 5, A1;

      let x be set;

      assume

       A2: x in I;

      consider R be 1-sorted such that

       A4: R = (F . x) & (( Carrier F) . x) = the carrier of R by PRALG_1:def 15, A2;

      x in ( dom F) by A2, PARTFUN1:def 2;

      then R in ( rng F) by A4, FUNCT_1: 3;

      then R is non empty multMagma by GROUP_7:def 1;

      hence thesis by A2, D2, D1, A4;

    end;

    theorem :: GROUP_18:21

    for G be strict finite commutative Group, p be Prime, m be Nat st ( card G) = (p |^ m) holds ex k be non zero Nat, a be k -element FinSequence of G, Inda be k -element FinSequence of NAT , F be associative Group-like commutative multMagma-Family of ( Seg k) st (for i be Nat st i in ( Seg k) holds ex ai be Element of G st ai = (a . i) & (F . i) = ( gr {ai}) & ( ord ai) = (p |^ (Inda . i))) & (for i be Nat st 1 <= i & i <= (k - 1) holds (Inda . i) <= (Inda . (i + 1))) & (for p,q be Element of ( Seg k) st p <> q holds (the carrier of (F . p) /\ the carrier of (F . q)) = {( 1_ G)}) & (for y be Element of G holds ex x be the carrier of G -valued total( Seg k) -defined Function st (for p be Element of ( Seg k) holds (x . p) in (F . p)) & y = ( Product x)) & for x1,x2 be the carrier of G -valued total( Seg k) -defined Function st (for p be Element of ( Seg k) holds (x1 . p) in (F . p)) & (for p be Element of ( Seg k) holds (x2 . p) in (F . p)) & ( Product x1) = ( Product x2) holds x1 = x2

    proof

      let G be strict finite commutative Group, p be Prime, m be Nat;

      assume ( card G) = (p |^ m);

      then

      consider k be non zero Nat, a be k -element FinSequence of G, Inda be k -element FinSequence of NAT , F be associative Group-like commutative multMagma-Family of ( Seg k), HFG be Homomorphism of ( product F), G such that

       P1: (for i be Nat st i in ( Seg k) holds ex ai be Element of G st ai = (a . i) & (F . i) = ( gr {ai}) & ( ord ai) = (p |^ (Inda . i))) & (for i be Nat st 1 <= i & i <= (k - 1) holds (Inda . i) <= (Inda . (i + 1))) & (for p,q be Element of ( Seg k) st p <> q holds (the carrier of (F . p) /\ the carrier of (F . q)) = {( 1_ G)}) & HFG is bijective & for x be the carrier of G -valued total( Seg k) -defined Function st for p be Element of ( Seg k) holds (x . p) in (F . p) holds x in ( product F) & (HFG . x) = ( Product x) by LM205A;

      set I = ( Seg k);

      

       P4: for y be Element of G holds ex x be the carrier of G -valued totalI -defined Function st (for p be Element of I holds (x . p) in (F . p)) & y = ( Product x)

      proof

        let y be Element of G;

        y in the carrier of G;

        then y in ( rng HFG) by P1, FUNCT_2:def 3;

        then

        consider x be object such that

         P2: x in the carrier of ( product F) & y = (HFG . x) by FUNCT_2: 11;

        reconsider x as totalI -defined Function by P2, XLM18Th401;

        

         P3: for p be Element of I holds (x . p) in (F . p)

        proof

          let p be Element of I;

          consider R be non empty multMagma such that

           P4: R = (F . p) & (x . p) in the carrier of R by XLM18Th402, P2;

          thus (x . p) in (F . p) by P4;

        end;

        ( rng x) c= the carrier of G

        proof

          let y be object;

          assume y in ( rng x);

          then

          consider i be object such that

           D2: i in ( dom x) & y = (x . i) by FUNCT_1:def 3;

          reconsider i as Element of I by D2;

          consider R be non empty multMagma such that

           P4: R = (F . i) & (x . i) in the carrier of R by P2, XLM18Th402;

          reconsider i0 = i as Nat;

          consider ai be Element of G such that

           XX2: ai = (a . i0) & (F . i0) = ( gr {ai}) & ( ord ai) = (p |^ (Inda . i0)) by P1;

          the carrier of (F . i) c= the carrier of G by XX2, GROUP_2:def 5;

          hence y in the carrier of G by D2, P4;

        end;

        then

        reconsider x as the carrier of G -valued totalI -defined Function by RELAT_1:def 19;

        take x;

        thus thesis by P1, P2, P3;

      end;

      now

        let x1,x2 be the carrier of G -valued totalI -defined Function;

        assume

         AS2: (for p be Element of I holds (x1 . p) in (F . p)) & (for p be Element of I holds (x2 . p) in (F . p)) & ( Product x1) = ( Product x2);

        x1 in ( product F) & (HFG . x1) = ( Product x1) by AS2, P1;

        then

         P4: (HFG . x1) = (HFG . x2) by AS2, P1;

        x1 in the carrier of ( product F) & x2 in the carrier of ( product F) by AS2, P1, STRUCT_0:def 5;

        hence x1 = x2 by P4, P1, FUNCT_2: 19;

      end;

      hence thesis by P1, P4;

    end;