group_17.miz



    begin

    theorem :: GROUP_17:1

    

     Th1: for A,B,A1,B1 be set st A misses B & A1 c= A & B1 c= B & (A1 \/ B1) = (A \/ B) holds A1 = A & B1 = B

    proof

      let A,B,A1,B1 be set;

      assume

       A1: A misses B;

      assume

       A2: A1 c= A & B1 c= B;

      assume

       A3: (A1 \/ B1) = (A \/ B);

      

       A4: A c= A1

      proof

        let x be object;

        assume

         A5: x in A;

        then

         A6: x in (A \/ B) by XBOOLE_0:def 3;

         not x in B1

        proof

          assume x in B1;

          then x in (A /\ B) by A5, XBOOLE_0:def 4, A2;

          hence contradiction by A1, XBOOLE_0:def 7;

        end;

        hence x in A1 by A6, XBOOLE_0:def 3, A3;

      end;

      B c= B1

      proof

        let x be object;

        assume

         A7: x in B;

        then

         A8: x in (A \/ B) by XBOOLE_0:def 3;

         not x in A1

        proof

          assume x in A1;

          then x in (A /\ B) by A7, XBOOLE_0:def 4, A2;

          hence contradiction by A1, XBOOLE_0:def 7;

        end;

        hence x in B1 by A8, XBOOLE_0:def 3, A3;

      end;

      hence thesis by A2, XBOOLE_0:def 10, A4;

    end;

    theorem :: GROUP_17:2

    

     Th2: for H,K be non empty finite set holds ( card ( product <*H, K*>)) = (( card H) * ( card K))

    proof

      let H,K be non empty finite set;

      consider I be Function of [:H, K:], ( product <*H, K*>) such that

       A1: I is one-to-one onto & for x,y be object st x in H & y in K holds (I . (x,y)) = <*x, y*> by PRVECT_3: 5;

      

       A2: ( dom I) = [:H, K:] by FUNCT_2:def 1;

      ( rng I) = ( product <*H, K*>) by FUNCT_2:def 3, A1;

      then ( card [:H, K:]) = ( card ( product <*H, K*>)) by CARD_1: 5, A1, A2, WELLORD2:def 4;

      hence thesis by CARD_2: 46;

    end;

    theorem :: GROUP_17:3

    

     Th3: for ps,pt,f be bag of SetPrimes , q be Nat st ( support ps) misses ( support pt) & f = (ps + pt) & q in ( support ps) holds (ps . q) = (f . q)

    proof

      let ps,pt,f be bag of SetPrimes , q be Nat;

      assume

       A1: ( support ps) misses ( support pt) & f = (ps + pt) & q in ( support ps);

      then (( support ps) /\ ( support pt)) = {} by XBOOLE_0:def 7;

      then

       A2: not q in ( support pt) by A1, XBOOLE_0:def 4;

      

      thus (f . q) = ((ps . q) + (pt . q)) by A1, PRE_POLY:def 5

      .= ((ps . q) + 0 ) by A2, PRE_POLY:def 7

      .= (ps . q);

    end;

    theorem :: GROUP_17:4

    

     Th4: for ps,pt,f be bag of SetPrimes , q be Nat st ( support ps) misses ( support pt) & f = (ps + pt) & q in ( support pt) holds (pt . q) = (f . q)

    proof

      let ps,pt,f be bag of SetPrimes , q be Nat;

      assume

       A1: ( support ps) misses ( support pt) & f = (ps + pt) & q in ( support pt);

      then (( support ps) /\ ( support pt)) = {} by XBOOLE_0:def 7;

      then

       A2: not q in ( support ps) by A1, XBOOLE_0:def 4;

      

      thus (f . q) = ((ps . q) + (pt . q)) by A1, PRE_POLY:def 5

      .= ( 0 + (pt . q)) by A2, PRE_POLY:def 7

      .= (pt . q);

    end;

    

     Lm1: for ps,pt,f be bag of SetPrimes st ps is prime-factorization-like & pt is prime-factorization-like & f = (ps + pt) & ( support ps) misses ( support pt) holds f is prime-factorization-like

    proof

      let ps,pt,f be bag of SetPrimes ;

      assume

       A1: ps is prime-factorization-like;

      assume

       A2: pt is prime-factorization-like;

      assume

       A3: f = (ps + pt);

      assume

       A4: ( support ps) misses ( support pt);

      

       A5: ( support f) = (( support ps) \/ ( support pt)) by A3, PRE_POLY: 38;

      for x be Prime st x in ( support f) holds ex n be Nat st 0 < n & (f . x) = (x |^ n)

      proof

        let x be Prime;

        assume

         A6: x in ( support f);

        per cases by A6, A5, XBOOLE_0:def 3;

          suppose

           A7: x in ( support ps);

          (ps . x) = (f . x) by A3, A4, A7, Th3;

          hence thesis by A7, A1, INT_7:def 1;

        end;

          suppose

           A8: x in ( support pt);

          (pt . x) = (f . x) by A3, A4, A8, Th4;

          hence thesis by A8, A2, INT_7:def 1;

        end;

      end;

      hence thesis by INT_7:def 1;

    end;

    theorem :: GROUP_17:5

    

     Th5: for h be non zero Nat, q be Prime st not (q,h) are_coprime holds q divides h

    proof

      let h be non zero Nat, q be Prime;

      set pq = ( prime_factorization q);

      set ph = ( prime_factorization h);

      

       A1: q = ( Product pq) by NAT_3: 61;

      

       A2: h = ( Product ph) by NAT_3: 61;

      assume not (q,h) are_coprime ;

      then (( support pq) /\ ( support ph)) <> {} by XBOOLE_0:def 7, INT_7: 12, A1, A2;

      then (( support ( pfexp q)) /\ ( support ph)) <> {} by NAT_3:def 9;

      then (( support ( pfexp q)) /\ ( support ( pfexp h))) <> {} by NAT_3:def 9;

      then ( {q} /\ ( support ( pfexp h))) <> {} by NAT_3: 43;

      then

      consider x be object such that

       A3: x in ( {q} /\ ( support ( pfexp h))) by XBOOLE_0:def 1;

      

       A4: x in {q} & x in ( support ( pfexp h)) by A3, XBOOLE_0:def 4;

      x = q by A4, TARSKI:def 1;

      hence q divides h by NAT_3: 36, A4;

    end;

    theorem :: GROUP_17:6

    

     Th6: for h,s be non zero Nat st for q be Prime st q in ( support ( prime_factorization s)) holds not (q,h) are_coprime holds ( support ( prime_factorization s)) c= ( support ( prime_factorization h))

    proof

      let h,s be non zero Nat;

      assume

       A1: for q be Prime st q in ( support ( prime_factorization s)) holds not (q,h) are_coprime ;

      let x be object;

      assume

       A2: x in ( support ( prime_factorization s));

      then

      reconsider q = x as Prime by NEWTON:def 6;

      q divides h by Th5, A2, A1;

      then q in ( support ( pfexp h)) by ORDINAL1:def 13, NAT_3: 37;

      hence thesis by NAT_3:def 9;

    end;

    theorem :: GROUP_17:7

    

     Th7: for h,k,s,t be non zero Nat st (h,k) are_coprime & (s * t) = (h * k) & (for q be Prime st q in ( support ( prime_factorization s)) holds not (q,h) are_coprime ) & (for q be Prime st q in ( support ( prime_factorization t)) holds not (q,k) are_coprime ) holds s = h & t = k

    proof

      let h,k,s,t be non zero Nat;

      assume

       A1: (h,k) are_coprime ;

      assume

       A2: (s * t) = (h * k);

      assume

       A3: for q be Prime st q in ( support ( prime_factorization s)) holds not (q,h) are_coprime ;

      assume

       A4: for q be Prime st q in ( support ( prime_factorization t)) holds not (q,k) are_coprime ;

      set ps = ( prime_factorization s);

      set ph = ( prime_factorization h);

      set pt = ( prime_factorization t);

      set pk = ( prime_factorization k);

      

       A5: ( support ps) c= ( support ph) by A3, Th6;

      

       A6: ( support pt) c= ( support pk) by A4, Th6;

      ( support ( pfexp h)) misses ( support ( pfexp k)) by NAT_3: 44, A1;

      then ( support ph) misses ( support ( pfexp k)) by NAT_3:def 9;

      then

       A7: ( support ph) misses ( support pk) by NAT_3:def 9;

      set f = (ps + pt);

      set g = (ph + pk);

      

       A8: f is prime-factorization-like by A7, A5, A6, XBOOLE_1: 64, Lm1;

      

       A9: g is prime-factorization-like by A7, Lm1;

      

       A10: ( Product g) = (( Product ph) * ( Product pk)) by A7, NAT_3: 19

      .= (h * ( Product pk)) by NAT_3: 61

      .= (h * k) by NAT_3: 61;

      

       A11: ( Product f) = (( Product ps) * ( Product pt)) by A5, A6, XBOOLE_1: 64, A7, NAT_3: 19

      .= (s * ( Product pt)) by NAT_3: 61

      .= (s * t) by NAT_3: 61;

      (( support ps) \/ ( support pt)) = ( support f) by PRE_POLY: 38

      .= ( support g) by A11, INT_7: 15, A8, A9, A10, A2

      .= (( support ph) \/ ( support pk)) by PRE_POLY: 38;

      then

       A12: ( support ps) = ( support ph) & ( support pt) = ( support pk) by A5, A6, A7, Th1;

      

       A13: ( support ps) = ( support ( pfexp h)) by A12, NAT_3:def 9;

      

       A14: ( support pt) = ( support ( pfexp k)) by A12, NAT_3:def 9;

      

       A15: for p be Nat st p in ( support ( pfexp h)) holds (ps . p) = (p |^ (p |-count h))

      proof

        let p be Nat;

        assume

         A16: p in ( support ( pfexp h));

        then

         A17: p in ( support ph) by NAT_3:def 9;

        

         A18: p in ( support ps) by A16, A12, NAT_3:def 9;

        

        thus (ps . p) = (f . p) by Th3, A18, A5, A6, XBOOLE_1: 64, A7

        .= (ph . p) by Th3, A17, A7, INT_7: 15, A8, A9, A10, A2, A11

        .= (p |^ (p |-count h)) by A16, NAT_3:def 9;

      end;

      

       A19: for p be Nat st p in ( support ( pfexp k)) holds (pt . p) = (p |^ (p |-count k))

      proof

        let p be Nat;

        assume

         A20: p in ( support ( pfexp k));

        then

         A21: p in ( support pk) by NAT_3:def 9;

        

         A22: p in ( support pt) by A12, A20, NAT_3:def 9;

        

        thus (pt . p) = (f . p) by Th4, A22, A5, A6, XBOOLE_1: 64, A7

        .= (pk . p) by Th4, A21, A7, A11, INT_7: 15, A8, A9, A10, A2

        .= (p |^ (p |-count k)) by A20, NAT_3:def 9;

      end;

      

      thus s = ( Product ps) by NAT_3: 61

      .= ( Product ph) by A15, A13, NAT_3:def 9

      .= h by NAT_3: 61;

      

      thus t = ( Product pt) by NAT_3: 61

      .= ( Product pk) by A19, A14, NAT_3:def 9

      .= k by NAT_3: 61;

    end;

    

     Lm2: for G be non empty multMagma, I be non empty finite set, b be the carrier of G -valued totalI -defined Function holds (b * ( canFS I)) is FinSequence of G & ( dom (b * ( canFS I))) = ( Seg ( card I))

    proof

      let G be non empty multMagma, I be non empty finite set, b be the carrier of G -valued totalI -defined Function;

      set cS = ( canFS I);

      set f = (b * cS);

      

       A1: ( rng f) c= the carrier of G;

      I = ( dom b) & ( rng cS) = I by FUNCT_2:def 3, PARTFUN1:def 2;

      then

       A2: ( dom f) = ( dom cS) by RELAT_1: 27;

      then ( dom f) = ( Seg ( len cS)) by FINSEQ_1:def 3;

      then f is FinSequence by FINSEQ_1:def 2;

      then

      reconsider f as FinSequence of G by A1, FINSEQ_1:def 4;

      ( len ( canFS I)) = ( card I) by FINSEQ_1: 93;

      then ( dom f) = ( Seg ( card I)) by A2, FINSEQ_1:def 3;

      hence thesis;

    end;

    

     Lm3: for A,B be non empty finite set st A misses B holds (( canFS A) ^ ( canFS B)) is one-to-one onto FinSequence of (A \/ B) & ( dom (( canFS A) ^ ( canFS B))) = ( Seg ( card (A \/ B)))

    proof

      let A,B be non empty finite set;

      assume

       A1: A misses B;

      

       A2: ( rng ( canFS A)) = A by FUNCT_2:def 3;

      

       A3: ( rng ( canFS B)) = B by FUNCT_2:def 3;

      then

       A4: ( rng (( canFS A) ^ ( canFS B))) = (A \/ B) by FINSEQ_1: 31, A2;

      then

      reconsider f = (( canFS A) ^ ( canFS B)) as FinSequence of (A \/ B) by FINSEQ_1:def 4;

      ( dom f) = ( Seg (( len ( canFS A)) + ( len ( canFS B)))) by FINSEQ_1:def 7

      .= ( Seg (( card A) + ( len ( canFS B)))) by FINSEQ_1: 93

      .= ( Seg (( card A) + ( card B))) by FINSEQ_1: 93

      .= ( Seg ( card (A \/ B))) by A1, CARD_2: 40;

      hence thesis by A2, FINSEQ_3: 91, A1, A3, A4, FUNCT_2:def 3;

    end;

    

     Lm4: for A,B be non empty finite set, FA be totalA -defined Function, FB be totalB -defined Function, f,g be FinSequence, FAB be (A \/ B) -defined Function st A misses B & FAB = (FA +* FB) & f = (FA * ( canFS A)) & g = (FB * ( canFS B)) holds (f ^ g) = (FAB * (( canFS A) ^ ( canFS B)))

    proof

      let A,B be non empty finite set, FA be totalA -defined Function, FB be totalB -defined Function, f,g be FinSequence, FAB be (A \/ B) -defined Function;

      assume

       A1: A misses B;

      assume

       A2: FAB = (FA +* FB);

      assume

       A3: f = (FA * ( canFS A));

      assume

       A4: g = (FB * ( canFS B));

      reconsider csAB = (( canFS A) ^ ( canFS B)) as one-to-one onto FinSequence of (A \/ B) by Lm3, A1;

      set fAB = (FAB * (( canFS A) ^ ( canFS B)));

      set cSA = ( canFS A);

      set cSB = ( canFS B);

      

       A5: A = ( dom FA) & ( rng cSA) = A by FUNCT_2:def 3, PARTFUN1:def 2;

      then

       A6: ( dom f) = ( dom cSA) by A3, RELAT_1: 27;

      then

       A7: ( dom f) = ( Seg ( len cSA)) by FINSEQ_1:def 3;

      

       A8: B = ( dom FB) & ( rng cSB) = B by FUNCT_2:def 3, PARTFUN1:def 2;

      then ( dom g) = ( dom cSB) by A4, RELAT_1: 27;

      then

       A9: ( dom g) = ( Seg ( len cSB)) by FINSEQ_1:def 3;

      

       A10: (A \/ B) = ( dom FAB) by A2, FUNCT_4:def 1, A5, A8;

      ( rng csAB) = (A \/ B) by FUNCT_2:def 3;

      then

       A11: ( dom fAB) = ( dom csAB) by RELAT_1: 27, A10;

      then ( dom fAB) = ( Seg ( len csAB)) by FINSEQ_1:def 3;

      then

      reconsider fAB as FinSequence by FINSEQ_1:def 2;

      

       A12: ( dom fAB) = ( Seg ( card (A \/ B))) by A11, Lm3, A1

      .= ( Seg (( card A) + ( card B))) by A1, CARD_2: 40

      .= ( Seg (( len cSA) + ( card B))) by FINSEQ_1: 93

      .= ( Seg (( len cSA) + ( len cSB))) by FINSEQ_1: 93

      .= ( Seg (( len f) + ( len cSB))) by A7, FINSEQ_1:def 3

      .= ( Seg (( len f) + ( len g))) by A9, FINSEQ_1:def 3;

      

       A13: for k be Nat st k in ( dom f) holds (fAB . k) = (f . k)

      proof

        let k be Nat;

        assume

         A14: k in ( dom f);

        then k in ( dom csAB) by A6, FINSEQ_1: 26, TARSKI:def 3;

        then

         A15: (fAB . k) = (FAB . (csAB . k)) by FUNCT_1: 13;

        

         A16: (csAB . k) = (cSA . k) by A14, A6, FINSEQ_1:def 7;

         not (csAB . k) in ( dom FB)

        proof

          assume

           A17: (csAB . k) in ( dom FB);

          (cSA . k) in ( rng cSA) by A14, A6, FUNCT_1: 3;

          then (csAB . k) in (A /\ B) by A16, A17, XBOOLE_0:def 4;

          hence contradiction by A1, XBOOLE_0:def 7;

        end;

        then (FAB . (csAB . k)) = (FA . (csAB . k)) by A2, FUNCT_4: 11;

        

        hence (fAB . k) = (FA . (cSA . k)) by A15, A14, A6, FINSEQ_1:def 7

        .= (f . k) by A3, A14, A6, FUNCT_1: 13;

      end;

      for k be Nat st k in ( dom g) holds (fAB . (( len f) + k)) = (g . k)

      proof

        let k be Nat;

        assume

         A18: k in ( dom g);

        

         A19: ( len cSA) = ( len f) by A7, FINSEQ_1:def 3;

        

         A20: k in ( dom cSB) by A4, RELAT_1: 27, A8, A18;

        then (( len f) + k) in ( dom csAB) by A19, FINSEQ_1: 28;

        then

         A21: (fAB . (( len f) + k)) = (FAB . (csAB . (( len f) + k))) by FUNCT_1: 13;

        (csAB . (( len f) + k)) = (cSB . k) by A20, A19, FINSEQ_1:def 7;

        

        hence (fAB . (( len f) + k)) = (FB . (cSB . k)) by A21, A20, FUNCT_1: 3, FUNCT_4: 13, A2, A8

        .= (g . k) by A4, A20, FUNCT_1: 13;

      end;

      hence thesis by FINSEQ_1:def 7, A12, A13;

    end;

    definition

      let G be non empty multMagma, I be finite set, b be the carrier of G -valued totalI -defined Function;

      :: GROUP_17:def1

      func Product b -> Element of G means

      : Def1: ex f be FinSequence of G st it = ( Product f) & f = (b * ( canFS I));

      existence

      proof

        set cS = ( canFS I);

        set f = (b * cS);

        

         A1: ( rng f) c= the carrier of G;

        I = ( dom b) & ( rng cS) = I by FUNCT_2:def 3, PARTFUN1:def 2;

        then ( dom f) = ( dom cS) by RELAT_1: 27;

        then ( dom f) = ( Seg ( len cS)) by FINSEQ_1:def 3;

        then f is FinSequence by FINSEQ_1:def 2;

        then

        reconsider f as FinSequence of G by A1, FINSEQ_1:def 4;

        take ( Product f);

        thus thesis;

      end;

      uniqueness ;

    end

    theorem :: GROUP_17:8

    

     Th8: for G be commutative Group, A,B be non empty finite set, FA be the carrier of G -valued totalA -defined Function, FB be the carrier of G -valued totalB -defined Function, FAB be the carrier of G -valued total(A \/ B) -defined Function st A misses B & FAB = (FA +* FB) holds ( Product FAB) = (( Product FA) * ( Product FB))

    proof

      let G be commutative Group, A,B be non empty finite set, FA be the carrier of G -valued totalA -defined Function, FB be the carrier of G -valued totalB -defined Function, FAB be the carrier of G -valued total(A \/ B) -defined Function;

      assume

       A1: A misses B;

      assume

       A2: FAB = (FA +* FB);

      consider fA be FinSequence of G such that

       A3: ( Product FA) = ( Product fA) & fA = (FA * ( canFS A)) by Def1;

      consider fB be FinSequence of G such that

       A4: ( Product FB) = ( Product fB) & fB = (FB * ( canFS B)) by Def1;

      set fAB = (FAB * ( canFS (A \/ B)));

      set cAB = (( canFS A) ^ ( canFS B));

      set uAB = ( canFS (A \/ B));

      reconsider SGAB = ( Seg ( card (A \/ B))) as non empty finite set;

      

       A5: cAB is one-to-one onto FinSequence of (A \/ B) & ( dom cAB) = SGAB by Lm3, A1;

      reconsider cAB as one-to-one onto FinSequence of (A \/ B) by Lm3, A1;

      ( rng cAB) c= (A \/ B);

      then

      reconsider JcAB = cAB as Function of SGAB, (A \/ B) by FUNCT_2: 2, A5;

      

       A6: ( dom uAB) = ( Seg ( len uAB)) by FINSEQ_1:def 3

      .= SGAB by FINSEQ_1: 93;

      ( rng uAB) c= (A \/ B);

      then

      reconsider KuAB = uAB as Function of SGAB, (A \/ B) by FUNCT_2: 2, A6;

      reconsider IuAB = (uAB " ) as Function of (A \/ B), SGAB by FINSEQ_1: 95;

      

       A7: ( rng uAB) = (A \/ B) by FUNCT_2:def 3;

      then (IuAB * KuAB) = ( id SGAB) & (KuAB * IuAB) = ( id (A \/ B)) by FUNCT_2: 29;

      then

       A8: IuAB is one-to-one & IuAB is onto by FUNCT_2: 23;

      set p = (IuAB * JcAB);

      p is onto & p is one-to-one by A8, FUNCT_2: 27;

      then

      reconsider p as Permutation of SGAB;

      reconsider fAB as FinSequence of G by Lm2;

      

       A9: (( canFS (A \/ B)) * p) = ((KuAB * IuAB) * JcAB) by RELAT_1: 36

      .= (( id (A \/ B)) * JcAB) by A7, FUNCT_2: 29

      .= (( canFS A) ^ ( canFS B)) by FUNCT_2: 17;

      

       A10: SGAB = ( dom fAB) by Lm2;

      

       A11: (fA ^ fB) = (FAB * (( canFS A) ^ ( canFS B))) by A3, A4, Lm4, A1, A2

      .= (fAB * p) by RELAT_1: 36, A9;

      

      thus ( Product FAB) = ( Product fAB) by Def1

      .= ( Product (fA ^ fB)) by A10, A11, UPROOTS: 16

      .= (( Product FA) * ( Product FB)) by A3, A4, GROUP_4: 5;

    end;

    theorem :: GROUP_17:9

    

     Th9: for G be non empty multMagma, q be set, z be Element of G, f be the carrier of G -valued total {q} -defined Function st f = (q .--> z) holds ( Product f) = z

    proof

      let G be non empty multMagma, q be set, z be Element of G, f be the carrier of G -valued total {q} -defined Function;

      assume

       A1: f = (q .--> z);

      set zz = <*z*>;

      ( rng zz) = {z} by FINSEQ_1: 38;

      then

      reconsider zz as FinSequence of G by FINSEQ_1:def 4;

      

       A2: (f * ( canFS {q})) is FinSequence of G & ( dom (f * ( canFS {q}))) = ( Seg ( card {q})) by Lm2;

      reconsider g = (f * ( canFS {q})) as FinSequence of G by Lm2;

      

       A3: ( card {q}) = 1 by CARD_1: 30;

      then ( dom g) = ( Seg 1) by Lm2;

      then

       A4: ( len g) = 1 by FINSEQ_1:def 3;

      

       A5: ( canFS {q}) = <*q*> by FINSEQ_1: 94;

      

       A6: q in {q} by TARSKI:def 1;

      

       A7: 1 in ( dom g) by A2, A3;

      (g . 1) = (f . (( canFS {q}) . 1)) by FUNCT_1: 12, A7

      .= (f . q) by A5, FINSEQ_1: 40

      .= z by A1, FUNCOP_1: 7, A6;

      then <*z*> = (f * ( canFS {q})) by A4, FINSEQ_1: 40;

      

      hence ( Product f) = ( Product zz) by Def1

      .= z by GROUP_4: 9;

    end;

    begin

    theorem :: GROUP_17:10

    

     Th10: for X,Y be non empty multMagma holds the carrier of ( product <*X, Y*>) = ( product <*the carrier of X, the carrier of Y*>)

    proof

      let X,Y be non empty multMagma;

      set CarrX = the carrier of X;

      set CarrY = the carrier of Y;

      

       A1: the carrier of ( product <*X, Y*>) = ( product ( Carrier <*X, Y*>)) by GROUP_7:def 2;

      ( len <*CarrX, CarrY*>) = 2 by FINSEQ_1: 44;

      then

       A2: ( dom <*CarrX, CarrY*>) = {1, 2} by FINSEQ_1: 2, FINSEQ_1:def 3;

      

       A3: ( <*X, Y*> . 1) = X & ( <*X, Y*> . 2) = Y by FINSEQ_1: 44;

      for a be object st a in ( dom ( Carrier <*X, Y*>)) holds (( Carrier <*X, Y*>) . a) = ( <*the carrier of X, the carrier of Y*> . a)

      proof

        let a be object;

        assume

         A4: a in ( dom ( Carrier <*X, Y*>));

        per cases by A4, TARSKI:def 2;

          suppose

           A5: a = 1;

          then ex R be 1-sorted st R = ( <*X, Y*> . 1) & (( Carrier <*X, Y*>) . 1) = the carrier of R by A4, PRALG_1:def 15;

          hence thesis by FINSEQ_1: 44, A3, A5;

        end;

          suppose

           A6: a = 2;

          then ex R be 1-sorted st R = ( <*X, Y*> . 2) & (( Carrier <*X, Y*>) . 2) = the carrier of R by A4, PRALG_1:def 15;

          hence thesis by FINSEQ_1: 44, A3, A6;

        end;

      end;

      hence thesis by PARTFUN1:def 2, A2, FUNCT_1: 2, A1;

    end;

    theorem :: GROUP_17:11

    

     Th11: for G be Group, A,B be normal Subgroup of G st (the carrier of A /\ the carrier of B) = {( 1_ G)} holds for a,b be Element of G st a in A & b in B holds (a * b) = (b * a)

    proof

      let G be Group, A,B be normal Subgroup of G;

      assume

       A1: (the carrier of A /\ the carrier of B) = {( 1_ G)};

      let a,b be Element of G;

      assume

       A2: a in A & b in B;

      

       A3: ((a * b) * ((b * a) " )) = ((a * b) * ((a " ) * (b " ))) by GROUP_1: 17

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

      

       A4: (b " ) in B by A2, GROUP_2: 51;

      (a * b) in (a * B) by GROUP_2: 27, A2;

      then (a * b) in (B * a) by GROUP_3: 117;

      then

      consider s be Element of G such that

       A5: (a * b) = (s * a) & s in the carrier of B by GROUP_2: 28;

      ((a * b) * (a " )) in B by GROUP_3: 1, A5;

      then

       A6: ((a * b) * ((b * a) " )) in the carrier of B by STRUCT_0:def 5, A3, A4, GROUP_2: 50;

      

       A7: ((a * b) * ((b * a) " )) = ((a * b) * ((a " ) * (b " ))) by GROUP_1: 17

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

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

      (a " ) in A by A2, GROUP_2: 51;

      then (b * (a " )) in (b * A) by GROUP_2: 27;

      then (b * (a " )) in (A * b) by GROUP_3: 117;

      then

      consider t be Element of G such that

       A8: (b * (a " )) = (t * b) & t in the carrier of A by GROUP_2: 28;

      ((b * (a " )) * (b " )) in A by GROUP_3: 1, A8;

      then ((a * b) * ((b * a) " )) in the carrier of A by STRUCT_0:def 5, A7, A2, GROUP_2: 50;

      then ((a * b) * ((b * a) " )) in (the carrier of A /\ the carrier of B) by XBOOLE_0:def 4, A6;

      then ((a * b) * ((b * a) " )) = ( 1_ G) by A1, TARSKI:def 1;

      then (( 1_ G) * (b * a)) = (a * b) by GROUP_1: 14;

      hence thesis by GROUP_1:def 4;

    end;

    theorem :: GROUP_17:12

    

     Th12: for G be Group, A,B be normal Subgroup of G st (for x be Element of G holds ex a,b be Element of G st a in A & b in B & x = (a * b)) & (the carrier of A /\ the carrier of B) = {( 1_ G)} holds ex h be Homomorphism of ( product <*A, B*>), G st h is bijective & for a,b be Element of G st a in A & b in B holds (h . <*a, b*>) = (a * b)

    proof

      let G be Group, A,B be normal Subgroup of G;

      assume

       A1: for x be Element of G holds ex a,b be Element of G st a in A & b in B & x = (a * b);

      assume

       A2: (the carrier of A /\ the carrier of B) = {( 1_ G)};

      defpred P[ set, set] means ex x be Element of G, y be Element of G st x in A & y in B & $1 = <*x, y*> & $2 = (x * y);

      

       A3: for z be Element of ( product <*A, B*>) holds ex w be Element of G st P[z, w]

      proof

        let z be Element of ( product <*A, B*>);

        consider x be Element of A, y be Element of B such that

         A4: z = <*x, y*> by TOPALG_4: 1;

        reconsider x1 = x, y1 = y as Element of G by GROUP_2: 41, STRUCT_0:def 5;

        

         A5: (x1 * y1) is Element of G;

        x1 in A & y1 in B;

        hence thesis by A4, A5;

      end;

      consider h be Function of ( product <*A, B*>), G such that

       A6: for z be Element of ( product <*A, B*>) holds P[z, (h . z)] from FUNCT_2:sch 3( A3);

      

       A7: for a,b be Element of G st a in A & b in B holds (h . <*a, b*>) = (a * b)

      proof

        let a,b be Element of G;

        assume

         A8: a in A & b in B;

        then

        reconsider a1 = a as Element of A;

        reconsider b1 = b as Element of B by A8;

        consider x be Element of G, y be Element of G such that

         A9: x in A & y in B & <*a1, b1*> = <*x, y*> & (h . <*a1, b1*>) = (x * y) by A6;

        

         A10: a1 = ( <*a1, b1*> . 1) by FINSEQ_1: 44

        .= x by FINSEQ_1: 44, A9;

        b1 = ( <*a1, b1*> . 2) by FINSEQ_1: 44

        .= y by FINSEQ_1: 44, A9;

        hence thesis by A9, A10;

      end;

      now

        let z1,z2 be object;

        assume

         A11: z1 in the carrier of ( product <*A, B*>) & z2 in the carrier of ( product <*A, B*>) & (h . z1) = (h . z2);

        then

        consider x1 be Element of G, y1 be Element of G such that

         A12: x1 in A & y1 in B & z1 = <*x1, y1*> & (h . z1) = (x1 * y1) by A6;

        consider x2 be Element of G, y2 be Element of G such that

         A13: x2 in A & y2 in B & z2 = <*x2, y2*> & (h . z2) = (x2 * y2) by A6, A11;

        x1 = ((x2 * y2) * (y1 " )) by GROUP_1: 14, A13, A11, A12;

        then x1 = (x2 * (y2 * (y1 " ))) by GROUP_1:def 3;

        then

         A14: ((x2 " ) * x1) = (y2 * (y1 " )) by GROUP_1: 13;

        (x2 " ) in A by A13, GROUP_2: 51;

        then

         A15: ((x2 " ) * x1) in the carrier of A by GROUP_2: 50, A12, STRUCT_0:def 5;

        (y1 " ) in B by A12, GROUP_2: 51;

        then (y2 * (y1 " )) in the carrier of B by A13, GROUP_2: 50, STRUCT_0:def 5;

        then

         A16: ((x2 " ) * x1) in (the carrier of A /\ the carrier of B) by A14, A15, XBOOLE_0:def 4;

        then ((x2 " ) * x1) = ( 1_ G) by A2, TARSKI:def 1;

        then x1 = (x2 * ( 1_ G)) by GROUP_1: 13;

        then

         A17: x1 = x2 by GROUP_1:def 4;

        (y2 * (y1 " )) = ( 1_ G) by A2, TARSKI:def 1, A14, A16;

        then y2 = (( 1_ G) * y1) by GROUP_1: 14;

        hence z1 = z2 by A12, A13, A17, GROUP_1:def 4;

      end;

      then

       A18: h is one-to-one by FUNCT_2: 19;

      now

        let w be object;

        assume w in the carrier of G;

        then

        reconsider g = w as Element of G;

        consider a,b be Element of G such that

         A19: a in A & b in B & g = (a * b) by A1;

        reconsider a1 = a as Element of A by A19;

        reconsider b1 = b as Element of B by A19;

        (h . <*a1, b1*>) = (a * b) by A7, A19;

        hence w in ( rng h) by A19, FUNCT_2: 112;

      end;

      then the carrier of G c= ( rng h) by TARSKI:def 3;

      then

       A20: h is onto by FUNCT_2:def 3, XBOOLE_0:def 10;

      for z,w be Element of ( product <*A, B*>) holds (h . (z * w)) = ((h . z) * (h . w))

      proof

        let z,w be Element of ( product <*A, B*>);

        consider x be Element of A, y be Element of B such that

         A21: z = <*x, y*> by TOPALG_4: 1;

        reconsider x1 = x, y1 = y as Element of G by GROUP_2: 41, STRUCT_0:def 5;

        consider a be Element of A, b be Element of B such that

         A22: w = <*a, b*> by TOPALG_4: 1;

        reconsider a1 = a, b1 = b as Element of G by GROUP_2: 41, STRUCT_0:def 5;

        

         A23: (y * b) = (y1 * b1) by GROUP_2: 43;

        

         A24: (z * w) = <*(x * a), (y * b)*> by A21, A22, GROUP_7: 29

        .= <*(x1 * a1), (y1 * b1)*> by GROUP_2: 43, A23;

        

         A25: x1 in A & a1 in A;

        then

         A26: (x1 * a1) in A by GROUP_2: 50;

        

         A27: y1 in B & b1 in B;

        then

         A28: (y1 * b1) in B by GROUP_2: 50;

        

         A29: (h . (z * w)) = ((x1 * a1) * (y1 * b1)) by A7, A24, A26, A28

        .= (x1 * (a1 * (y1 * b1))) by GROUP_1:def 3

        .= (x1 * ((a1 * y1) * b1)) by GROUP_1:def 3

        .= (x1 * ((y1 * a1) * b1)) by Th11, A2, A25, A27

        .= (x1 * (y1 * (a1 * b1))) by GROUP_1:def 3

        .= ((x1 * y1) * (a1 * b1)) by GROUP_1:def 3;

        (h . z) = (x1 * y1) by A21, A7, A25, A27;

        hence (h . (z * w)) = ((h . z) * (h . w)) by A29, A22, A7, A25, A27;

      end;

      then h is Homomorphism of ( product <*A, B*>), G by GROUP_6:def 6;

      hence thesis by A7, A20, A18;

    end;

    theorem :: GROUP_17:13

    

     Th13: for G be finite commutative Group, m be Nat, A be Subset of G st A = { x where x be Element of G : (x |^ m) = ( 1_ G) } holds A <> {} & (for g1,g2 be Element of G st g1 in A & g2 in A holds (g1 * g2) in A) & for g be Element of G st g in A holds (g " ) in A

    proof

      let G be finite commutative Group, m be Nat, A be Subset of G;

      assume

       A1: A = { x where x be Element of G : (x |^ m) = ( 1_ G) };

      (( 1_ G) |^ m) = ( 1_ G) by GROUP_1: 31;

      then

       A2: ( 1_ G) in A by A1;

      

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

      proof

        let g1,g2 be Element of G;

        assume

         A4: g1 in A & g2 in A;

        then

         A5: ex x1 be Element of G st g1 = x1 & (x1 |^ m) = ( 1_ G) by A1;

        

         A6: ex x2 be Element of G st g2 = x2 & (x2 |^ m) = ( 1_ G) by A1, A4;

        ((g1 * g2) |^ m) = ((g1 |^ m) * (g2 |^ m)) by GROUP_1: 38

        .= ( 1_ G) by GROUP_1:def 4, A5, A6;

        hence (g1 * g2) in A by A1;

      end;

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

      proof

        let g be Element of G;

        assume g in A;

        then

         A7: ex x be Element of G st g = x & (x |^ m) = ( 1_ G) by A1;

        ((g " ) |^ m) = ((g |^ m) " ) by GROUP_1: 37

        .= ( 1_ G) by GROUP_1: 8, A7;

        hence (g " ) in A by A1;

      end;

      hence thesis by A2, A3;

    end;

    theorem :: GROUP_17:14

    

     Th14: for G be finite commutative Group, m be Nat, A be Subset of G st A = { x where x be Element of G : (x |^ m) = ( 1_ G) } holds ex H be strict finite Subgroup of G st the carrier of H = A & H is commutative normal

    proof

      let G be finite commutative Group, m be Nat, A be Subset of G;

      assume A = { x where x be Element of G : (x |^ m) = ( 1_ G) };

      then A <> {} & (for g1,g2 be Element of G st g1 in A & g2 in A holds (g1 * g2) in A) & for g be Element of G st g in A holds (g " ) in A by Th13;

      then

      consider H be strict Subgroup of G such that

       A1: the carrier of H = A by GROUP_2: 52;

      H is normal by GROUP_3: 116;

      hence thesis by A1;

    end;

    

     Lm5: for G be finite Group, q be Prime st q in ( support ( prime_factorization ( card G))) holds ex a be Element of G st a <> ( 1_ G) & ( ord a) = q

    proof

      let G be finite Group, q be Prime;

      assume q in ( support ( prime_factorization ( card G)));

      then q in ( support ( pfexp ( card G))) by NAT_3:def 9;

      then

      consider g be Element of G such that

       A1: ( ord g) = q by GROUP_10: 11, NAT_3: 36;

      

       A2: 1 < q by INT_2:def 4;

      take g;

      thus thesis by A1, A2, GROUP_1: 42;

    end;

    theorem :: GROUP_17:15

    

     Th15: for G be finite commutative Group, m be Nat, H be finite Subgroup of G st the carrier of H = { x where x be Element of G : (x |^ m) = ( 1_ G) } holds for q be Prime st q in ( support ( prime_factorization ( card H))) holds not (q,m) are_coprime

    proof

      let G be finite commutative Group, m be Nat, H be finite Subgroup of G;

      assume

       A1: the carrier of H = { x where x be Element of G : (x |^ m) = ( 1_ G) };

      let q be Prime;

      assume

       A2: q in ( support ( prime_factorization ( card H)));

      assume

       A3: (q,m) are_coprime ;

      consider a be Element of H such that

       A4: a <> ( 1_ H) & ( ord a) = q by A2, Lm5;

      a in { x where x be Element of G : (x |^ m) = ( 1_ G) } by A1;

      then

      consider x be Element of G such that

       A5: x = a & (x |^ m) = ( 1_ G);

      

       A6: (a |^ m) = ( 1_ G) by A5, GROUP_4: 2;

      (q gcd m) = 1 by A3, INT_2:def 3;

      then

      consider x,y be Integer such that

       A7: ((x * q) + (y * m)) = 1 by NAT_D: 68;

      a = (a |^ 1) by GROUP_1: 26

      .= ((a |^ (q * x)) * (a |^ (m * y))) by GROUP_1: 33, A7

      .= (((a |^ q) |^ x) * (a |^ (m * y))) by GROUP_1: 35

      .= (((a |^ q) |^ x) * ((a |^ m) |^ y)) by GROUP_1: 35

      .= ((( 1_ H) |^ x) * ((a |^ m) |^ y)) by A4, GROUP_1: 41

      .= ((( 1_ H) |^ x) * (( 1_ H) |^ y)) by A6, GROUP_2: 44

      .= (( 1_ H) * (( 1_ H) |^ y)) by GROUP_1: 31

      .= (( 1_ H) * ( 1_ H)) by GROUP_1: 31

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

      .= ( 1_ G) by GROUP_2: 44;

      hence contradiction by GROUP_2: 44, A4;

    end;

    theorem :: GROUP_17:16

    

     Th16: for G be finite commutative Group, h,k be Nat st ( card G) = (h * k) & (h,k) are_coprime holds ex H,K be strict finite Subgroup of G st the carrier of H = { x where x be Element of G : (x |^ h) = ( 1_ G) } & the carrier of K = { x where x be Element of G : (x |^ k) = ( 1_ G) } & H is normal & K is normal & (for x be Element of G holds ex a,b be Element of G st a in H & b in K & x = (a * b)) & (the carrier of H /\ the carrier of K) = {( 1_ G)}

    proof

      let G be finite commutative Group, h,k be Nat;

      assume

       A1: ( card G) = (h * k) & (h,k) are_coprime ;

      set A = { x where x be Element of G : (x |^ h) = ( 1_ G) };

      set B = { x where x be Element of G : (x |^ k) = ( 1_ G) };

      A c= the carrier of G

      proof

        let y be object;

        assume y in A;

        then ex x be Element of G st y = x & (x |^ h) = ( 1_ G);

        hence y in the carrier of G;

      end;

      then

      reconsider A as Subset of G;

      B c= the carrier of G

      proof

        let y be object;

        assume y in B;

        then ex x be Element of G st y = x & (x |^ k) = ( 1_ G);

        hence y in the carrier of G;

      end;

      then

      reconsider B as Subset of G;

      consider H be strict finite Subgroup of G such that

       A2: the carrier of H = A & H is commutative & H is normal by Th14;

      consider K be strict finite Subgroup of G such that

       A3: the carrier of K = B & K is commutative & K is normal by Th14;

      (( 1_ G) |^ h) = ( 1_ G) by GROUP_1: 31;

      then

       A4: ( 1_ G) in the carrier of H by A2;

      (( 1_ G) |^ k) = ( 1_ G) by GROUP_1: 31;

      then ( 1_ G) in the carrier of K by A3;

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

      then

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

      (h gcd k) = 1 by A1, INT_2:def 3;

      then

      consider a,b be Integer such that

       A6: ((a * h) + (b * k)) = 1 by NAT_D: 68;

      (the carrier of H /\ the carrier of K) c= {( 1_ G)}

      proof

        let z be object;

        assume

         A7: z in (the carrier of H /\ the carrier of K);

        then z in the carrier of H by XBOOLE_0:def 4;

        then z in G by STRUCT_0:def 5, GROUP_2: 40;

        then

        reconsider w = z as Element of G;

        

         A8: w in A & w in B by A2, A3, A7, XBOOLE_0:def 4;

        then

         A9: ex x be Element of G st w = x & (x |^ h) = ( 1_ G);

        

         A10: ex x be Element of G st w = x & (x |^ k) = ( 1_ G) by A8;

        w = (w |^ 1) by GROUP_1: 26

        .= ((w |^ (a * h)) * (w |^ (b * k))) by GROUP_1: 33, A6

        .= (((w |^ h) |^ a) * (w |^ (b * k))) by GROUP_1: 35

        .= (((w |^ h) |^ a) * ((w |^ k) |^ b)) by GROUP_1: 35

        .= (( 1_ G) * (( 1_ G) |^ b)) by GROUP_1: 31, A10, A9

        .= (( 1_ G) * ( 1_ G)) by GROUP_1: 31

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

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

      end;

      then

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

      

       A12: for x be Element of G holds ex s,t be Element of G st s in H & t in K & x = (s * t)

      proof

        let x be Element of G;

        

         A13: x = (x |^ 1) by GROUP_1: 26

        .= ((x |^ (b * k)) * (x |^ (a * h))) by GROUP_1: 33, A6;

        set t = (x |^ (a * h));

        set s = (x |^ (b * k));

        (s |^ h) = (x |^ ((b * k) * h)) by GROUP_1: 35

        .= (x |^ ((k * h) * b))

        .= ((x |^ (k * h)) |^ b) by GROUP_1: 35

        .= (( 1_ G) |^ b) by A1, GR_CY_1: 9

        .= ( 1_ G) by GROUP_1: 31;

        then

         A14: s in H by A2;

        (t |^ k) = (x |^ ((a * h) * k)) by GROUP_1: 35

        .= (x |^ ((h * k) * a))

        .= ((x |^ (h * k)) |^ a) by GROUP_1: 35

        .= (( 1_ G) |^ a) by A1, GR_CY_1: 9

        .= ( 1_ G) by GROUP_1: 31;

        then t in K by A3;

        hence thesis by A13, A14;

      end;

      take H, K;

      thus thesis by A2, A3, A11, A12, A5, XBOOLE_0:def 10;

    end;

    theorem :: GROUP_17:17

    

     Th17: for H,K be finite Group holds ( card ( product <*H, K*>)) = (( card H) * ( card K))

    proof

      let H,K be finite Group;

      ( card ( product <*the carrier of H, the carrier of K*>)) = ( card the carrier of ( product <*H, K*>)) by Th10;

      hence thesis by Th2;

    end;

    theorem :: GROUP_17:18

    

     Th18: for G be finite commutative Group, h,k be non zero Nat st ( card G) = (h * k) & (h,k) are_coprime holds ex H,K be strict finite Subgroup of G st ( card H) = h & ( card K) = k & (the carrier of H /\ the carrier of K) = {( 1_ G)} & ex F be Homomorphism of ( product <*H, K*>), G st F is bijective & for a,b be Element of G st a in H & b in K holds (F . <*a, b*>) = (a * b)

    proof

      let G be finite commutative Group, h,k be non zero Nat;

      assume

       A1: ( card G) = (h * k) & (h,k) are_coprime ;

      then

      consider H,K be strict finite Subgroup of G such that

       A2: the carrier of H = { x where x be Element of G : (x |^ h) = ( 1_ G) } & the carrier of K = { x where x be Element of G : (x |^ k) = ( 1_ G) } & H is normal & K is normal & (for x be Element of G holds ex a,b be Element of G st a in H & b in K & x = (a * b)) & (the carrier of H /\ the carrier of K) = {( 1_ G)} by Th16;

      take H, K;

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

       A3: F is bijective & for a,b be Element of G st a in H & b in K holds (F . <*a, b*>) = (a * b) by A2, Th12;

      set s = ( card H);

      set t = ( card K);

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

      then ( card ( product <*H, K*>)) = ( card G) by CARD_1: 5, WELLORD2:def 4;

      then

       A4: (s * t) = (h * k) by A1, Th17;

      

       A5: for q be Prime st q in ( support ( prime_factorization s)) holds not (q,h) are_coprime by A2, Th15;

      for q be Prime st q in ( support ( prime_factorization t)) holds not (q,k) are_coprime by A2, Th15;

      hence thesis by A2, A3, A4, Th7, A5, A1;

    end;

    begin

    theorem :: GROUP_17:19

    

     Th19: for G be Group, q be set, F be associative Group-like multMagma-Family of {q}, f be Function of G, ( product F) st F = (q .--> G) & for x be Element of G holds (f . x) = (q .--> x) holds f is Homomorphism of G, ( product F)

    proof

      let G be Group, q be set, F be associative Group-like multMagma-Family of {q}, f be Function of G, ( product F);

      assume

       A1: F = (q .--> G);

      assume

       A2: for x be Element of G holds (f . x) = (q .--> x);

      

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

      now

        let a,b be Element of G;

        

         A4: (f . a) = (q .--> a) by A2;

        

         A5: (f . b) = (q .--> b) by A2;

        reconsider fa = (f . a), fb = (f . b) as Element of ( product F);

        set ga = (q .--> a);

        set gb = (q .--> b);

        consider gab be Function such that

         A6: (fa * fb) = gab & ( dom gab) = ( dom ( Carrier F)) & for y be object st y in ( dom ( Carrier F)) holds (gab . y) in (( Carrier F) . y) by CARD_3:def 5, A3;

        

         A7: for z be object st z in ( dom gab) holds (gab . z) = (a * b)

        proof

          let z be object;

          assume

           A8: z in ( dom gab);

          

           A9: G = (F . z) by A1, FUNCOP_1: 7, A8, A6;

          

           A10: (ga . z) = a by FUNCOP_1: 7, A8, A6;

          (gb . z) = b by FUNCOP_1: 7, A8, A6;

          hence (gab . z) = (a * b) by A4, A5, A6, A8, A9, A10, GROUP_7: 1;

        end;

        gab = (( dom gab) --> (a * b)) by A7, FUNCOP_1: 11

        .= (q .--> (a * b)) by A6, PARTFUN1:def 2

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

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

      end;

      hence thesis by GROUP_6:def 6;

    end;

    theorem :: GROUP_17:20

    

     Th20: for G be Group, q be set, F be associative Group-like multMagma-Family of {q}, f be Function of G, ( product F) st F = (q .--> G) & for x be Element of G holds (f . x) = (q .--> x) holds f is bijective

    proof

      let G be Group, q be set, F be associative Group-like multMagma-Family of {q}, f be Function of G, ( product F);

      assume

       A1: F = (q .--> G);

      assume

       A2: for x be Element of G holds (f . x) = (q .--> x);

      

       A3: q in {q} by TARSKI:def 1;

      

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

      ex R be 1-sorted st R = (F . q) & (( Carrier F) . q) = the carrier of R by PRALG_1:def 15, A3;

      then

       A5: (( Carrier F) . q) = the carrier of G by A1, FUNCOP_1: 7, A3;

      

       A6: ( dom ( Carrier F)) = {q} by PARTFUN1:def 2;

      for x1,x2 be object st x1 in the carrier of G & x2 in the carrier of G & (f . x1) = (f . x2) holds x1 = x2

      proof

        let z1,z2 be object;

        assume

         A7: z1 in the carrier of G & z2 in the carrier of G & (f . z1) = (f . z2);

        then

        reconsider x1 = z1, x2 = z2 as Element of G;

        

         A8: (f . x2) = (q .--> x2) by A2;

        

        thus z1 = ((q .--> x1) . q) by FUNCOP_1: 7, A3

        .= ((q .--> x2) . q) by A8, A2, A7

        .= z2 by FUNCOP_1: 7, A3;

      end;

      then

       A9: f is one-to-one by FUNCT_2: 19;

      for y be object st y in the carrier of ( product F) holds ex x be object st x in the carrier of G & y = (f . x)

      proof

        let y be object;

        assume y in the carrier of ( product F);

        then

        consider g be Function such that

         A10: y = g & ( dom g) = ( dom ( Carrier F)) & for z be object st z in ( dom ( Carrier F)) holds (g . z) in (( Carrier F) . z) by CARD_3:def 5, A4;

        reconsider x = (g . q) as Element of G by A5, A10, A3, A6;

        

         A11: for z be object st z in ( dom g) holds (g . z) = x by TARSKI:def 1, A10;

        take x;

        thus x in the carrier of G;

        

        thus y = (( dom g) --> x) by A11, FUNCOP_1: 11, A10

        .= (q .--> x) by A10, PARTFUN1:def 2

        .= (f . x) by A2;

      end;

      then ( rng f) = the carrier of ( product F) by FUNCT_2: 10;

      then f is onto by FUNCT_2:def 3;

      hence thesis by A9;

    end;

    theorem :: GROUP_17:21

    

     Th21: for q be set, F be associative Group-like multMagma-Family of {q}, G be Group st F = (q .--> G) holds ex I be Homomorphism of G, ( product F) st I is bijective & for x be Element of G holds (I . x) = (q .--> x)

    proof

      let q be set, F be associative Group-like multMagma-Family of {q}, G be Group;

      assume

       A1: F = (q .--> G);

      

       A2: q in {q} by TARSKI:def 1;

      

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

      ex R be 1-sorted st R = (F . q) & (( Carrier F) . q) = the carrier of R by PRALG_1:def 15, A2;

      then

       A4: (( Carrier F) . q) = the carrier of G by A1, FUNCOP_1: 7, A2;

      

       A5: ( dom ( Carrier F)) = {q} by PARTFUN1:def 2;

      defpred P[ set, set] means $2 = (q .--> $1);

      

       A6: for z be Element of G holds ex w be Element of ( product F) st P[z, w]

      proof

        let z be Element of G;

        set w = (q .--> z);

        now

          let i be object;

          assume

           A8: i in ( dom w);

          then

           A9: i = q by TARSKI:def 1;

          (w . i) = z by FUNCOP_1: 7, A8;

          hence (w . i) in (( Carrier F) . i) by A4, A9;

        end;

        then w in ( product ( Carrier F)) by A5, CARD_3: 9;

        hence ex w be Element of ( product F) st P[z, w] by A3;

      end;

      consider I be Function of G, ( product F) such that

       A10: for x be Element of G holds P[x, (I . x)] from FUNCT_2:sch 3( A6);

      reconsider I as Homomorphism of G, ( product F) by Th19, A1, A10;

      I is bijective by Th20, A1, A10;

      hence thesis by A10;

    end;

    theorem :: GROUP_17:22

    

     Th22: for I0,I be non empty finite set, F0 be associative Group-like multMagma-Family of I0, F be associative Group-like multMagma-Family of I, H,K be Group, q be Element of I, k be Element of K, g be Function st g in the carrier of ( product F0) & not q in I0 & I = (I0 \/ {q}) & F = (F0 +* (q .--> K)) holds (g +* (q .--> k)) in the carrier of ( product F)

    proof

      let I0,I be non empty finite set, F0 be associative Group-like multMagma-Family of I0, F be associative Group-like multMagma-Family of I, H,K be Group, q be Element of I, k be Element of K, g be Function;

      assume

       A1: g in the carrier of ( product F0) & not q in I0 & I = (I0 \/ {q}) & F = (F0 +* (q .--> K));

      set HK = <*H, K*>;

      

       A2: ( dom ( Carrier F0)) = I0 by PARTFUN1:def 2;

      

       A3: ( dom (q .--> k)) = {q};

      

       A4: ( dom (q .--> K)) = {q};

      

       A5: ( dom F0) = I0 by PARTFUN1:def 2;

      set w = (g +* (q .--> k));

      

       A6: g in ( product ( Carrier F0)) by A1, GROUP_7:def 2;

      then

       A7: ex g0 be Function st g = g0 & ( dom g0) = ( dom ( Carrier F0)) & for y be object st y in ( dom ( Carrier F0)) holds (g0 . y) in (( Carrier F0) . y) by CARD_3:def 5;

      ( dom w) = (( dom g) \/ ( dom (q .--> k))) by FUNCT_4:def 1

      .= (I0 \/ ( dom (q .--> k))) by PARTFUN1:def 2, A6

      .= I by A1;

      then

       A8: ( dom w) = ( dom ( Carrier F)) by PARTFUN1:def 2;

      for x be object st x in ( dom ( Carrier F)) holds (w . x) in (( Carrier F) . x)

      proof

        let x be object;

        assume

         A9: x in ( dom ( Carrier F));

        per cases by A1, XBOOLE_0:def 3, A9;

          suppose

           A10: x in I0;

          

           A11: not x in {q} by A1, A10, TARSKI:def 1;

          then

           A12: (F . x) = (F0 . x) by A1, FUNCT_4:def 1, A5, A4, A9;

          consider R1 be 1-sorted such that

           A13: R1 = (F0 . x) & (( Carrier F0) . x) = the carrier of R1 by PRALG_1:def 15, A10;

          consider R2 be 1-sorted such that

           A14: R2 = (F . x) & (( Carrier F) . x) = the carrier of R2 by PRALG_1:def 15, A9;

          (w . x) = (g . x) by FUNCT_4:def 1, A7, A2, A3, A9, A1, A11;

          hence (w . x) in (( Carrier F) . x) by A13, A14, A12, A10, A2, A7;

        end;

          suppose

           A15: x in {q};

          then (F . x) = ((q .--> K) . x) by A1, FUNCT_4:def 1, A5, A4;

          then

           A16: (F . x) = K by A15, FUNCOP_1: 7;

          

           A17: (w . x) = ((q .--> k) . x) by A7, A2, A3, A1, FUNCT_4:def 1, A15

          .= k by A15, FUNCOP_1: 7;

          ex R2 be 1-sorted st R2 = (F . x) & (( Carrier F) . x) = the carrier of R2 by PRALG_1:def 15, A15;

          hence (w . x) in (( Carrier F) . x) by A17, A16;

        end;

      end;

      then w in ( product ( Carrier F)) by A8, CARD_3:def 5;

      hence thesis by GROUP_7:def 2;

    end;

    

     Lm6: for I be non empty set, F be 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 set, F be multMagma-Family of I, x be set;

      assume

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

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

      hence thesis by A1;

    end;

    

     Lm7: for I be non empty set, F be 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 set, F be multMagma-Family of I, f be Function;

      assume

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

      

       A2: ( 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

       A3: 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

       A4: x in I;

      consider R be 1-sorted such that

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

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

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

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

      hence thesis by A4, A3, A2, A5;

    end;

    theorem :: GROUP_17:23

    

     Th23: for I0,I be non empty finite set, F0 be associative Group-like multMagma-Family of I0, F be associative Group-like multMagma-Family of I, H,K be Group, q be Element of I, G0 be Function of H, ( product F0) st G0 is Homomorphism of H, ( product F0) & G0 is bijective & not q in I0 & I = (I0 \/ {q}) & F = (F0 +* (q .--> K)) holds for G be Function of ( product <*H, K*>), ( product F) st for h be Element of H, k be Element of K holds ex g be Function st g = (G0 . h) & (G . <*h, k*>) = (g +* (q .--> k)) holds G is Homomorphism of ( product <*H, K*>), ( product F)

    proof

      let I0,I be non empty finite set, F0 be associative Group-like multMagma-Family of I0, F be associative Group-like multMagma-Family of I, H,K be Group, q be Element of I, G0 be Function of H, ( product F0);

      assume

       A1: G0 is Homomorphism of H, ( product F0) & G0 is bijective & not q in I0 & I = (I0 \/ {q}) & F = (F0 +* (q .--> K));

      let G be Function of ( product <*H, K*>), ( product F);

      assume

       A2: for h be Element of H, k be Element of K holds ex g be Function st g = (G0 . h) & (G . <*h, k*>) = (g +* (q .--> k));

      set HK = <*H, K*>;

      

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

      now

        let a,b be Element of ( product <*H, K*>);

        consider h1 be Element of H, k1 be Element of K such that

         A4: a = <*h1, k1*> by TOPALG_4: 1;

        consider h2 be Element of H, k2 be Element of K such that

         A5: b = <*h2, k2*> by TOPALG_4: 1;

        consider g1 be Function such that

         A6: g1 = (G0 . h1) & (G . <*h1, k1*>) = (g1 +* (q .--> k1)) by A2;

        consider g2 be Function such that

         A7: g2 = (G0 . h2) & (G . <*h2, k2*>) = (g2 +* (q .--> k2)) by A2;

        reconsider g1 as totalI0 -defined Function by A6, Lm6;

        reconsider g2 as totalI0 -defined Function by A7, Lm6;

        reconsider g12 = (G0 . (h1 * h2)) as totalI0 -defined Function by Lm6;

        

         A12: ex g12 be Function st g12 = (G0 . (h1 * h2)) & (G . <*(h1 * h2), (k1 * k2)*>) = (g12 +* (q .--> (k1 * k2))) by A2;

        reconsider Ga = (G . a), Gb = (G . b) as Element of ( product F);

        reconsider ga = (g1 +* (q .--> k1)) as totalI -defined Function by Lm6, A6;

        reconsider gb = (g2 +* (q .--> k2)) as totalI -defined Function by Lm6, A7;

        reconsider pab = (Ga * Gb) as totalI -defined Function by Lm6;

        

         A13: ( dom pab) = ( dom ( Carrier F)) by PARTFUN1:def 2, A3;

        

         A14: g12 = ((G0 . h1) * (G0 . h2)) by A1, GROUP_6:def 6;

        reconsider gab = (G . (a * b)) as totalI -defined Function by Lm6;

        

         A15: gab = (g12 +* (q .--> (k1 * k2))) by A4, A5, GROUP_7: 29, A12;

        

         A16: for i be set st i in I0 holds (ga . i) = (g1 . i) & (gb . i) = (g2 . i) & (gab . i) = (g12 . i) & (F . i) = (F0 . i)

        proof

          let i be set;

          assume

           A17: i in I0;

          

           A18: ( dom g1) = I0 by PARTFUN1:def 2;

          

           A19: ( dom g2) = I0 by PARTFUN1:def 2;

          

           A20: ( dom g12) = I0 by PARTFUN1:def 2;

          

           A21: ( dom F0) = I0 by PARTFUN1:def 2;

          

           A22: i in (( dom g1) \/ ( dom (q .--> k1))) by A18, A17, XBOOLE_0:def 3;

          

           A23: i in (( dom g2) \/ ( dom (q .--> k2))) by A19, A17, XBOOLE_0:def 3;

          

           A24: i in (( dom g12) \/ ( dom (q .--> (k1 * k2)))) by A20, A17, XBOOLE_0:def 3;

          

           A25: i in (( dom F0) \/ ( dom (q .--> K))) by A21, A17, XBOOLE_0:def 3;

           not i in ( dom (q .--> K)) by A1, A17, FUNCOP_1: 75;

          hence thesis by A25, FUNCT_4:def 1, A1, A22, A23, A24, A15;

        end;

        

         A29: (ga . q) = k1 & (gb . q) = k2 & (gab . q) = (k1 * k2) & (F . q) = K

        proof

          

           A30: q in {q} by TARSKI:def 1;

          

           A31: q in ( dom (q .--> k1)) by TARSKI:def 1;

          

           A32: q in ( dom (q .--> k2)) by TARSKI:def 1;

          

           A33: q in ( dom (q .--> (k1 * k2))) by TARSKI:def 1;

          

           A34: q in ( dom (q .--> K)) by TARSKI:def 1;

          

           A35: q in (( dom g1) \/ ( dom (q .--> k1))) by A30, XBOOLE_0:def 3;

          

           A36: q in (( dom g2) \/ ( dom (q .--> k2))) by A30, XBOOLE_0:def 3;

          

           A37: q in (( dom g12) \/ ( dom (q .--> (k1 * k2)))) by A30, XBOOLE_0:def 3;

          

           A38: q in (( dom F0) \/ ( dom (q .--> K))) by A30, XBOOLE_0:def 3;

          

           A39: (ga . q) = ((q .--> k1) . q) by A31, A35, FUNCT_4:def 1

          .= k1 by FUNCOP_1: 7, A30;

          

           A40: (gb . q) = ((q .--> k2) . q) by A32, A36, FUNCT_4:def 1

          .= k2 by FUNCOP_1: 7, A30;

          

           A41: (gab . q) = ((q .--> (k1 * k2)) . q) by A33, A37, A15, FUNCT_4:def 1

          .= (k1 * k2) by FUNCOP_1: 7, A30;

          (F . q) = ((q .--> K) . q) by A34, A38, A1, FUNCT_4:def 1

          .= K by FUNCOP_1: 7, A30;

          hence thesis by A39, A40, A41;

        end;

        

         A42: for x be set st x in I0 holds (pab . x) = (gab . x)

        proof

          let x be set;

          assume

           A43: x in I0;

          then

           A44: x in I by A1, XBOOLE_0:def 3;

          consider S be non empty multMagma such that

           A45: S = (F0 . x) & (g1 . x) in the carrier of S by A43, Lm7, A6;

          reconsider x0 = (g1 . x) as Element of S by A45;

          ex R be non empty multMagma st R = (F0 . x) & (g2 . x) in the carrier of R by Lm7, A43, A7;

          then

          reconsider y0 = (g2 . x) as Element of S by A45;

          

           A46: S = (F . x) by A45, A16, A43;

          x0 = (ga . x) & y0 = (gb . x) by A16, A43;

          

          hence (pab . x) = (x0 * y0) by A44, A46, GROUP_7: 1, A6, A4, A7, A5

          .= (g12 . x) by A14, A6, A7, GROUP_7: 1, A43, A45

          .= (gab . x) by A16, A43;

        end;

        for x be object st x in ( dom gab) holds (gab . x) = (pab . x)

        proof

          let x be object;

          assume x in ( dom gab);

          per cases by XBOOLE_0:def 3, A1;

            suppose x in I0;

            hence (gab . x) = (pab . x) by A42;

          end;

            suppose x in {q};

            then x = q by TARSKI:def 1;

            hence (gab . x) = (pab . x) by A29, GROUP_7: 1, A6, A4, A7, A5;

          end;

        end;

        hence (G . (a * b)) = ((G . a) * (G . b)) by A13, PARTFUN1:def 2, A3, FUNCT_1: 2;

      end;

      hence thesis by GROUP_6:def 6;

    end;

    theorem :: GROUP_17:24

    

     Th24: for I0,I be non empty finite set, F0 be associative Group-like multMagma-Family of I0, F be associative Group-like multMagma-Family of I, H,K be Group, q be Element of I, G0 be Function of H, ( product F0) st G0 is Homomorphism of H, ( product F0) & G0 is bijective & not q in I0 & I = (I0 \/ {q}) & F = (F0 +* (q .--> K)) holds for G be Function of ( product <*H, K*>), ( product F) st for h be Element of H, k be Element of K holds ex g be Function st g = (G0 . h) & (G . <*h, k*>) = (g +* (q .--> k)) holds G is bijective

    proof

      let I0,I be non empty finite set, F0 be associative Group-like multMagma-Family of I0, F be associative Group-like multMagma-Family of I, H,K be Group, q be Element of I, G0 be Function of H, ( product F0);

      assume

       A1: G0 is Homomorphism of H, ( product F0) & G0 is bijective & not q in I0 & I = (I0 \/ {q}) & F = (F0 +* (q .--> K));

      let G be Function of ( product <*H, K*>), ( product F);

      assume

       A2: for h be Element of H, k be Element of K holds ex g be Function st g = (G0 . h) & (G . <*h, k*>) = (g +* (q .--> k));

      set HK = <*H, K*>;

      

       A3: ( dom ( Carrier F0)) = I0 by PARTFUN1:def 2;

      

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

      

       A5: ( dom F0) = I0 by PARTFUN1:def 2;

      

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

      for x1,x2 be object st x1 in the carrier of ( product <*H, K*>) & x2 in the carrier of ( product <*H, K*>) & (G . x1) = (G . x2) holds x1 = x2

      proof

        let z1,z2 be object;

        assume

         A8: z1 in the carrier of ( product <*H, K*>) & z2 in the carrier of ( product <*H, K*>) & (G . z1) = (G . z2);

        then

        reconsider x1 = z1, x2 = z2 as Element of ( product <*H, K*>);

        consider h1 be Element of H, k1 be Element of K such that

         A9: x1 = <*h1, k1*> by TOPALG_4: 1;

        consider h2 be Element of H, k2 be Element of K such that

         A10: x2 = <*h2, k2*> by TOPALG_4: 1;

        consider g1 be Function such that

         A11: g1 = (G0 . h1) & (G . <*h1, k1*>) = (g1 +* (q .--> k1)) by A2;

        consider g2 be Function such that

         A12: g2 = (G0 . h2) & (G . <*h2, k2*>) = (g2 +* (q .--> k2)) by A2;

        reconsider g1 as totalI0 -defined Function by Lm6, A11;

        reconsider g2 as totalI0 -defined Function by Lm6, A12;

        reconsider ga = (g1 +* (q .--> k1)) as totalI -defined Function by Lm6, A11;

        reconsider gb = (g2 +* (q .--> k2)) as totalI -defined Function by Lm6, A12;

        

         A15: for i be set st i in I0 holds (ga . i) = (g1 . i) & (gb . i) = (g2 . i) & (F . i) = (F0 . i)

        proof

          let i be set;

          assume

           A16: i in I0;

          

           A17: ( dom g1) = I0 by PARTFUN1:def 2;

          

           A18: ( dom g2) = I0 by PARTFUN1:def 2;

          

           A19: i in (( dom g1) \/ ( dom (q .--> k1))) by A17, A16, XBOOLE_0:def 3;

          

           A20: i in (( dom g2) \/ ( dom (q .--> k2))) by A18, A16, XBOOLE_0:def 3;

          

           A21: i in (( dom F0) \/ ( dom (q .--> K))) by A5, A16, XBOOLE_0:def 3;

           not i in ( dom (q .--> K)) by A1, A16, FUNCOP_1: 75;

          hence thesis by A21, A1, A19, A20, FUNCT_4:def 1;

        end;

        

         A24: ( dom g2) = I0 by PARTFUN1:def 2;

        for x be object st x in ( dom g1) holds (g1 . x) = (g2 . x)

        proof

          let x be object;

          assume

           A25: x in ( dom g1);

          

          thus (g1 . x) = (ga . x) by A15, A25

          .= (g2 . x) by A15, A25, A11, A12, A9, A10, A8;

        end;

        then

         A26: (G0 . h1) = (G0 . h2) by A11, A12, FUNCT_1: 2, PARTFUN1:def 2, A24;

        (ga . q) = k1 & (gb . q) = k2

        proof

          

           A27: q in {q} by TARSKI:def 1;

          

           A28: q in ( dom (q .--> k1)) by TARSKI:def 1;

          

           A29: q in ( dom (q .--> k2)) by TARSKI:def 1;

          

           A30: q in (( dom g1) \/ ( dom (q .--> k1))) by A27, XBOOLE_0:def 3;

          

           A31: q in (( dom g2) \/ ( dom (q .--> k2))) by A27, XBOOLE_0:def 3;

          

           A32: (ga . q) = ((q .--> k1) . q) by A28, A30, FUNCT_4:def 1

          .= k1 by FUNCOP_1: 7, A27;

          (gb . q) = ((q .--> k2) . q) by A29, A31, FUNCT_4:def 1

          .= k2 by FUNCOP_1: 7, A27;

          hence thesis by A32;

        end;

        hence z1 = z2 by A9, A10, A26, A1, FUNCT_2: 19, A11, A12, A8;

      end;

      then

       A33: G is one-to-one by FUNCT_2: 19;

      for y be object st y in the carrier of ( product F) holds ex x be object st x in the carrier of ( product <*H, K*>) & y = (G . x)

      proof

        let y be object;

        assume

         A34: y in the carrier of ( product F);

        then

        reconsider y as totalI -defined Function by Lm6;

        

         A35: q in {q} by TARSKI:def 1;

        

         A36: q in ( dom (q .--> K)) by TARSKI:def 1;

        

         A37: q in (( dom F0) \/ ( dom (q .--> K))) by A35, XBOOLE_0:def 3;

        

         A38: (F . q) = ((q .--> K) . q) by A36, A37, A1, FUNCT_4:def 1

        .= K by FUNCOP_1: 7, A35;

        ex R be non empty multMagma st R = (F . q) & (y . q) in the carrier of R by Lm7, A34;

        then

        reconsider k = (y . q) as Element of K by A38;

        reconsider y0 = (y | I0) as I0 -defined Function;

        

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

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

        then

         A40: ( dom y0) = I0 by RELAT_1: 62, A1, XBOOLE_1: 7;

        for i be object st i in ( dom ( Carrier F0)) holds (y0 . i) in (( Carrier F0) . i)

        proof

          let i be object;

          assume

           A41: i in ( dom ( Carrier F0));

          then

           A42: i in I0;

          

           A43: i in (( dom F0) \/ ( dom (q .--> K))) by A5, A41, XBOOLE_0:def 3;

          

           A44: not i in ( dom (q .--> K)) by A1, A42, FUNCOP_1: 75;

          

           A45: I0 c= I by XBOOLE_1: 7, A1;

          

           A46: ex R be 1-sorted st R = (F0 . i) & (( Carrier F0) . i) = the carrier of R by A41, PRALG_1:def 15;

          ex R be 1-sorted st R = (F . i) & (( Carrier F) . i) = the carrier of R by A42, A45, PRALG_1:def 15;

          then

           A47: (( Carrier F0) . i) = (( Carrier F) . i) by A43, FUNCT_4:def 1, A1, A44, A46;

          ex g be Function st y = g & ( dom g) = ( dom ( Carrier F)) & for i be object st i in ( dom ( Carrier F)) holds (g . i) in (( Carrier F) . i) by CARD_3:def 5, A34, A6;

          then (y . i) in (( Carrier F) . i) by A45, A4, A42;

          hence (y0 . i) in (( Carrier F0) . i) by A47, A41, FUNCT_1: 49;

        end;

        then y0 in the carrier of ( product F0) by A40, A3, CARD_3:def 5, A39;

        then y0 in ( rng G0) by A1, FUNCT_2:def 3;

        then

        consider h be Element of H such that

         A48: y0 = (G0 . h) by FUNCT_2: 113;

        

         A49: ( dom y) = I by PARTFUN1:def 2;

        then (y | {q}) = (q .--> k) by FUNCT_7: 6;

        then

         A50: y = ((y | I0) +* (q .--> k)) by A1, A49, FUNCT_4: 70;

        consider g be Function such that

         A51: g = (G0 . h) & (G . <*h, k*>) = (g +* (q .--> k)) by A2;

        thus thesis by A48, A50, A51;

      end;

      then ( rng G) = the carrier of ( product F) by FUNCT_2: 10;

      then G is onto by FUNCT_2:def 3;

      hence thesis by A33;

    end;

    theorem :: GROUP_17:25

    

     Th25: for q be set, F be multMagma-Family of {q}, G be non empty multMagma st F = (q .--> G) holds for y be the carrier of G -valued total {q} -defined Function holds y in the carrier of ( product F) & (y . q) in the carrier of G & y = (q .--> (y . q))

    proof

      let q be set, F be multMagma-Family of {q}, G be non empty multMagma;

      assume

       A1: F = (q .--> G);

      

       A2: q in {q} by TARSKI:def 1;

      

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

      ex R be 1-sorted st R = (F . q) & (( Carrier F) . q) = the carrier of R by PRALG_1:def 15, A2;

      then

       A4: (( Carrier F) . q) = the carrier of G by A2, A1, FUNCOP_1: 7;

      

       A5: ( dom ( Carrier F)) = {q} by PARTFUN1:def 2;

      let y be the carrier of G -valued total {q} -defined Function;

      

       A6: ( dom y) = {q} by PARTFUN1:def 2;

      then (y . q) in ( rng y) by FUNCT_1: 3, A2;

      then

      reconsider z = (y . q) as Element of G;

      

       A7: for x be object st x in ( dom y) holds (y . x) = z by TARSKI:def 1;

      now

        let i be object;

        assume

         A8: i in ( dom y);

        then

         A9: i = q by TARSKI:def 1;

        (y . i) = z by TARSKI:def 1, A8;

        hence (y . i) in (( Carrier F) . i) by A4, A9;

      end;

      hence thesis by A7, FUNCOP_1: 11, A5, A6, CARD_3: 9, A3;

    end;

    theorem :: GROUP_17:26

    

     Th26: for q be set, F be associative Group-like multMagma-Family of {q}, G be Group st F = (q .--> G) holds ex HFG be Homomorphism of ( product F), G st HFG is bijective & for x be the carrier of G -valued total {q} -defined Function holds (HFG . x) = ( Product x)

    proof

      let q be set, F be associative Group-like multMagma-Family of {q}, G be Group;

      assume

       A1: F = (q .--> G);

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

       A2: I is bijective & for x be Element of G holds (I . x) = (q .--> x) by Th21, A1;

      set HFG = (I " );

      

       A3: ( rng I) = the carrier of ( product F) by A2, FUNCT_2:def 3;

      then

      reconsider HFG as Function of ( product F), G by FUNCT_2: 25, A2;

      

       A4: (HFG * I) = ( id the carrier of G) & (I * HFG) = ( id the carrier of ( product F)) by A2, A3, FUNCT_2: 29;

      

       A5: HFG is onto by A4, FUNCT_2: 23;

      reconsider HFG as Homomorphism of ( product F), G by A2, GROUP_6: 62;

      for y be the carrier of G -valued total {q} -defined Function holds (HFG . y) = ( Product y)

      proof

        let y be the carrier of G -valued total {q} -defined Function;

        

         A6: y in the carrier of ( product F) & (y . q) in the carrier of G & y = (q .--> (y . q)) by A1, Th25;

        reconsider z = (y . q) as Element of G by A1, Th25;

        

         A7: (I . z) = (q .--> z) by A2

        .= y by A1, Th25;

        

        thus (HFG . y) = z by FUNCT_2: 26, A2, A7

        .= ( Product y) by Th9, A6;

      end;

      hence thesis by A5, A2;

    end;

    theorem :: GROUP_17:27

    

     Th27: for I0,I be non empty finite set, F0 be associative Group-like multMagma-Family of I0, F be associative Group-like multMagma-Family of I, H,K be Group, q be Element of I, G0 be Homomorphism of H, ( product F0) st not q in I0 & I = (I0 \/ {q}) & F = (F0 +* (q .--> K)) & G0 is bijective holds ex G be Homomorphism of ( product <*H, K*>), ( product F) st G is bijective & for h be Element of H, k be Element of K holds ex g be Function st g = (G0 . h) & (G . <*h, k*>) = (g +* (q .--> k))

    proof

      let I0,I be non empty finite set, F0 be associative Group-like multMagma-Family of I0, F be associative Group-like multMagma-Family of I, H,K be Group, q be Element of I, G0 be Homomorphism of H, ( product F0);

      assume

       A1: not q in I0 & I = (I0 \/ {q}) & F = (F0 +* (q .--> K)) & G0 is bijective;

      set HK = <*H, K*>;

      

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

      defpred P[ set, set] means ex h be Element of H, k be Element of K, g be Function st $1 = <*h, k*> & g = (G0 . h) & $2 = (g +* (q .--> k));

      

       A3: for z be Element of ( product <*H, K*>) holds ex w be Element of the carrier of ( product F) st P[z, w]

      proof

        let z be Element of ( product <*H, K*>);

        consider h be Element of H, k be Element of K such that

         A4: z = <*h, k*> by TOPALG_4: 1;

        consider g be Function such that

         A5: (G0 . h) = g & ( dom g) = ( dom ( Carrier F0)) & for y be object st y in ( dom ( Carrier F0)) holds (g . y) in (( Carrier F0) . y) by CARD_3:def 5, A2;

        set w = (g +* (q .--> k));

        w in the carrier of ( product F) by A1, A5, Th22;

        hence thesis by A4, A5;

      end;

      consider G be Function of ( product <*H, K*>), ( product F) such that

       A6: for x be Element of ( product <*H, K*>) holds P[x, (G . x)] from FUNCT_2:sch 3( A3);

      

       A7: for h be Element of H, k be Element of K holds ex g be Function st g = (G0 . h) & (G . <*h, k*>) = (g +* (q .--> k))

      proof

        let h be Element of H, k be Element of K;

        reconsider z = <*h, k*> as Element of ( product <*H, K*>);

        consider h1 be Element of H, k1 be Element of K, g be Function such that

         A8: z = <*h1, k1*> & g = (G0 . h1) & (G . z) = (g +* (q .--> k1)) by A6;

        

         A9: h1 = ( <*h1, k1*> . 1) by FINSEQ_1: 44

        .= h by FINSEQ_1: 44, A8;

        k1 = ( <*h1, k1*> . 2) by FINSEQ_1: 44

        .= k by FINSEQ_1: 44, A8;

        hence thesis by A8, A9;

      end;

      then

      reconsider G as Homomorphism of ( product <*H, K*>), ( product F) by Th23, A1;

      G is bijective by Th24, A1, A7;

      hence thesis by A7;

    end;

    theorem :: GROUP_17:28

    

     Th28: for I0,I be non empty finite set, F0 be associative Group-like multMagma-Family of I0, F be associative Group-like multMagma-Family of I, H,K be Group, q be Element of I, G0 be Homomorphism of ( product F0), H st not q in I0 & I = (I0 \/ {q}) & F = (F0 +* (q .--> K)) & G0 is bijective holds ex G be Homomorphism of ( product F), ( product <*H, K*>) st G is bijective & for x0 be Function, k be Element of K, h be Element of H st h = (G0 . x0) & x0 in ( product F0) holds (G . (x0 +* (q .--> k))) = <*h, k*>

    proof

      let I0,I be non empty finite set, F0 be associative Group-like multMagma-Family of I0, F be associative Group-like multMagma-Family of I, H,K be Group, q be Element of I, G0 be Homomorphism of ( product F0), H;

      assume

       A1: not q in I0 & I = (I0 \/ {q}) & F = (F0 +* (q .--> K)) & G0 is bijective;

      set L0 = (G0 " );

      

       A2: ( rng G0) = the carrier of H by FUNCT_2:def 3, A1;

      then

      reconsider L0 as Function of H, ( product F0) by FUNCT_2: 25, A1;

      

       A3: (L0 * G0) = ( id the carrier of ( product F0)) & (G0 * L0) = ( id the carrier of H) by A1, A2, FUNCT_2: 29;

      

       A4: L0 is onto by A3, FUNCT_2: 23;

      reconsider L0 as Homomorphism of H, ( product F0) by A1, GROUP_6: 62;

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

       A5: L is bijective & for h be Element of H, k be Element of K holds ex g be Function st g = (L0 . h) & (L . <*h, k*>) = (g +* (q .--> k)) by Th27, A1, A4;

      set G = (L " );

      

       A6: ( rng L) = the carrier of ( product F) by FUNCT_2:def 3, A5;

      then

      reconsider G as Function of ( product F), ( product <*H, K*>) by FUNCT_2: 25, A5;

      

       A7: (G * L) = ( id the carrier of ( product <*H, K*>)) & (L * G) = ( id the carrier of ( product F)) by A5, A6, FUNCT_2: 29;

      

       A8: G is onto by A7, FUNCT_2: 23;

      reconsider G as Homomorphism of ( product F), ( product <*H, K*>) by A5, GROUP_6: 62;

      for x0 be Function, k be Element of K, h be Element of H st h = (G0 . x0) & x0 in ( product F0) holds (G . (x0 +* (q .--> k))) = <*h, k*>

      proof

        let x0 be Function, k be Element of K, h be Element of H;

        assume

         A9: h = (G0 . x0) & x0 in ( product F0);

        consider g be Function such that

         A10: g = (L0 . h) & (L . <*h, k*>) = (g +* (q .--> k)) by A5;

        g = x0 by A10, A1, A9, FUNCT_2: 26;

        hence (G . (x0 +* (q .--> k))) = <*h, k*> by A5, FUNCT_2: 26, A10;

      end;

      hence thesis by A8, A5;

    end;

    theorem :: GROUP_17:29

    

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

    proof

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

      assume

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

      

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

      

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

      

       A4: ( dom x) = I by PARTFUN1:def 2;

      now

        let i be object;

        assume

         A5: i in ( dom ( Carrier F));

        consider R be 1-sorted such that

         A6: R = (F . i) & (( Carrier F) . i) = the carrier of R by PRALG_1:def 15, A5;

        reconsider i0 = i as Element of I by A5;

        (x . i0) in the carrier of R by A6, STRUCT_0:def 5, A1;

        hence (x . i) in (( Carrier F) . i) by A6;

      end;

      hence thesis by A3, A2, A4, CARD_3:def 5;

    end;

    theorem :: GROUP_17:30

    

     Th30: for I0,I be non empty finite set, F0 be associative Group-like multMagma-Family of I0, F be associative Group-like multMagma-Family of I, K be Group, q be Element of I, x be Element of ( product F) st not q in I0 & I = (I0 \/ {q}) & F = (F0 +* (q .--> K)) holds ex x0 be totalI0 -defined Function, k be Element of K st x0 in ( product F0) & x = (x0 +* (q .--> k)) & for p be Element of I0 holds (x0 . p) in (F0 . p)

    proof

      let I0,I be non empty finite set, F0 be associative Group-like multMagma-Family of I0, F be associative Group-like multMagma-Family of I, K be Group, q be Element of I, x be Element of ( product F);

      assume

       A1: not q in I0 & I = (I0 \/ {q}) & F = (F0 +* (q .--> K));

      reconsider y = x as totalI -defined Function by Lm6;

      

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

      

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

      

       A4: ( dom F0) = I0 by PARTFUN1:def 2;

      

       A6: q in {q} by TARSKI:def 1;

      

       A7: q in ( dom (q .--> K)) by TARSKI:def 1;

      

       A8: q in (( dom F0) \/ ( dom (q .--> K))) by A6, XBOOLE_0:def 3;

      

       A9: (F . q) = ((q .--> K) . q) by A7, A8, A1, FUNCT_4:def 1

      .= K by FUNCOP_1: 7, A6;

      ex R be non empty multMagma st R = (F . q) & (y . q) in the carrier of R by Lm7;

      then

      reconsider k = (y . q) as Element of K by A9;

      reconsider y0 = (y | I0) as I0 -defined Function;

      

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

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

      then

       A11: ( dom y0) = I0 by RELAT_1: 62, A1, XBOOLE_1: 7;

      then

      reconsider y0 as totalI0 -defined Function by PARTFUN1:def 2;

      

       A12: ( dom ( Carrier F0)) = I0 by PARTFUN1:def 2;

      

       A13: for i be Element of I0 holds (y0 . i) in (( Carrier F0) . i) & (y0 . i) in (F0 . i)

      proof

        let i be Element of I0;

        

         A14: i in (( dom F0) \/ ( dom (q .--> K))) by A4, XBOOLE_0:def 3;

        i <> q by A1;

        then

         A15: not i in ( dom (q .--> K)) by FUNCOP_1: 75;

        

         A16: i in I by TARSKI:def 3, XBOOLE_1: 7, A1;

        consider R be 1-sorted such that

         A17: R = (F0 . i) & (( Carrier F0) . i) = the carrier of R by PRALG_1:def 15;

        ex R be 1-sorted st R = (F . i) & (( Carrier F) . i) = the carrier of R by A16, PRALG_1:def 15;

        then

         A18: (( Carrier F0) . i) = (( Carrier F) . i) by A15, A14, FUNCT_4:def 1, A1, A17;

        ex g be Function st y = g & ( dom g) = ( dom ( Carrier F)) & for i be object st i in ( dom ( Carrier F)) holds (g . i) in (( Carrier F) . i) by CARD_3:def 5, A3;

        then (y . i) in (( Carrier F) . i) by A16, A2;

        hence thesis by A17, FUNCT_1: 49, A18;

      end;

      for i be object st i in ( dom ( Carrier F0)) holds (y0 . i) in (( Carrier F0) . i) by A13;

      then

       A19: y0 in the carrier of ( product F0) by A10, A11, A12, CARD_3:def 5;

      

       A20: ( dom y) = I by PARTFUN1:def 2;

      then (y | {q}) = (q .--> k) by FUNCT_7: 6;

      then y = ((y | I0) +* (q .--> k)) by A1, A20, FUNCT_4: 70;

      hence thesis by A19, STRUCT_0:def 5, A13;

    end;

    theorem :: GROUP_17:31

    

     Th31: for G be Group, H be Subgroup of G, f be FinSequence of G, g be FinSequence of H st f = g holds ( Product f) = ( Product g)

    proof

      let G be Group, H be Subgroup of G;

      defpred P[ Nat] means for f be FinSequence of G, g be FinSequence of H st $1 = ( len f) & f = g holds ( Product f) = ( Product g);

      

       A1: P[ 0 ]

      proof

        let f be FinSequence of G, g be FinSequence of H;

        assume

         A2: 0 = ( len f) & f = g;

        then f = ( <*> the carrier of G);

        then

         A3: ( Product f) = ( 1_ G) by GROUP_4: 8;

        g = ( <*> the carrier of H) by A2;

        then ( Product g) = ( 1_ H) by GROUP_4: 8;

        hence thesis by A3, GROUP_2: 44;

      end;

      

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

      proof

        let k be Nat;

        assume

         A5: P[k];

        let f be FinSequence of G, g be FinSequence of H;

        assume

         A6: (k + 1) = ( len f) & f = g;

        

         A7: (k + 1) in ( Seg (k + 1)) by FINSEQ_1: 4;

        then (k + 1) in ( dom f) by A6, FINSEQ_1:def 3;

        then (f . (k + 1)) in ( rng f) by FUNCT_1: 3;

        then

        reconsider af = (f . (k + 1)) as Element of G;

        (k + 1) in ( dom g) by A7, A6, FINSEQ_1:def 3;

        then (g . (k + 1)) in ( rng g) by FUNCT_1: 3;

        then

        reconsider ag = (g . (k + 1)) as Element of H;

        reconsider f1 = (f | k) as FinSequence of G;

        reconsider g1 = (g | k) as FinSequence of H;

        

         A8: f = (f1 ^ <*af*>) by A6, RFINSEQ: 7;

        

         A9: g = (g1 ^ <*ag*>) by A6, RFINSEQ: 7;

        

         A10: ( Product f) = (( Product f1) * af) by GROUP_4: 6, A8;

        

         A11: ( Product g) = (( Product g1) * ag) by GROUP_4: 6, A9;

        ( len f1) = k by FINSEQ_1: 59, A6, NAT_1: 11;

        then ( Product f1) = ( Product g1) by A6, A5;

        hence thesis by A10, A11, GROUP_2: 43, A6;

      end;

      

       A12: for k be Nat holds P[k] from NAT_1:sch 2( A1, A4);

      let f be FinSequence of G, g be FinSequence of H;

      assume

       A13: f = g;

      ( len f) is Nat;

      hence thesis by A13, A12;

    end;

    theorem :: GROUP_17:32

    

     Th32: for I be non empty finite set, G be Group, H be Subgroup of G, x be the carrier of G -valued totalI -defined Function, x0 be the carrier of H -valued totalI -defined Function st x = x0 holds ( Product x) = ( Product x0)

    proof

      let I be non empty finite set, G be Group, H be Subgroup of G, x be the carrier of G -valued totalI -defined Function, x0 be the carrier of H -valued totalI -defined Function;

      assume

       A1: x = x0;

      consider f be FinSequence of G such that

       A2: ( Product x) = ( Product f) & f = (x * ( canFS I)) by Def1;

      consider g be FinSequence of the carrier of H such that

       A3: ( Product x0) = ( Product g) & g = (x0 * ( canFS I)) by Def1;

      thus thesis by A2, A1, A3, Th31;

    end;

    theorem :: GROUP_17:33

    

     Th33: for G be commutative Group, I0,I be non empty finite set, q be Element of I, x be the carrier of G -valued totalI -defined Function, x0 be the carrier of G -valued totalI0 -defined Function, k be Element of G st not q in I0 & I = (I0 \/ {q}) & x = (x0 +* (q .--> k)) holds ( Product x) = (( Product x0) * k)

    proof

      let G be commutative Group, I0,I be non empty finite set, q be Element of I, x be the carrier of G -valued totalI -defined Function, x0 be the carrier of G -valued totalI0 -defined Function, k be Element of G;

      assume

       A1: not q in I0 & I = (I0 \/ {q}) & x = (x0 +* (q .--> k));

      reconsider y = (q .--> k) as the carrier of G -valued total {q} -defined Function;

      

       A2: I0 misses {q}

      proof

        assume I0 meets {q};

        then

        consider x be object such that

         A3: x in I0 & x in {q} by XBOOLE_0: 3;

        thus contradiction by A3, A1, TARSKI:def 1;

      end;

      ( Product x) = (( Product x0) * ( Product y)) by A2, A1, Th8;

      hence thesis by Th9;

    end;

    theorem :: GROUP_17:34

    

     Th34: for G be strict finite commutative Group st ( card G) > 1 holds ex I be non empty finite set, F be associative Group-like commutative multMagma-Family of I, HFG be Homomorphism of ( product F), G st I = ( support ( prime_factorization ( card G))) & (for p be Element of I holds (F . p) is strict Subgroup of G & ( card (F . p)) = (( prime_factorization ( card G)) . p)) & (for p,q be Element of I 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 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

      defpred P[ Nat] means for G be strict finite commutative Group st ( card ( support ( prime_factorization ( card G)))) = $1 & $1 <> 0 holds ex I be non empty finite set, F be associative Group-like commutative multMagma-Family of I, HFG be Homomorphism of ( product F), G st I = ( support ( prime_factorization ( card G))) & (for p be Element of I holds (F . p) is strict Subgroup of G & ( card (F . p)) = (( prime_factorization ( card G)) . p)) & (for p,q be Element of I 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 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);

      

       A1: P[ 0 ];

      

       A2: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume

         A3: P[n];

        thus P[(n + 1)]

        proof

          let G be strict finite commutative Group;

          assume

           A4: ( card ( support ( prime_factorization ( card G)))) = (n + 1) & (n + 1) <> 0 ;

          per cases ;

            suppose

             A5: n = 0 ;

            set f = ( prime_factorization ( card G));

            

             A6: ( support f) = ( support ( pfexp ( card G))) by NAT_3:def 9;

            ( support f) <> {} by A4;

            then

            consider q be object such that

             A7: q in ( support f) by XBOOLE_0:def 1;

            reconsider q as Prime by A6, A7, NAT_3: 34;

            ( card {q}) = 1 by CARD_1: 30;

            then

            consider q0 be object such that

             A8: ( support ( prime_factorization ( card G))) = {q0} by CARD_1: 29, A5, A4;

            

             A9: {q} = ( support ( prime_factorization ( card G))) by A8, TARSKI:def 1, A7;

            reconsider Gq = (q |^ (q |-count ( card G))) as non zero Nat;

            set g = ( prime_factorization Gq);

            

             A10: ( Product g) = Gq by NAT_3: 61;

            (q |-count ( card G)) <> 0

            proof

              assume (q |-count ( card G)) = 0 ;

              then (f . q) = 0 by NAT_3: 55;

              hence contradiction by A7, PRE_POLY:def 7;

            end;

            then

             A11: ( support ( pfexp Gq)) = {q} by NAT_3: 42;

            then q in ( support ( pfexp Gq)) by TARSKI:def 1;

            then

             A12: (g . q) = (q |^ (q |-count Gq)) by NAT_3:def 9;

            ( support g) = {q} by A11, NAT_3:def 9;

            then

             A13: ( support g) = ( support ( pfexp ( card G))) by A9, NAT_3:def 9;

            for p be Nat st p in ( support ( pfexp ( card G))) holds (g . p) = (p |^ (p |-count ( card G)))

            proof

              let p be Nat;

              assume p in ( support ( pfexp ( card G)));

              then p in {q} by NAT_3:def 9, A9;

              then p = q by TARSKI:def 1;

              hence thesis by A12, NAT_3: 25, INT_2:def 4;

            end;

            

            then

             A14: Gq = ( Product ( prime_factorization ( card G))) by A13, NAT_3:def 9, A10

            .= ( card G) by NAT_3: 61;

            reconsider I = {q} as non empty finite set;

            set F = (q .--> G);

            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

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

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

            end;

            then

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

            

             A16: 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

               A17: s <> t;

              s = q by TARSKI:def 1;

              hence (the carrier of (F . s) /\ the carrier of (F . t)) = {( 1_ G)} by A17, TARSKI:def 1;

            end;

            

             A18: for x be Element of I holds (F . x) is strict Subgroup of G & ( card (F . x)) = (( prime_factorization ( card G)) . x)

            proof

              let x be Element of I;

              x in ( support f) by TARSKI:def 1, A7;

              then

               A20: x in ( support ( pfexp ( card G))) by NAT_3:def 9;

              

               A21: x = q by TARSKI:def 1;

              ( card (F . x)) = ( card G)

              .= (f . x) by A21, A20, NAT_3:def 9, A14;

              hence thesis by GROUP_2: 54;

            end;

            

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

            

             A23: 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 A22, GROUP_7:def 6, A23, GROUP_7:def 7, GROUP_7:def 8;

            take I, F;

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

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

            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 A24, Th25;

            hence thesis by A9, A24, A16, A18;

          end;

            suppose

             A25: n <> 0 ;

            set f = ( prime_factorization ( card G));

            

             A26: ( Product f) = ( card G) by NAT_3: 61;

            

             A27: ( support f) = ( support ( pfexp ( card G))) by NAT_3:def 9;

            ( support f) <> {} by A4;

            then

            consider q be object such that

             A28: q in ( support f) by XBOOLE_0:def 1;

            reconsider q as Prime by A27, A28, NAT_3: 34;

            reconsider Gq = (q |^ (q |-count ( card G))) as non zero Nat;

            set g = ( prime_factorization Gq);

            set h = (f -' g);

            (q |-count ( card G)) <> 0

            proof

              assume (q |-count ( card G)) = 0 ;

              then (f . q) = 0 by NAT_3: 55;

              hence contradiction by A28, PRE_POLY:def 7;

            end;

            then

             A29: ( support ( pfexp Gq)) = {q} by NAT_3: 42;

            then q in ( support ( pfexp Gq)) by TARSKI:def 1;

            then

             A30: (g . q) = (q |^ (q |-count Gq)) by NAT_3:def 9;

            

             A31: (g . q) = (q |^ (q |-count ( card G))) by NAT_3: 25, INT_2:def 4, A30;

            

             A32: ( support g) = {q} by A29, NAT_3:def 9;

            

             A33: for x be object holds x in ( support h) iff x in (( support f) \ {q})

            proof

              let x be object;

              hereby

                assume

                 A34: x in ( support h);

                then

                 A35: x in ( support f) by PRE_POLY: 39, TARSKI:def 3;

                then

                 A36: x in ( support ( pfexp ( card G))) by NAT_3:def 9;

                 not x in {q}

                proof

                  assume x in {q};

                  then

                   A37: x = q by TARSKI:def 1;

                  (h . x) = ((f . x) -' (g . x)) by PRE_POLY:def 6

                  .= ((q |^ (q |-count ( card G))) -' (g . q)) by A37, A36, NAT_3:def 9

                  .= ((q |^ (q |-count ( card G))) -' (q |^ (q |-count ( card G)))) by NAT_3: 25, INT_2:def 4, A30

                  .= ((q |^ (q |-count ( card G))) - (q |^ (q |-count ( card G)))) by XREAL_0:def 2

                  .= 0 ;

                  hence contradiction by A34, PRE_POLY:def 7;

                end;

                hence x in (( support f) \ {q}) by XBOOLE_0:def 5, A35;

              end;

              assume x in (( support f) \ {q});

              then

               A38: x in ( support f) & not x in {q} by XBOOLE_0:def 5;

              x in ( support ( pfexp ( card G))) by A38, NAT_3:def 9;

              then

              reconsider x0 = x as Prime by NAT_3: 34;

              

               A39: (h . x0) = ((f . x0) -' (g . x0)) by PRE_POLY:def 6;

              

               A40: (g . x0) = 0 by A38, A32, PRE_POLY:def 7;

              (f . x0) <> 0 by A38, PRE_POLY:def 7;

              then (h . x) <> 0 by A39, A40, NAT_D: 40;

              hence x in ( support h) by PRE_POLY:def 7;

            end;

            then

             A41: ( support h) = (( support f) \ {q}) by TARSKI: 2;

            then

             A42: ( support h) misses ( support g) by A32, XBOOLE_1: 79;

            reconsider h as bag of SetPrimes ;

            

             A43: for x be Prime st x in ( support h) holds ex n be Nat st 0 < n & (h . x) = (x |^ n)

            proof

              let x be Prime;

              assume x in ( support h);

              then

               A44: x in ( support f) & not x in {q} by XBOOLE_0:def 5, A41;

              

               A45: (h . x) = ((f . x) -' (g . x)) by PRE_POLY:def 6;

              (g . x) = 0 by A44, A32, PRE_POLY:def 7;

              then (h . x) = (f . x) by A45, NAT_D: 40;

              hence thesis by A44, INT_7:def 1;

            end;

            then

             A46: h is prime-factorization-like by INT_7:def 1;

            

             A47: {q} c= ( support f) by A28, ZFMISC_1: 31;

            

             A48: ( support h) c= ( support f) by XBOOLE_1: 36, A41;

            

             A49: (( support h) \/ {q}) = ( support f) by A28, ZFMISC_1: 31, A41, XBOOLE_1: 45;

            for x be object st x in SetPrimes holds (f . x) = ((h . x) + (g . x))

            proof

              let x be object;

              assume x in SetPrimes ;

              per cases ;

                suppose

                 A50: not x in ( support f);

                then

                 A51: not x in ( support h) by A48;

                

                 A52: not x in ( support g) by A32, A47, A50;

                

                thus (f . x) = 0 qua Real by PRE_POLY:def 7, A50

                .= ((h . x) + 0 qua Real) by PRE_POLY:def 7, A51

                .= ((h . x) + (g . x)) by PRE_POLY:def 7, A52;

              end;

                suppose

                 A53: x in ( support f);

                

                 A54: x in ( support ( pfexp ( card G))) by A53, NAT_3:def 9;

                thus (f . x) = ((h . x) + (g . x))

                proof

                  per cases by A53, A49, XBOOLE_0:def 3;

                    suppose x in ( support h);

                    then

                     A55: x in ( support f) & not x in {q} by A41, XBOOLE_0:def 5;

                    x in ( support ( pfexp ( card G))) by A55, NAT_3:def 9;

                    then

                    reconsider x0 = x as Prime by NAT_3: 34;

                    

                     A56: (h . x0) = ((f . x0) -' (g . x0)) by PRE_POLY:def 6;

                    (g . x0) = 0 by A55, A32, PRE_POLY:def 7;

                    hence thesis by A56, NAT_D: 40;

                  end;

                    suppose x in {q};

                    then

                     A57: x = q by TARSKI:def 1;

                    

                     A58: (h . x) = ((f . q) -' (g . q)) by A57, PRE_POLY:def 6;

                    (f . q) = (q |^ (q |-count ( card G))) by A57, A54, NAT_3:def 9;

                    then (h . x) = ((f . q) - (g . q)) by A58, XREAL_0:def 2, A31;

                    hence thesis by A57;

                  end;

                end;

              end;

            end;

            then (h + g) = f by PRE_POLY: 33;

            then

             A59: ( Product f) = (( Product h) * ( Product g)) by A32, XBOOLE_1: 79, A41, NAT_3: 19;

            ( Product h) is non zero & ( Product g) is non zero by A59, NAT_3: 61;

            then

            consider H,K be strict finite Subgroup of G such that

             A60: ( card H) = ( Product h) & ( card K) = ( Product g) & (the carrier of H /\ the carrier of K) = {( 1_ G)} & ex F be Homomorphism of ( product <*H, K*>), G st F is bijective & for a,b be Element of G st a in H & b in K holds (F . <*a, b*>) = (a * b) by A26, A59, Th18, A46, A42, INT_7: 12;

            reconsider H, K as finite commutative Group;

            

             A61: ( support ( prime_factorization ( card H))) = ( support h) by INT_7: 16, INT_7:def 1, A43, A60;

            ( card ( support ( prime_factorization ( card H)))) = ( card ( support h)) by INT_7: 16, INT_7:def 1, A43, A60

            .= (( card ( support f)) - ( card {q})) by A41, A28, EULER_1: 4

            .= ((n + 1) - 1) by A4, CARD_1: 30

            .= n;

            then

            consider I0 be non empty finite set, F0 be associative Group-like commutative multMagma-Family of I0, HFG0 be Homomorphism of ( product F0), H such that

             A62: I0 = ( support ( prime_factorization ( card H))) & (for p be Element of I0 holds (F0 . p) is strict Subgroup of H & ( card (F0 . p)) = (( prime_factorization ( card H)) . p)) & (for p,q be Element of I0 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 totalI0 -defined Function st for p be Element of I0 holds (x . p) in (F0 . p) holds x in ( product F0) & (HFG0 . x) = ( Product x) by A3, A25;

            set I = (I0 \/ {q});

            reconsider I as non empty finite set;

            

             A63: ( Product ( prime_factorization ( card H))) = ( Product h) by A60, NAT_3: 61;

            then

             A64: ( prime_factorization ( card H)) = h by A46, INT_7: 15;

            

             A65: I = ( support ( prime_factorization ( card G))) by A62, A49, A46, INT_7: 15, A63;

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

            

             A67: ( 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 RELAT_1:def 18;

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

            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

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

              

               A69: x in (( dom F0) \/ ( dom (q .--> K))) by A68, FUNCT_4:def 1;

              

               A70: I0 = ( support h) by INT_7: 16, INT_7:def 1, A43, A60, A62

              .= (( support f) \ {q}) by TARSKI: 2, A33;

              per cases by XBOOLE_0:def 3, A68;

                suppose

                 A71: x in I0;

                then not x in ( dom (q .--> K)) by A70, XBOOLE_0:def 5;

                then

                 A72: (F . x) = (F0 . x) by FUNCT_4:def 1, A69;

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

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

                hence y is non empty multMagma by A72, A68, GROUP_7:def 1;

              end;

                suppose

                 A73: x in {q};

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

                hence y is non empty multMagma by A68, A73, FUNCOP_1: 7;

              end;

            end;

            then

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

            

             A74: for x be Element of I holds (F . x) is strict Subgroup of G & ( card (F . x)) = (( prime_factorization ( card G)) . x)

            proof

              let x be Element of I;

              

               A75: x in ( dom F) by A67;

              

               A76: x in (( dom F0) \/ ( dom (q .--> K))) by A75, FUNCT_4:def 1;

              

               A77: I0 = ( support h) by INT_7: 16, INT_7:def 1, A43, A60, A62

              .= (( support f) \ {q}) by A33, TARSKI: 2;

              per cases by XBOOLE_0:def 3;

                suppose

                 A78: x in I0;

                then not x in ( dom (q .--> K)) by A77, XBOOLE_0:def 5;

                then

                 A79: (F . x) = (F0 . x) by FUNCT_4:def 1, A76;

                reconsider p = x as Element of I0 by A78;

                

                 A80: (F0 . p) is strict Subgroup of H & ( card (F0 . p)) = (( prime_factorization ( card H)) . p) by A62;

                

                 A81: x in ( support f) & not x in {q} by A41, XBOOLE_0:def 5, A61, A62, A78;

                x in ( support ( pfexp ( card G))) by A81, NAT_3:def 9;

                then

                reconsider x0 = x as Prime by NAT_3: 34;

                

                 A82: (h . x0) = ((f . x0) -' (g . x0)) by PRE_POLY:def 6;

                (g . x0) = 0 by A81, A32, PRE_POLY:def 7;

                hence (F . x) is strict Subgroup of G & ( card (F . x)) = (( prime_factorization ( card G)) . x) by A79, A80, GROUP_2: 56, A64, A82, NAT_D: 40;

              end;

                suppose

                 A83: x in {q};

                then

                 A84: (F . x) = ((q .--> K) . x) by FUNCT_4:def 1, A76;

                x in ( support f) by A83, A47;

                then

                 A85: x in ( support ( pfexp ( card G))) by NAT_3:def 9;

                

                 A86: x = q by TARSKI:def 1, A83;

                ( card (F . x)) = ( Product g) by A60, A83, FUNCOP_1: 7, A84

                .= Gq by NAT_3: 61

                .= (f . x) by A86, A85, NAT_3:def 9;

                hence (F . x) is strict Subgroup of G & ( card (F . x)) = (( prime_factorization ( card G)) . x) by A84, A83, FUNCOP_1: 7;

              end;

            end;

            

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

            

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

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

            then

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

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

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

            

             A90: I0 = ( support h) by INT_7: 16, INT_7:def 1, A43, A60, A62

            .= (( support f) \ {q}) by TARSKI: 2, A33

            .= (I \ {q}) by A62, A49, A46, INT_7: 15, A63;

            

             A91: not q in I0

            proof

              assume q in I0;

              then q in I & not q in {q} by A90, XBOOLE_0:def 5;

              hence contradiction by TARSKI:def 1;

            end;

            then

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

             A92: 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 Th28, A62, A28, A65;

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

            

             A93: HFG is onto by FUNCT_2: 27, A89, A92;

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

            

             A94: 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

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

              then x in the carrier of ( product F) by Th29;

              then

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

               A96: x0 in ( product F0) & x = (x0 +* (q .--> k)) & for p be Element of I0 holds (x0 . p) in (F0 . p) by Th30, A91, A28, A65;

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

              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

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

                reconsider z as Element of I0 by A97;

                

                 A98: (x0 . z) in (F0 . z) by A96;

                (F0 . z) is strict Subgroup of H by A62;

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

              end;

              then

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

              

               A99: (HFG0 . x0) = ( Product x0) by A62, A96;

              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;

              

               A100: ( Product x0) = ( Product xx0) by Th32;

              thus x in ( product F) by Th29, A95;

              

               A101: hh in H & kk in K;

              

              thus (HFG . x) = (FHKG . (FHK . x)) by FUNCT_2: 15, Th29, A95

              .= (FHKG . <*hh, kk*>) by A92, A96

              .= (hh * kk) by A89, A101

              .= ( Product x) by A99, A100, Th33, A91, A28, A65, A96;

            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

               A102: s <> t;

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

              then

               A103: 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;

                

                 A104: s in (( dom F0) \/ ( dom (q .--> K))) by A103, FUNCT_4:def 1;

                

                 A105: t in (( dom F0) \/ ( dom (q .--> K))) by A103, FUNCT_4:def 1;

                

                 A106: I0 = ( support h) by INT_7: 16, INT_7:def 1, A43, A60, A62

                .= (( support f) \ {q}) by TARSKI: 2, A33;

                then not ss in ( dom (q .--> K)) by XBOOLE_0:def 5;

                then

                 A107: (F . ss) = (F0 . ss) by FUNCT_4:def 1, A104;

                 not tt in ( dom (q .--> K)) by A106, XBOOLE_0:def 5;

                then

                 A108: (F . tt) = (F0 . tt) by FUNCT_4:def 1, A105;

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

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

              end;

                suppose

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

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

                proof

                  per cases by A109;

                    suppose

                     A110: not s in I0;

                    

                     A111: s in (( dom F0) \/ ( dom (q .--> K))) by A103, FUNCT_4:def 1;

                    

                     A112: s in {q} by A110, A90, XBOOLE_0:def 5;

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

                    then

                     A113: (F . s) = K by A112, FUNCOP_1: 7;

                    t in I0

                    proof

                      assume not t in I0;

                      then not t in I or t in {q} by XBOOLE_0:def 5, A90;

                      then t = q by TARSKI:def 1;

                      hence contradiction by A102, TARSKI:def 1, A112;

                    end;

                    then

                    reconsider tt = t as Element of I0;

                    

                     A114: tt in (( dom F0) \/ ( dom (q .--> K))) by A103, FUNCT_4:def 1;

                    I0 = ( support h) by INT_7: 16, INT_7:def 1, A43, A60, A62

                    .= (( support f) \ {q}) by TARSKI: 2, A33;

                    then not tt in ( dom (q .--> K)) by XBOOLE_0:def 5;

                    then

                     A115: (F . tt) = (F0 . tt) by FUNCT_4:def 1, A114;

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

                    

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

                    

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

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

                    then ( 1_ G) in the carrier of S1 by GROUP_2: 44;

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

                    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 A113, A115, A116, XBOOLE_0:def 10;

                  end;

                    suppose

                     A118: not t in I0;

                    

                     A119: t in (( dom F0) \/ ( dom (q .--> K))) by A103, FUNCT_4:def 1;

                    

                     A120: t in {q} by A118, A90, XBOOLE_0:def 5;

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

                    then

                     A121: (F . t) = K by A120, FUNCOP_1: 7;

                    s in I0

                    proof

                      assume not s in I0;

                      then not s in I or s in {q} by XBOOLE_0:def 5, A90;

                      then s = q by TARSKI:def 1;

                      hence contradiction by A102, TARSKI:def 1, A120;

                    end;

                    then

                    reconsider ss = s as Element of I0;

                    

                     A122: ss in (( dom F0) \/ ( dom (q .--> K))) by A103, FUNCT_4:def 1;

                    I0 = ( support h) by INT_7: 16, INT_7:def 1, A43, A60, A62

                    .= (( support f) \ {q}) by A33, TARSKI: 2;

                    then not ss in ( dom (q .--> K)) by XBOOLE_0:def 5;

                    then

                     A123: (F . ss) = (F0 . ss) by FUNCT_4:def 1, A122;

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

                    

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

                    

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

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

                    then ( 1_ G) in the carrier of S1 by GROUP_2: 44;

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

                    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 A121, A123, A124, XBOOLE_0:def 10;

                  end;

                end;

              end;

            end;

            hence thesis by A65, A74, A93, A89, A92, A94;

          end;

        end;

      end;

      

       A126: for k be Nat holds P[k] from NAT_1:sch 2( A1, A2);

      let G be strict finite commutative Group;

      assume

       A127: ( card G) > 1;

      ( card ( support ( prime_factorization ( card G)))) <> 0

      proof

        assume ( card ( support ( prime_factorization ( card G)))) = 0 ;

        then ( support ( prime_factorization ( card G))) = {} ;

        hence contradiction by A127, NAT_3: 57;

      end;

      hence thesis by A126;

    end;

    theorem :: GROUP_17:35

    for G be strict finite commutative Group st ( card G) > 1 holds ex I be non empty finite set, F be associative Group-like commutative multMagma-Family of I st I = ( support ( prime_factorization ( card G))) & (for p be Element of I holds (F . p) is strict Subgroup of G & ( card (F . p)) = (( prime_factorization ( card G)) . p)) & (for p,q be Element of I 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 totalI -defined Function st (for p be Element of I holds (x . p) in (F . p)) & y = ( Product x)) & for x1,x2 be the carrier of G -valued totalI -defined Function st (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) holds x1 = x2

    proof

      let G be strict finite commutative Group;

      assume ( card G) > 1;

      then

      consider I be non empty finite set, F be associative Group-like commutative multMagma-Family of I, HFG be Homomorphism of ( product F), G such that

       A1: I = ( support ( prime_factorization ( card G))) & (for p be Element of I holds (F . p) is strict Subgroup of G & ( card (F . p)) = (( prime_factorization ( card G)) . p)) & (for p,q be Element of I 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 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 Th34;

      

       A2: 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 A1, FUNCT_2:def 3;

        then

        consider x be object such that

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

        reconsider x as totalI -defined Function by A3, Lm6;

        

         A4: 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

           A5: R = (F . p) & (x . p) in the carrier of R by Lm7, A3;

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

        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

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

          reconsider i as Element of I by A6;

          consider R be non empty multMagma such that

           A7: R = (F . i) & (x . i) in the carrier of R by A3, Lm7;

          (F . i) is strict Subgroup of G by A1;

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

          hence y in the carrier of G by A6, A7;

        end;

        then

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

        take x;

        thus thesis by A1, A3, A4;

      end;

      now

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

        assume

         A8: (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 A8, A1;

        then

         A9: (HFG . x1) = (HFG . x2) by A8, A1;

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

        hence x1 = x2 by A9, A1, FUNCT_2: 19;

      end;

      hence thesis by A1, A2;

    end;