group_20.miz



    begin

    definition

      let I be set, G be Group;

      :: GROUP_20:def1

      mode Subgroup-Family of I,G -> Group-Family of I means

      : Def1: for i be object st i in I holds (it . i) is Subgroup of G;

      existence

      proof

        deffunc f( object) = ( (1). G);

        consider F be Function such that

         A1: ( dom F) = I and

         A2: for i be object st i in I holds (F . i) = f(i) from FUNCT_1:sch 3;

        for i be object st i in I holds (F . i) is Group by A2;

        then

        reconsider F as Group-Family of I by A1, GROUP_19: 2;

        take F;

        thus thesis by A2;

      end;

    end

    definition

      let I be set, G be Group, F be Subgroup-Family of I, G;

      :: GROUP_20:def2

      attr F is component-commutative means for i,j be object, gi,gj be Element of G st i in I & j in I & i <> j holds ex Fi,Fj be Subgroup of G st Fi = (F . i) & Fj = (F . j) & (gi in Fi & gj in Fj implies (gi * gj) = (gj * gi));

    end

    definition

      let I be non empty set, G be Group, F be Subgroup-Family of I, G;

      :: original: component-commutative

      redefine

      :: GROUP_20:def3

      attr F is component-commutative means

      : Def2: for i,j be Element of I, gi,gj be Element of G st i <> j & gi in (F . i) & gj in (F . j) holds (gi * gj) = (gj * gi);

      compatibility

      proof

        thus F is component-commutative implies for i,j be Element of I, gi,gj be Element of G st i <> j & gi in (F . i) & gj in (F . j) holds (gi * gj) = (gj * gi)

        proof

          assume

           A1: F is component-commutative;

          let i,j be Element of I, gi,gj be Element of G;

          assume i <> j;

          then ex Fi,Fj be Subgroup of G st Fi = (F . i) & Fj = (F . j) & (gi in Fi & gj in Fj implies (gi * gj) = (gj * gi)) by A1;

          hence thesis;

        end;

        assume

         A2: for i,j be Element of I, gi,gj be Element of G st i <> j & gi in (F . i) & gj in (F . j) holds (gi * gj) = (gj * gi);

        let i,j be object, gi,gj be Element of G;

        assume that

         A3: i in I & j in I and

         A4: i <> j;

        reconsider Fi = (F . i), Fj = (F . j) as Subgroup of G by A3, Def1;

        take Fi, Fj;

        thus thesis by A2, A3, A4;

      end;

    end

    registration

      let I be non empty set, G be Group;

      cluster component-commutative for Subgroup-Family of I, G;

      existence

      proof

        deffunc f( object) = ( (1). G);

        consider F be Function such that

         A1: ( dom F) = I and

         A2: for i be object st i in I holds (F . i) = f(i) from FUNCT_1:sch 3;

        for i be object st i in I holds (F . i) is Group by A2;

        then

        reconsider F as Group-Family of I by A1, GROUP_19: 2;

        for i be object st i in I holds (F . i) is Subgroup of G by A2;

        then

        reconsider F as Subgroup-Family of I, G by Def1;

        take F;

        for i,j be Element of I, gi,gj be Element of G st i <> j & gi in (F . i) & gj in (F . j) holds (gi * gj) = (gj * gi)

        proof

          let i,j be Element of I;

          let gi,gj be Element of G;

          assume i <> j & gi in (F . i) & gj in (F . j);

          then gi in ( (1). G) & gj in ( (1). G) by A2;

          then gi in {( 1_ G)} & gj in {( 1_ G)} by GROUP_2:def 7;

          then gi = ( 1_ G) & gj = ( 1_ G) by TARSKI:def 1;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: GROUP_20:1

    

     Th1: for G be Group, H be normal Subgroup of G, x,y be Element of G st y in H holds ((x * y) * (x " )) in H & (x * (y * (x " ))) in H

    proof

      let G be Group, H be normal Subgroup of G, x,y be Element of G;

      assume

       A1: y in H;

      (x * H) = (H * x) by GROUP_3: 117;

      then

      consider g be Element of G such that

       A2: (x * y) = (g * x) & g in H by A1, GROUP_2: 103, GROUP_2: 104;

      ((x * y) * (x " )) = g by A2, GROUP_3: 1;

      hence thesis by A2, GROUP_1:def 3;

    end;

    theorem :: GROUP_20:2

    

     Th2: for I be non empty set, G be Group, F be Group-Family of I, x be Function of I, G st x in ( product F) holds x is Function of I, ( Union ( Carrier F))

    proof

      let I be non empty set, G be Group, F be Group-Family of I, x be Function of I, G;

      assume

       A1: x in ( product F);

      

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

      for z be object st z in ( rng x) holds z in ( Union ( Carrier F))

      proof

        let z be object;

        assume z in ( rng x);

        then

        consider i be object such that

         A3: i in I & z = (x . i) by FUNCT_2: 11;

        reconsider i as Element of I by A3;

        (x . i) in (F . i) by A1, GROUP_19: 5;

        then z in ( [#] (F . i)) by A3;

        then

         A4: z in (( Carrier F) . i) by PENCIL_3: 7;

        (( Carrier F) . i) in ( rng ( Carrier F)) by A2, FUNCT_1: 3;

        then z in ( union ( rng ( Carrier F))) by A4, TARSKI:def 4;

        hence z in ( Union ( Carrier F)) by CARD_3:def 4;

      end;

      then ( rng x) c= ( Union ( Carrier F));

      hence x is Function of I, ( Union ( Carrier F)) by FUNCT_2: 6;

    end;

    theorem :: GROUP_20:3

    

     Th3: for I be non empty set, G be Group, H be Subgroup of G, x be Function of I, G, y be Function of I, H st x = y holds ( support x) = ( support y)

    proof

      let I be non empty set, G be Group, H be Subgroup of G, x be Function of I, G, y be Function of I, H;

      assume

       A1: x = y;

      for i be object holds i in ( support x) iff i in ( support y)

      proof

        let i be object;

        

         A2: i in ( support x) iff (x . i) <> ( 1_ G) & i in I by GROUP_19:def 2;

        i in ( support y) iff (y . i) <> ( 1_ H) & i in I by GROUP_19:def 2;

        hence thesis by A1, A2, GROUP_2: 44;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: GROUP_20:4

    

     Th4: for I be non empty set, G be Group, H be Subgroup of G, y be finite-support Function of I, H holds y is finite-support Function of I, G

    proof

      let I be non empty set, G be Group, H be Subgroup of G, y be finite-support Function of I, H;

      ( [#] H) c= ( [#] G) by GROUP_2:def 5;

      then

      reconsider x = y as Function of I, G by FUNCT_2: 7;

      ( support x) = ( support y) by Th3;

      hence thesis by GROUP_19:def 3;

    end;

    theorem :: GROUP_20:5

    

     Th5: for I be non empty set, G be Group, H be Subgroup of G, x be finite-support Function of I, G st ( rng x) c= ( [#] H) holds x is finite-support Function of I, H

    proof

      let I be non empty set, G be Group, H be Subgroup of G, x be finite-support Function of I, G;

      assume ( rng x) c= ( [#] H);

      then

      reconsider y = x as Function of I, H by FUNCT_2: 6;

      ( support x) = ( support y) by Th3;

      hence thesis by GROUP_19:def 3;

    end;

    theorem :: GROUP_20:6

    

     Th6: for I be non empty set, G be Group, H be Subgroup of G, x be finite-support Function of I, G, y be finite-support Function of I, H st x = y holds ( Product x) = ( Product y)

    proof

      let I be non empty set, G be Group, H be Subgroup of G, x be finite-support Function of I, G, y be finite-support Function of I, H;

      assume

       A1: x = y;

      then

       A2: ( support x) = ( support y) by Th3;

      reconsider fx = ((x | ( support x)) * ( canFS ( support x))) as FinSequence of G by FINSEQ_2: 32;

      reconsider fy = ((y | ( support y)) * ( canFS ( support y))) as FinSequence of H by FINSEQ_2: 32;

      

      thus ( Product x) = ( Product fx) by GROUP_17:def 1

      .= ( Product fy) by A1, A2, GROUP_19: 45

      .= ( Product y) by GROUP_17:def 1;

    end;

    theorem :: GROUP_20:7

    

     Th7: for f be Function, i,x be set holds f = ((f +* (i,x)) +* (i,(f . i)))

    proof

      let f be Function, i,x be set;

      

      thus f = (f +* (i,(f . i))) by FUNCT_7: 35

      .= ((f +* (i,x)) +* (i,(f . i))) by FUNCT_7: 34;

    end;

    theorem :: GROUP_20:8

    

     Th8: for I be non empty set, G be Group, F be component-commutative Subgroup-Family of I, G, x,y be finite-support Function of I, G, i be Element of I st y = (x +* (i,( 1_ (F . i)))) & x in ( product F) holds ( Product x) = (( Product y) * (x . i)) = ((x . i) * ( Product y))

    proof

      let I be non empty set, G be Group, F be component-commutative Subgroup-Family of I, G, x,y be finite-support Function of I, G, i be Element of I;

      

       A1: for i be object st i in I holds (F . i) is Subgroup of G by Def1;

      

       A2: for i,j be Element of I, gi,gj be Element of G st i <> j & gi in (F . i) & gj in (F . j) holds (gi * gj) = (gj * gi) by Def2;

      assume that

       A3: y = (x +* (i,( 1_ (F . i)))) and

       A4: x in ( product F);

      

       A5: for i be Element of I holds (F . i) is Subgroup of G by Def1;

      reconsider px = x as Element of ( product F) by A4;

      

       A6: (x . i) in (F . i) by A4, GROUP_19: 5;

      y in ( product F) by A3, A4, GROUP_19: 24;

      then

      reconsider py = y as Element of ( product F);

      ( support y) = ( support (py,F)) by A1, GROUP_19: 9;

      then py in ( sum F) by GROUP_19: 8;

      then

      reconsider sy = py as Element of ( sum F);

      set z = (( 1_ ( product F)) +* (i,(x . i)));

      

       A7: z in ( sum F) by A6, GROUP_19: 25, GROUP_2: 46;

      then

       A8: z in ( product F) by GROUP_2: 40;

      reconsider sz = z as Element of ( sum F) by A7;

      reconsider pz = z as Element of ( product F) by A8;

      reconsider z as finite-support Function of I, G by A1, A7, GROUP_19: 10;

      

       A9: ( dom x) = I by A4, GROUP_19: 3;

      (sy * sz) is Element of ( product F) by GROUP_2: 42;

      then

       A10: ( dom (sy * sz)) = I by GROUP_19: 3;

      

       A11: ( dom ( 1_ ( product F))) = I by GROUP_19: 3;

      

       A12: x = (sy * sz)

      proof

        for j be object st j in I holds (x . j) = ((sy * sz) . j)

        proof

          let j be object;

          assume j in I;

          then

          reconsider j as Element of I;

          (y . j) in (F . j) by A3, A4, GROUP_19: 5, GROUP_19: 24;

          then

          reconsider yj = (y . j) as Element of (F . j);

          (z . j) in (F . j) by A7, GROUP_19: 5, GROUP_2: 40;

          then

          reconsider zj = (z . j) as Element of (F . j);

          per cases ;

            suppose

             A13: j = i;

            then

             A14: (y . j) = ( 1_ (F . j)) by A3, A9, FUNCT_7: 31;

            (z . j) = (x . j) by A11, A13, FUNCT_7: 31;

            then (yj * zj) = (x . j) by A14, GROUP_1:def 4;

            then (px . j) = ((py * pz) . j) by GROUP_7: 1;

            hence thesis by GROUP_2: 43;

          end;

            suppose

             A15: j <> i;

            then

             A16: (y . j) = (x . j) by A3, FUNCT_7: 32;

            (( 1_ ( product F)) . j) = ( 1_ (F . j)) by GROUP_7: 6;

            then (z . j) = ( 1_ (F . j)) by A15, FUNCT_7: 32;

            then (yj * zj) = (x . j) by A16, GROUP_1:def 4;

            then (px . j) = ((py * pz) . j) by GROUP_7: 1;

            hence thesis by GROUP_2: 43;

          end;

        end;

        hence thesis by A9, A10, FUNCT_1: 2;

      end;

      

       A17: (sy * sz) = (sz * sy)

      proof

        

         A18: ( support (py,F)) = (( support (px,F)) \ {i}) by A3, A9, GROUP_19: 27;

        

         A19: ( support (py,F)) misses ( support (pz,F)) by A6, A18, GROUP_19: 17, XBOOLE_1: 85;

        

        thus (sy * sz) = (py * pz) by GROUP_2: 43

        .= (pz * py) by A19, GROUP_19: 32

        .= (sz * sy) by GROUP_2: 43;

      end;

      

       A20: ( Product x) = (( Product y) * ( Product z)) by A2, A5, A12, GROUP_19: 53;

      ( 1_ ( product F)) = (I --> ( 1_ G)) by A5, GROUP_19: 13;

      then ( Product z) = (x . i) by GROUP_19: 21;

      hence thesis by A2, A5, A12, A17, A20, GROUP_19: 53;

    end;

    theorem :: GROUP_20:9

    

     Th9: for I be non empty set, G be Group, F be component-commutative Subgroup-Family of I, G, UF be Subset of G holds for i be Element of I, x,y be finite-support Function of I, ( gr UF) st y = (x +* (i,( 1_ (F . i)))) & x in ( product F) holds ( Product x) = (( Product y) * (x . i)) = ((x . i) * ( Product y))

    proof

      let I be non empty set, G be Group, F be component-commutative Subgroup-Family of I, G, UF be Subset of G;

      let i be Element of I, x,y be finite-support Function of I, ( gr UF);

      assume that

       A1: y = (x +* (i,( 1_ (F . i)))) and

       A2: x in ( product F);

      reconsider x0 = x, y0 = y as finite-support Function of I, G by Th4;

      

       A3: ( Product x) = ( Product x0) by Th6;

      

       A4: ( Product y) = ( Product y0) by Th6;

      

       A5: ( Product x0) = (( Product y0) * (x0 . i)) = ((x0 . i) * ( Product y0)) by A1, A2, Th8;

      then ( Product x) = (( Product y) * (x . i)) by A3, A4, GROUP_2: 43;

      hence thesis by A3, A4, A5, GROUP_2: 43;

    end;

    theorem :: GROUP_20:10

    

     Th10: for I be non empty set, G be Group, F be component-commutative Subgroup-Family of I, G, UF be Subset of G holds for y be finite-support Function of I, ( gr UF), i be Element of I, g be Element of ( gr UF) st y in ( product F) & (y . i) = ( 1_ (F . i)) & g in (F . i) holds (( Product y) * g) = (g * ( Product y))

    proof

      let I be non empty set, G be Group, F be component-commutative Subgroup-Family of I, G, UF be Subset of G;

      let y be finite-support Function of I, ( gr UF), i be Element of I, g be Element of ( gr UF);

      assume that

       A1: y in ( product F) and

       A2: (y . i) = ( 1_ (F . i)) and

       A3: g in (F . i);

      reconsider x = (y +* (i,g)) as finite-support Function of I, ( gr UF) by GROUP_19: 26;

      

       A4: y = (x +* (i,( 1_ (F . i)))) by A2, Th7;

      

       A5: x in ( product F) by A1, A3, GROUP_19: 24;

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

      then (x . i) = g by FUNCT_7: 31;

      hence thesis by A4, A5, Th9;

    end;

    theorem :: GROUP_20:11

    

     Th11: for I be non empty set, G be Group, F be component-commutative Subgroup-Family of I, G, UF be Subset of G st UF = ( Union ( Carrier F)) holds for g be Element of G, H be FinSequence of G, K be FinSequence of INT st ( len H) = ( len K) & ( rng H) c= UF & ( Product (H |^ K)) = g holds ex f be finite-support Function of I, G st f in ( product F) & g = ( Product f)

    proof

      let I be non empty set, G be Group, F be component-commutative Subgroup-Family of I, G, UF be Subset of G;

      assume

       A1: UF = ( Union ( Carrier F));

      defpred P[ Nat] means for g be Element of G, H be FinSequence of G, K be FinSequence of INT st ( len H) = $1 & ( len H) = ( len K) & ( rng H) c= UF & ( Product (H |^ K)) = g holds ex f be finite-support Function of I, G st f in ( product F) & g = ( Product f);

      

       A2: P[ 0 ]

      proof

        let g be Element of G, H be FinSequence of G, K be FinSequence of INT such that

         A3: ( len H) = 0 & ( len H) = ( len K) & ( rng H) c= UF & ( Product (H |^ K)) = g;

        H = ( <*> ( [#] G)) & K = ( <*> INT ) by A3;

        then

         A4: (H |^ K) = ( <*> ( [#] G)) by GROUP_4: 21;

        reconsider f = (I --> ( 1_ G)) as Function of I, G;

        ( support f) is finite by GROUP_19: 12;

        then

        reconsider f as finite-support Function of I, G by GROUP_19:def 3;

        take f;

        for i be Element of I holds (F . i) is Subgroup of G by Def1;

        then f = ( 1_ ( product F)) by GROUP_19: 13;

        hence f in ( product F);

        ( Product f) = ( 1_ G) by GROUP_19: 16;

        hence g = ( Product f) by A3, A4, GROUP_4: 8;

      end;

      

       A5: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume

         A6: P[n];

        let g be Element of G, H be FinSequence of G, K be FinSequence of INT such that

         A7: ( len H) = (n + 1) & ( len H) = ( len K) & ( rng H) c= UF & ( Product (H |^ K)) = g;

        reconsider h = (H /. (n + 1)) as Element of G;

        reconsider k = (K /. (n + 1)) as Element of INT ;

        reconsider H0 = (H | n) as FinSequence of G;

        reconsider K0 = (K | n) as FinSequence of INT ;

        reconsider H1 = <*h*> as FinSequence of G;

        reconsider K1 = <*k*> as FinSequence of INT ;

        ( rng H0) c= ( rng H) by RELAT_1: 70;

        then

         A8: ( rng H0) c= UF by A7;

        

         A9: <*( @ k)*> = K1 by GROUP_4:def 1;

        (n + 1) in ( Seg (n + 1)) by FINSEQ_1: 4;

        then

         A10: (n + 1) in ( dom H) & (n + 1) in ( dom K) by A7, FINSEQ_1:def 3;

        then (H /. (n + 1)) = (H . (n + 1)) & (K /. (n + 1)) = (K . (n + 1)) by PARTFUN1:def 6;

        then

         A11: H = (H0 ^ H1) & K = (K0 ^ K1) by A7, FINSEQ_3: 55;

        h = (H . (n + 1)) by A10, PARTFUN1:def 6;

        then

         A12: h in UF by A7, A10, FUNCT_1: 3;

        n <= ( len H) & n <= ( len K) by A7, XREAL_1: 31;

        then

         A13: ( len H0) = n & ( len K0) = n by FINSEQ_1: 17;

        

         A14: ( len H1) = 1 & ( len K1) = 1 by FINSEQ_1: 39;

        

         A15: (H |^ K) = ((H0 |^ K0) ^ (H1 |^ K1)) by A11, A13, A14, GROUP_4: 19

        .= ((H0 |^ K0) ^ <*(h |^ k)*>) by A9, GROUP_4: 22;

        consider f0 be finite-support Function of I, G such that

         A16: f0 in ( product F) & ( Product (H0 |^ K0)) = ( Product f0) by A6, A8, A13;

        h in ( union ( rng ( Carrier F))) by A1, A12, CARD_3:def 4;

        then

        consider Fi be set such that

         A17: h in Fi & Fi in ( rng ( Carrier F)) by TARSKI:def 4;

        consider i be object such that

         A18: i in ( dom ( Carrier F)) & Fi = (( Carrier F) . i) by A17, FUNCT_1:def 3;

        reconsider i as Element of I by A18;

        

         A19: (F . i) is Subgroup of G by Def1;

        (( Carrier F) . i) = ( [#] (F . i)) by PENCIL_3: 7;

        then h in (F . i) by A17, A18;

        then

         A22: (h |^ k) in (F . i) by A19, GROUP_4: 4;

        

         A23: (f0 . i) in (F . i) by A16, GROUP_19: 5;

        ( 1_ (F . i)) is Element of G by A19, GROUP_2: 42;

        then

        reconsider f1 = (f0 +* (i,( 1_ (F . i)))) as finite-support Function of I, G by GROUP_19: 26;

        reconsider f = (f1 +* (i,((f0 . i) * (h |^ k)))) as finite-support Function of I, G by GROUP_19: 26;

        

         A27: ( dom f0) = I by FUNCT_2:def 1;

        

         A28: ( dom f1) = I by FUNCT_2:def 1;

        

         A29: f1 in ( product F) by A16, GROUP_19: 24;

        

         A30: (f . i) = ((f0 . i) * (h |^ k)) by A28, FUNCT_7: 31;

        take f;

        ((f0 . i) * (h |^ k)) in (F . i) by A19, A22, A23, GROUP_2: 50;

        hence

         A31: f in ( product F) by A29, GROUP_19: 24;

        (f1 . i) = ( 1_ (F . i)) by A27, FUNCT_7: 31;

        then f1 = (f +* (i,( 1_ (F . i)))) by Th7;

        

        then ( Product f) = (( Product f1) * ((f0 . i) * (h |^ k))) by A30, A31, Th8

        .= ((( Product f1) * (f0 . i)) * (h |^ k)) by GROUP_1:def 3

        .= (( Product f0) * (h |^ k)) by A16, Th8

        .= g by A7, A15, A16, GROUP_4: 6;

        hence thesis;

      end;

      for n be Nat holds P[n] from NAT_1:sch 2( A2, A5);

      hence thesis;

    end;

    theorem :: GROUP_20:12

    

     Th12: for I be non empty set, G be Group, F be Subgroup-Family of I, G, h,h0 be finite-support Function of I, G, i be Element of I, UFi be Subset of G st UFi = ( Union (( Carrier F) | (I \ {i}))) & h0 = (h +* (i,( 1_ (F . i)))) & h in ( product F) holds ( Product h0) in ( gr UFi)

    proof

      let I be non empty set, G be Group, F be Subgroup-Family of I, G, h,h0 be finite-support Function of I, G, i be Element of I, UFi be Subset of G;

      assume that

       A1: UFi = ( Union (( Carrier F) | (I \ {i}))) and

       A2: h0 = (h +* (i,( 1_ (F . i)))) and

       A3: h in ( product F);

      set CFi = (( Carrier F) | (I \ {i}));

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

      then

       A4: ( dom CFi) = (I \ {i}) by RELAT_1: 62;

      for y be object st y in ( rng h0) holds y in ( [#] ( gr UFi))

      proof

        let y be object;

        assume y in ( rng h0);

        then

        consider j be Element of I such that

         A5: y = (h0 . j) by FUNCT_2: 113;

        per cases ;

          suppose

           A6: j <> i;

          then not j in {i} by TARSKI:def 1;

          then

           A7: j in ( dom CFi) by A4, XBOOLE_0:def 5;

          

           A8: (h0 . j) = (h . j) by A2, A6, FUNCT_7: 32;

          (h . j) in (F . j) by A3, GROUP_19: 5;

          then (h . j) in ( [#] (F . j));

          then (h . j) in (( Carrier F) . j) by PENCIL_3: 7;

          then

           A9: (h0 . j) in (CFi . j) by A7, A8, FUNCT_1: 47;

          (CFi . j) c= ( union ( rng CFi)) by A7, FUNCT_1: 3, ZFMISC_1: 74;

          then

           A10: (CFi . j) c= UFi by A1, CARD_3:def 4;

          UFi c= ( [#] ( gr UFi)) by GROUP_4:def 4;

          hence thesis by A5, A9, A10;

        end;

          suppose

           A11: j = i;

          ( dom h) = I by A3, GROUP_19: 3;

          then

           A12: (h0 . j) = ( 1_ (F . j)) by A2, A11, FUNCT_7: 31;

          (F . j) is Subgroup of G by Def1;

          then ( 1_ (F . j)) = ( 1_ ( gr UFi)) by GROUP_2: 45;

          hence thesis by A5, A12;

        end;

      end;

      then ( rng h0) c= ( [#] ( gr UFi));

      then

      reconsider x0 = h0 as finite-support Function of I, ( gr UFi) by Th5;

      ( Product x0) = ( Product h0) by Th6;

      hence ( Product h0) in ( gr UFi);

    end;

    theorem :: GROUP_20:13

    

     Th13: for I be non empty set, G be Group, F be component-commutative Subgroup-Family of I, G, UF be Subset of G st UF = ( Union ( Carrier F)) holds for g be Element of G st g in ( gr UF) holds ex f be finite-support Function of I, ( gr UF) st f in ( sum F) & g = ( Product f)

    proof

      let I be non empty set, G be Group, F be component-commutative Subgroup-Family of I, G, UF be Subset of G;

      assume

       A1: UF = ( Union ( Carrier F));

      

       A2: for i be object st i in I holds (F . i) is Subgroup of G by Def1;

      let g be Element of G;

      assume g in ( gr UF);

      then

      consider H be FinSequence of G, K be FinSequence of INT such that

       A3: ( len H) = ( len K) & ( rng H) c= UF & ( Product (H |^ K)) = g by GROUP_4: 28;

      consider f be finite-support Function of I, G such that

       A4: f in ( product F) & g = ( Product f) by A1, A3, Th11;

      f is Function of I, ( Union ( Carrier F)) by A4, Th2;

      then

       A5: ( rng f) c= UF by A1, RELAT_1:def 19;

      UF c= ( [#] ( gr UF)) by GROUP_4:def 4;

      then ( rng f) c= ( [#] ( gr UF)) by A5;

      then

      reconsider f0 = f as finite-support Function of I, ( gr UF) by Th5;

      take f0;

      ( support (f,F)) = ( support f) by A2, A4, GROUP_19: 9;

      hence thesis by A4, GROUP_19: 8, Th6;

    end;

    theorem :: GROUP_20:14

    

     Th14: for I be non empty set, G be Group, F be component-commutative Subgroup-Family of I, G, UF be Subset of G st UF = ( Union ( Carrier F)) holds for i be Element of I holds (F . i) is normal Subgroup of ( gr UF)

    proof

      let I be non empty set, G be Group, F be component-commutative Subgroup-Family of I, G, UF be Subset of G;

      assume

       A1: UF = ( Union ( Carrier F));

      let i be Element of I;

      

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

      

       A3: (F . i) is Subgroup of G by Def1;

      (( Carrier F) . i) in ( rng ( Carrier F)) by A2, FUNCT_1: 3;

      then ( [#] (F . i)) in ( rng ( Carrier F)) by PENCIL_3: 7;

      then ( [#] (F . i)) c= ( union ( rng ( Carrier F))) by ZFMISC_1: 74;

      then

       A4: ( [#] (F . i)) c= UF by A1, CARD_3:def 4;

      UF c= ( [#] ( gr UF)) by GROUP_4:def 4;

      then ( [#] (F . i)) c= ( [#] ( gr UF)) by A4;

      then

      reconsider Fi = (F . i) as Subgroup of ( gr UF) by A3, GROUP_2: 57;

      for a be Element of ( gr UF) holds (a * Fi) c= (Fi * a)

      proof

        let a be Element of ( gr UF);

        for x be object st x in (a * Fi) holds x in (Fi * a)

        proof

          let x be object;

          assume x in (a * Fi);

          then

          consider g be Element of ( gr UF) such that

           A5: x = (a * g) & g in Fi by GROUP_2: 103;

          reconsider a1 = a as Element of G by GROUP_2: 42;

          a1 in ( gr UF);

          then

          consider h be finite-support Function of I, ( gr UF) such that

           A6: h in ( sum F) & a = ( Product h) by A1, Th13;

          reconsider m = (h . i) as Element of ( gr UF);

          

           A7: h in ( product F) by A6, GROUP_2: 40;

          

           A8: (h . i) in (F . i) by A6, GROUP_19: 5, GROUP_2: 40;

          reconsider I0 = (I \ {i}) as Subset of I;

          ( 1_ (F . i)) in ( gr UF) by A3, GROUP_2: 47;

          then

          reconsider h0 = (h +* (i,( 1_ (F . i)))) as finite-support Function of I, ( gr UF) by GROUP_19: 26;

          

           A9: h0 in ( product F) by A6, GROUP_19: 24, GROUP_2: 40;

          ( dom h) = I by FUNCT_2:def 1;

          then

           A10: (h0 . i) = ( 1_ (F . i)) by FUNCT_7: 31;

          

           A11: (a * g) = ((( Product h0) * m) * g) by A6, A7, Th9

          .= (( Product h0) * (m * g)) by GROUP_1:def 3;

          

           A12: (a * g) = ((m * g) * ( Product h0)) by A5, A8, A9, A10, A11, GROUP_2: 50, Th10

          .= (((m * g) * ( 1_ ( gr UF))) * ( Product h0)) by GROUP_1:def 4

          .= (((m * g) * ((m " ) * m)) * ( Product h0)) by GROUP_1:def 5

          .= ((((m * g) * (m " )) * m) * ( Product h0)) by GROUP_1:def 3

          .= (((m * g) * (m " )) * (m * ( Product h0))) by GROUP_1:def 3

          .= (((m * g) * (m " )) * (( Product h0) * m)) by A7, Th9

          .= (((m * g) * (m " )) * a) by A6, A7, Th9;

          (m " ) in Fi by A8, GROUP_2: 51;

          then (g * (m " )) in Fi by A5, GROUP_2: 50;

          then (m * (g * (m " ))) in Fi by A8, GROUP_2: 50;

          then ((m * g) * (m " )) in Fi by GROUP_1:def 3;

          hence thesis by A5, A12, GROUP_2: 104;

        end;

        hence thesis;

      end;

      hence thesis by GROUP_3: 118;

    end;

    theorem :: GROUP_20:15

    

     Th15: for I be non empty set, G be Group, F be component-commutative Subgroup-Family of I, G st for i be Element of I holds ex UFi be Subset of G st UFi = ( Union (( Carrier F) | (I \ {i}))) & (( [#] ( gr UFi)) /\ ( [#] (F . i))) = {( 1_ G)} holds for x1,x2 be finite-support Function of I, G st x1 in ( sum F) & x2 in ( sum F) & ( Product x1) = ( Product x2) holds x1 = x2

    proof

      let I be non empty set, G be Group, F be component-commutative Subgroup-Family of I, G;

      

       A1: for i be object st i in I holds (F . i) is Subgroup of G by Def1;

      assume

       A2: for i be Element of I holds ex UFi be Subset of G st UFi = ( Union (( Carrier F) | (I \ {i}))) & (( [#] ( gr UFi)) /\ ( [#] (F . i))) = {( 1_ G)};

      let x1,x2 be finite-support Function of I, G;

      assume that

       A3: x1 in ( sum F) & x2 in ( sum F) and

       A4: ( Product x1) = ( Product x2);

      defpred P[ Nat] means for x1,x2 be finite-support Function of I, G st ( card ( support x1)) = $1 & x1 in ( sum F) & x2 in ( sum F) & ( Product x1) = ( Product x2) holds x1 = x2;

      

       A5: P[ 0 ]

      proof

        let x1,x2 be finite-support Function of I, G;

        assume that

         A6: ( card ( support x1)) = 0 and

         A7: x1 in ( sum F) & x2 in ( sum F) and

         A8: ( Product x1) = ( Product x2);

        

         A9: ( support x1) = {} by A6;

        

         A10: ( Product x2) = ( 1_ G) by A8, A9, GROUP_19: 15;

        x2 = ( 1_ ( product F))

        proof

          assume x2 <> ( 1_ ( product F));

          then not ( support x2) is empty by A1, GROUP_19: 14;

          then

          consider i be object such that

           A11: i in ( support x2) by XBOOLE_0:def 1;

          

           A12: (x2 . i) <> ( 1_ G) & i in I by A11, GROUP_19:def 2;

          reconsider i as Element of I by A11;

          

           A13: (F . i) is Subgroup of G by Def1;

          then ( 1_ (F . i)) is Element of G by GROUP_2: 42;

          then

          reconsider y = (x2 +* (i,( 1_ (F . i)))) as finite-support Function of I, G by GROUP_19: 26;

          x2 in ( product F) by A7, GROUP_2: 41;

          then

           A14: ( Product x2) = (( Product y) * (x2 . i)) by Th8;

          consider UFi be Subset of G such that

           A15: UFi = ( Union (( Carrier F) | (I \ {i}))) and

           A16: (( [#] ( gr UFi)) /\ ( [#] (F . i))) = {( 1_ G)} by A2;

          

           A17: ( Product y) in ( gr UFi) by A7, A15, GROUP_2: 41, Th12;

          (x2 . i) in (F . i) by A7, GROUP_19: 5, GROUP_2: 41;

          then

           A18: ((x2 . i) " ) in (F . i) by A13, GROUP_2: 51;

          

           A19: ( Product y) = ((x2 . i) " ) by A10, A14, GROUP_1: 12;

          then ( Product y) in {( 1_ G)} by A16, A17, A18, XBOOLE_0:def 4;

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

          hence contradiction by A12, A19, GROUP_1: 10;

        end;

        hence thesis by A1, A9, GROUP_19: 14;

      end;

      

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

      proof

        let k be Nat;

        assume

         A21: P[k];

        let x1,x2 be finite-support Function of I, G;

        assume that

         A22: ( card ( support x1)) = (k + 1) and

         A23: x1 in ( sum F) & x2 in ( sum F) and

         A24: ( Product x1) = ( Product x2);

         not ( support x1) is empty by A22;

        then

        consider i be object such that

         A25: i in ( support x1) by XBOOLE_0:def 1;

        reconsider i as Element of I by A25;

        

         A26: (F . i) is Subgroup of G by Def1;

        then

         A27: ( 1_ (F . i)) is Element of G by GROUP_2: 42;

        reconsider y1 = (x1 +* (i,( 1_ (F . i)))) as finite-support Function of I, G by A27, GROUP_19: 26;

        reconsider y2 = (x2 +* (i,( 1_ (F . i)))) as finite-support Function of I, G by A27, GROUP_19: 26;

        consider UFi be Subset of G such that

         A28: UFi = ( Union (( Carrier F) | (I \ {i}))) and

         A29: (( [#] ( gr UFi)) /\ ( [#] (F . i))) = {( 1_ G)} by A2;

        ( 1_ (F . i)) = ( 1_ G) by A26, GROUP_2: 44;

        

        then

         A30: ( card ( support y1)) = (( card ( support x1)) - 1) by A25, GROUP_19: 30

        .= k by A22;

        

         A31: y1 in ( sum F) & y2 in ( sum F) by A23, GROUP_19: 25;

        

         A32: x1 in ( product F) & x2 in ( product F) by A23, GROUP_2: 41;

        

         A33: ( Product x1) = (( Product y1) * (x1 . i)) by A32, Th8;

        

         A34: ( Product y1) in ( gr UFi) & ( Product y2) in ( gr UFi) by A23, A28, GROUP_2: 41, Th12;

        

         A35: (x1 . i) in (F . i) & (x2 . i) in (F . i) by A23, GROUP_19: 5, GROUP_2: 41;

        ( Product y1) = ((( Product y2) * (x2 . i)) * ((x1 . i) " )) by A24, A32, A33, GROUP_1: 14, Th8;

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

        then

         A36: ((( Product y2) " ) * ( Product y1)) = ((x2 . i) * ((x1 . i) " )) by GROUP_1: 13;

        (( Product y2) " ) in ( gr UFi) by A34, GROUP_2: 51;

        then

         A37: ((( Product y2) " ) * ( Product y1)) in ( gr UFi) by A34, GROUP_2: 50;

        ((x1 . i) " ) in (F . i) by A26, A35, GROUP_2: 51;

        then

         A38: ((x2 . i) * ((x1 . i) " )) in (F . i) by A26, A35, GROUP_2: 50;

        ((( Product y2) " ) * ( Product y1)) in {( 1_ G)} by A29, A36, A37, A38, XBOOLE_0:def 4;

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

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

        then

         A39: y1 = y2 by A21, A30, A31, GROUP_1: 9;

        ((x2 . i) * ((x1 . i) " )) in {( 1_ G)} by A29, A36, A37, A38, XBOOLE_0:def 4;

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

        then ((x1 . i) " ) = ((x2 . i) " ) by GROUP_1: 12;

        then

         A40: (x1 . i) = (x2 . i) by GROUP_1: 9;

        x1 = (y1 +* (i,(x1 . i))) by Th7;

        hence thesis by A39, A40, Th7;

      end;

      

       A42: for k be Nat holds P[k] from NAT_1:sch 2( A5, A20);

      ( card ( support x1)) is Nat;

      hence thesis by A3, A4, A42;

    end;

    theorem :: GROUP_20:16

    for I be non empty set, G be strict Group, F be Group-Family of I holds F is internal DirectSumComponents of G, I iff (for i be Element of I holds (F . i) is normal Subgroup of G) & (ex UF be Subset of G st UF = ( Union ( Carrier F)) & ( gr UF) = G) & for i be Element of I holds ex UFi be Subset of G st UFi = ( Union (( Carrier F) | (I \ {i}))) & (( [#] ( gr UFi)) /\ ( [#] (F . i))) = {( 1_ G)}

    proof

      let I be non empty set, G be strict Group, F be Group-Family of I;

      

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

      

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

      hereby

        assume

         A3: F is internal DirectSumComponents of G, I;

        then

         A4: (for i be object st i in I holds (F . i) is Subgroup of G) & (for i,j be Element of I, gi,gj be Element of G st i <> j & gi in (F . i) & gj in (F . j) holds (gi * gj) = (gj * gi)) & (for y be Element of G holds ex x be finite-support Function of I, G st x in ( sum F) & y = ( Product x)) & (for x1,x2 be finite-support Function of I, G st x1 in ( sum F) & x2 in ( sum F) & ( Product x1) = ( Product x2) holds x1 = x2) by GROUP_19: 54;

        then

         A5: F is component-commutative Subgroup-Family of I, G by Def1, Def2;

        for x be object st x in ( Union ( Carrier F)) holds x in ( [#] G)

        proof

          let x be object;

          assume x in ( Union ( Carrier F));

          then x in ( union ( rng ( Carrier F))) by CARD_3:def 4;

          then

          consider Fi be set such that

           A6: x in Fi & Fi in ( rng ( Carrier F)) by TARSKI:def 4;

          consider i be object such that

           A7: i in I & Fi = (( Carrier F) . i) by A2, A6, FUNCT_1:def 3;

          reconsider i as Element of I by A7;

          

           A8: (( Carrier F) . i) = ( [#] (F . i)) by PENCIL_3: 7;

          (F . i) is Subgroup of G by A3, GROUP_19: 54;

          then ( [#] (F . i)) c= ( [#] G) by GROUP_2:def 5;

          hence thesis by A6, A7, A8;

        end;

        then ( Union ( Carrier F)) c= ( [#] G);

        then

        reconsider UF = ( Union ( Carrier F)) as Subset of G;

        

         A9: for g be Element of G holds g in ( gr UF)

        proof

          let g be Element of G;

          consider x be finite-support Function of I, G such that

           A10: x in ( sum F) & g = ( Product x) by A3, GROUP_19: 54;

          x is Function of I, ( Union ( Carrier F)) by A10, GROUP_2: 41, Th2;

          then

           A11: ( rng x) c= UF by RELAT_1:def 19;

          UF c= ( [#] ( gr UF)) by GROUP_4:def 4;

          then ( rng x) c= ( [#] ( gr UF)) by A11;

          then

          reconsider x0 = x as finite-support Function of I, ( gr UF) by Th5;

          reconsider fx = ((x0 | ( support x0)) * ( canFS ( support x0))) as FinSequence of ( gr UF) by FINSEQ_2: 32;

          ( Product fx) = ( Product x0) by GROUP_17:def 1

          .= g by A10, Th6;

          hence thesis;

        end;

        then

         A12: ( gr UF) = G by GROUP_2: 62;

        thus for i be Element of I holds (F . i) is normal Subgroup of G by A5, A12, Th14;

        thus ex UF be Subset of G st UF = ( Union ( Carrier F)) & ( gr UF) = G by A9, GROUP_2: 62;

        thus for i be Element of I holds ex UFi be Subset of G st UFi = ( Union (( Carrier F) | (I \ {i}))) & (( [#] ( gr UFi)) /\ ( [#] (F . i))) = {( 1_ G)}

        proof

          let i be Element of I;

          

           A13: for i be Element of I holds (F . i) is Subgroup of G by A3, GROUP_19: 54;

          per cases ;

            suppose (I \ {i}) = {} ;

            

            then

             A14: ( Union (( Carrier F) | (I \ {i}))) = ( Union (( Carrier F) | {} ))

            .= ( union ( rng {} )) by CARD_3:def 4

            .= {} by ZFMISC_1: 2;

            reconsider UFi = ( {} the carrier of G) as Subset of G;

            reconsider Fi = (F . i) as Subgroup of G by A3, GROUP_19: 54;

            ( gr UFi) = ( (1). G) by GROUP_4: 30;

            then

             A15: (( gr UFi) /\ Fi) = ( (1). G) by GROUP_2: 85;

            (( [#] ( gr UFi)) /\ ( [#] Fi)) = (( carr ( gr UFi)) /\ ( carr Fi))

            .= ( carr ( (1). G)) by A15, GROUP_2: 81

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

            hence thesis by A14;

          end;

            suppose

             A16: (I \ {i}) <> {} ;

            set CFi = (( Carrier F) | (I \ {i}));

            set UFi = ( Union CFi);

            for x be object st x in UFi holds x in ( [#] G)

            proof

              let x be object;

              assume x in UFi;

              then x in ( union ( rng CFi)) by CARD_3:def 4;

              then

              consider Fi be set such that

               A17: x in Fi & Fi in ( rng CFi) by TARSKI:def 4;

              

               A18: ( dom CFi) = (I \ {i}) by A2, RELAT_1: 62;

              consider j be object such that

               A19: j in (I \ {i}) & Fi = (CFi . j) by A17, A18, FUNCT_1:def 3;

              reconsider j as Element of I by A19;

              

               A20: (CFi . j) = (( Carrier F) . j) by A19, FUNCT_1: 49

              .= ( [#] (F . j)) by PENCIL_3: 7;

              (F . j) is Subgroup of G by A3, GROUP_19: 54;

              then ( [#] (F . j)) c= ( [#] G) by GROUP_2:def 5;

              hence thesis by A17, A19, A20;

            end;

            then

            reconsider UFi as Subset of G by TARSKI:def 3;

            take UFi;

            thus UFi = ( Union CFi);

            

             A21: ( 1_ G) in ( gr UFi) by GROUP_2: 46;

            (F . i) is Subgroup of G by A3, GROUP_19: 54;

            then ( 1_ G) in (F . i) by GROUP_2: 46;

            then ( 1_ G) in (( [#] ( gr UFi)) /\ ( [#] (F . i))) by A21, XBOOLE_0:def 4;

            then

             A22: {( 1_ G)} c= (( [#] ( gr UFi)) /\ ( [#] (F . i))) by ZFMISC_1: 31;

            for x be object st x in (( [#] ( gr UFi)) /\ ( [#] (F . i))) holds x in {( 1_ G)}

            proof

              let x be object;

              assume

               A23: x in (( [#] ( gr UFi)) /\ ( [#] (F . i)));

              then x in ( [#] ( gr UFi)) & x in ( [#] (F . i)) by XBOOLE_0:def 4;

              then

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

              set I0 = (I \ {i});

              set F0 = (F | I0);

              

               A24: ( dom F0) = I0 by A1, RELAT_1: 62;

              

               A25: for j be object st j in I0 holds (F0 . j) is Subgroup of G

              proof

                let j be object;

                assume

                 A26: j in I0;

                then

                 A27: (F . j) = (F0 . j) by FUNCT_1: 49;

                reconsider j as Element of I by A26;

                (F0 . j) is Subgroup of G by A3, A27, GROUP_19: 54;

                hence thesis;

              end;

              then for j be object st j in I0 holds (F0 . j) is Group;

              then

              reconsider F0 as Group-Family of I0 by A24, GROUP_19: 2;

              reconsider F0 as Subgroup-Family of I0, G by A25, Def1;

              

               A29: F0 is component-commutative

              proof

                let j,k be object, gj,gk be Element of G;

                assume

                 A28: j in I0 & k in I0 & j <> k;

                then

                reconsider Fj = (F0 . j), Fk = (F0 . k) as Subgroup of G by Def1;

                take Fj, Fk;

                thus Fj = (F0 . j) & Fk = (F0 . k);

                assume

                 A29: gj in Fj & gk in Fk;

                reconsider j, k as Element of I by A28;

                (F0 . j) = (F . j) & (F0 . k) = (F . k) by A28, FUNCT_1: 49;

                hence (gj * gk) = (gk * gj) by A3, A28, A29, GROUP_19: 54;

              end;

              

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

              for j be object st j in ( dom CFi) holds (CFi . j) = (( Carrier F0) . j)

              proof

                let j be object;

                assume

                 A31: j in ( dom CFi);

                then

                 A32: j in I0;

                then

                reconsider I0 as non empty set;

                reconsider F0 as Group-Family of I0;

                reconsider j0 = j as Element of I0 by A31;

                reconsider j as Element of I by A32;

                (CFi . j) = (( Carrier F) . j) by A31, FUNCT_1: 49

                .= ( [#] (F . j)) by PENCIL_3: 7

                .= ( [#] (F0 . j0)) by FUNCT_1: 49

                .= (( Carrier F0) . j) by PENCIL_3: 7;

                hence thesis;

              end;

              then

               A33: UFi = ( Union ( Carrier F0)) by A2, A30, FUNCT_1: 2, RELAT_1: 62;

              g in ( gr UFi) by A23, XBOOLE_0:def 4;

              then

              consider hi be finite-support Function of I0, ( gr UFi) such that

               A34: hi in ( sum F0) & g = ( Product hi) by A16, A29, A33, Th13;

              set h = (hi +* ( {i} --> ( 1_ G)));

              

               A35: ( rng h) c= (( rng hi) \/ ( rng ( {i} --> ( 1_ G)))) by FUNCT_4: 17;

              ( rng hi) c= ( [#] G) by GROUP_2:def 5, TARSKI:def 3;

              then (( rng hi) \/ ( rng ( {i} --> ( 1_ G)))) c= ( [#] G) by XBOOLE_1: 8;

              then

               A36: ( rng h) c= ( [#] G) by A35;

              

               A37: ( dom ( {i} --> ( 1_ G))) = {i};

              ( dom hi) = I0 by FUNCT_2:def 1;

              

              then

               A38: ( dom h) = (I0 \/ {i}) by A37, FUNCT_4:def 1

              .= I by XBOOLE_1: 45;

              then

              reconsider h as Function of I, G by A36, FUNCT_2: 2;

              

               A39: for j be object holds j in ( support h) iff j in ( support hi)

              proof

                let j be object;

                hereby

                  assume

                   A40: j in ( support h);

                  then

                   A41: j in I & (h . j) <> ( 1_ G) by GROUP_19:def 2;

                  

                   A42: i <> j

                  proof

                    assume

                     A43: j = i;

                    then

                     A44: j in {i} by TARSKI:def 1;

                    i in {i} by TARSKI:def 1;

                    then i in ( dom ( {i} --> ( 1_ G)));

                    

                    then (h . j) = (( {i} --> ( 1_ G)) . j) by A43, FUNCT_4: 13

                    .= ( 1_ G) by A44, FUNCOP_1: 7;

                    hence contradiction by A40, GROUP_19:def 2;

                  end;

                  then not j in {i} by TARSKI:def 1;

                  then

                   A45: j in I0 by A40, XBOOLE_0:def 5;

                   not j in ( dom ( {i} --> ( 1_ G))) by A42, TARSKI:def 1;

                  then (hi . j) <> ( 1_ G) by A41, FUNCT_4: 11;

                  then (hi . j) <> ( 1_ ( gr UFi)) by GROUP_2: 44;

                  hence j in ( support hi) by A45, GROUP_19:def 2;

                end;

                assume

                 A46: j in ( support hi);

                then

                 A47: j in I0 & (hi . j) <> ( 1_ ( gr UFi)) by GROUP_19:def 2;

                

                 A48: j in I & not j in {i} by A46, XBOOLE_0:def 5;

                 not j in ( dom ( {i} --> ( 1_ G))) by A46, XBOOLE_0:def 5;

                then (h . j) = (hi . j) by FUNCT_4: 11;

                then (h . j) <> ( 1_ G) by A47, GROUP_2: 44;

                hence j in ( support h) by A48, GROUP_19:def 2;

              end;

              then

               A49: ( support h) = ( support hi) by TARSKI: 2;

              then

              reconsider h as finite-support Function of I, G by GROUP_19:def 3;

              

               A50: ( support h) = ( dom (h | ( support h))) by PARTFUN1:def 2;

              

               A51: ( support hi) = ( dom (hi | ( support hi))) by PARTFUN1:def 2;

              for x be object st x in ( dom (h | ( support h))) holds ((h | ( support h)) . x) = ((hi | ( support hi)) . x)

              proof

                let x be object;

                assume

                 A52: x in ( dom (h | ( support h)));

                x in ( dom (hi | ( support hi))) by A39, A51, A52;

                then

                 A53: x in (( dom hi) /\ ( support hi)) by RELAT_1: 61;

                

                 A54: ( dom hi) = I0 & ( dom ( {i} --> ( 1_ G))) = {i} by FUNCT_2:def 1;

                

                thus ((h | ( support h)) . x) = (h . x) by A52, FUNCT_1: 47

                .= (hi . x) by A53, A54, FUNCT_4: 16, XBOOLE_1: 79

                .= ((hi | ( support hi)) . x) by A39, A51, A52, FUNCT_1: 47;

              end;

              then

               A55: (h | ( support h)) = (hi | ( support hi)) by A39, A50, A51, FUNCT_1: 2, TARSKI: 2;

              reconsider fh = ((h | ( support h)) * ( canFS ( support h))) as FinSequence of G by FINSEQ_2: 32;

              reconsider fhi = ((hi | ( support hi)) * ( canFS ( support hi))) as FinSequence of ( gr UFi) by FINSEQ_2: 32;

              

               A56: g = ( Product fhi) by A34, GROUP_17:def 1

              .= ( Product fh) by A49, A55, GROUP_19: 45

              .= ( Product h) by GROUP_17:def 1;

              

               A57: i in {i} by TARSKI:def 1;

              

               A58: ( dom ( {i} --> ( 1_ G))) = {i};

              

               A59: h in ( product F)

              proof

                for j be object st j in I holds (h . j) in (( Carrier F) . j)

                proof

                  let j be object;

                  assume j in I;

                  then

                  reconsider j as Element of I;

                  (h . j) in ( [#] (F . j))

                  proof

                    per cases ;

                      suppose i = j;

                      

                      then

                       A60: (h . j) = (( {i} --> ( 1_ G)) . i) by A57, A58, FUNCT_4: 13

                      .= ( 1_ G) by A57, FUNCOP_1: 7;

                      (F . j) is Subgroup of G by A3, GROUP_19: 54;

                      then ( 1_ G) in (F . j) by GROUP_2: 46;

                      hence thesis by A60;

                    end;

                      suppose

                       A61: i <> j;

                      then not j in {i} by TARSKI:def 1;

                      then

                       A62: j in I0 by XBOOLE_0:def 5;

                      

                       A63: not j in ( dom ( {i} --> ( 1_ G))) by A61, TARSKI:def 1;

                      

                       A64: (h . j) = (hi . j) by A63, FUNCT_4: 11;

                      reconsider I0 as non empty set by A62;

                      reconsider F0 as Group-Family of I0;

                      reconsider j0 = j as Element of I0 by A62;

                      (hi . j0) in (F0 . j0) by A34, GROUP_19: 5, GROUP_2: 40;

                      hence thesis by A64, FUNCT_1: 49;

                    end;

                  end;

                  hence thesis by PENCIL_3: 7;

                end;

                then h in ( product ( Carrier F)) by A2, A38, CARD_3:def 5;

                hence thesis by GROUP_7:def 2;

              end;

              

               A65: h in ( sum F)

              proof

                reconsider h0 = h as Element of ( product F) by A59;

                ( support h) = ( support (h0,F)) by A4, GROUP_19: 9;

                hence thesis by GROUP_19: 8;

              end;

              reconsider id1g = (I --> ( 1_ G)) as Function of I, G;

              ( support id1g) is empty by GROUP_19: 12;

              then

              reconsider id1g as finite-support Function of I, G by GROUP_19:def 3;

              

               A66: ( 1_ ( product F)) = id1g by A13, GROUP_19: 13;

              then

              reconsider k = (( 1_ ( product F)) +* (i,g)) as finite-support Function of I, G by GROUP_19: 26;

              

               A67: ( Product k) = g by A66, GROUP_19: 21;

              k in ( ProjSet (F,i)) by A23, GROUP_12:def 1;

              then k in ( ProjGroup (F,i)) by GROUP_12:def 2;

              then

               A68: k in ( sum F) by GROUP_2: 40;

              ( dom ( 1_ ( product F))) = I by GROUP_19: 3;

              

              then g = (k . i) by FUNCT_7: 31

              .= (h . i) by A3, A56, A65, A67, A68, GROUP_19: 54

              .= (( {i} --> ( 1_ G)) . i) by A57, A58, FUNCT_4: 13

              .= ( 1_ G) by A57, FUNCOP_1: 7;

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

            end;

            then (( [#] ( gr UFi)) /\ ( [#] (F . i))) c= {( 1_ G)};

            hence thesis by A22, XBOOLE_0:def 10;

          end;

        end;

      end;

      assume that

       A69: for i be Element of I holds (F . i) is normal Subgroup of G and

       A70: ex UF be Subset of G st UF = ( Union ( Carrier F)) & ( gr UF) = G and

       A71: for i be Element of I holds ex UFi be Subset of G st UFi = ( Union (( Carrier F) | (I \ {i}))) & (( [#] ( gr UFi)) /\ ( [#] (F . i))) = {( 1_ G)};

      consider UF be Subset of G such that

       A72: UF = ( Union ( Carrier F)) & ( gr UF) = G by A70;

      

       A73: for i be Element of I holds (F . i) is Subgroup of G by A69;

      

       A74: for i be object st i in I holds (F . i) is Subgroup of G by A69;

      

       A75: for i,j be Element of I st i <> j holds (( [#] (F . i)) /\ ( [#] (F . j))) = {( 1_ G)}

      proof

        let i,j be Element of I;

        assume

         A76: i <> j;

        (F . i) is Subgroup of G by A69;

        then ( 1_ G) in (F . i) by GROUP_2: 46;

        then

         A77: {( 1_ G)} c= ( [#] (F . i)) by ZFMISC_1: 31;

        (F . j) is Subgroup of G by A69;

        then ( 1_ G) in (F . j) by GROUP_2: 46;

        then {( 1_ G)} c= ( [#] (F . j)) by ZFMISC_1: 31;

        then

         A78: {( 1_ G)} c= (( [#] (F . i)) /\ ( [#] (F . j))) by A77, XBOOLE_1: 19;

        for x be object st x in (( [#] (F . i)) /\ ( [#] (F . j))) holds x in {( 1_ G)}

        proof

          let x be object;

          assume

           A79: x in (( [#] (F . i)) /\ ( [#] (F . j)));

          then

           A80: x in ( [#] (F . i)) & x in ( [#] (F . j)) by XBOOLE_0:def 4;

          consider UFj be Subset of G such that

           A81: UFj = ( Union (( Carrier F) | (I \ {j}))) & (( [#] ( gr UFj)) /\ ( [#] (F . j))) = {( 1_ G)} by A71;

          i in I & not i in {j} by A76, TARSKI:def 1;

          then

           A82: i in (I \ {j}) by XBOOLE_0:def 5;

          

           A83: i in ( dom (( Carrier F) | (I \ {j}))) by A2, A82, RELAT_1: 62;

          ((( Carrier F) | (I \ {j})) . i) = (( Carrier F) . i) by A82, FUNCT_1: 49

          .= ( [#] (F . i)) by PENCIL_3: 7;

          then ( [#] (F . i)) c= ( union ( rng (( Carrier F) | (I \ {j})))) by A83, FUNCT_1: 3, ZFMISC_1: 74;

          then

           A84: ( [#] (F . i)) c= UFj by A81, CARD_3:def 4;

          UFj c= ( [#] ( gr UFj)) by GROUP_4:def 4;

          then x in ( [#] ( gr UFj)) by A80, A84;

          hence thesis by A79, A81, XBOOLE_0:def 4;

        end;

        then (( [#] (F . i)) /\ ( [#] (F . j))) c= {( 1_ G)};

        hence thesis by A78, XBOOLE_0:def 10;

      end;

      

       A85: for i,j be Element of I, gi,gj be Element of G st i <> j & gi in (F . i) & gj in (F . j) holds (gi * gj) = (gj * gi)

      proof

        let i,j be Element of I, gi,gj be Element of G;

        assume

         A86: i <> j & gi in (F . i) & gj in (F . j);

        

         A87: (F . i) is normal Subgroup of G by A69;

        

         A88: (F . j) is normal Subgroup of G by A69;

        

         A89: (( [#] (F . i)) /\ ( [#] (F . j))) = {( 1_ G)} by A75, A86;

        set x = ((gi * gj) * ((gj * gi) " ));

        

         A90: (gi " ) in (F . i) by A86, A87, GROUP_2: 51;

        

         A91: (gj " ) in (F . j) by A86, A88, GROUP_2: 51;

        

         A92: ((gi * gj) * (gi " )) in (F . j) by A86, A88, Th1;

        

         A93: (gj * ((gi " ) * (gj " ))) in (F . i) by A87, A90, Th1;

        x = ((gi * gj) * ((gi " ) * (gj " ))) by GROUP_1: 17

        .= (((gi * gj) * (gi " )) * (gj " )) by GROUP_1:def 3;

        then

         A94: x in (F . j) by A88, A91, A92, GROUP_2: 50;

        x = ((gi * gj) * ((gi " ) * (gj " ))) by GROUP_1: 17

        .= (gi * (gj * ((gi " ) * (gj " )))) by GROUP_1:def 3;

        then x in (F . i) by A86, A87, A93, GROUP_2: 50;

        then x in (( [#] (F . i)) /\ ( [#] (F . j))) by A94, XBOOLE_0:def 4;

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

        then ((gi * gj) " ) = ((gj * gi) " ) by GROUP_1: 12;

        hence thesis by GROUP_1: 9;

      end;

      

       A95: F is component-commutative Subgroup-Family of I, G by A74, A85, Def1, Def2;

      

       A96: for y be Element of G holds ex x be finite-support Function of I, G st x in ( sum F) & y = ( Product x)

      proof

        let y be Element of G;

        y in ( gr UF) by A72;

        then

        consider x be finite-support Function of I, ( gr UF) such that

         A97: x in ( sum F) & y = ( Product x) by A72, A95, Th13;

        reconsider x as finite-support Function of I, G by A72;

        take x;

        thus thesis by A72, A97;

      end;

      for x1,x2 be finite-support Function of I, G st x1 in ( sum F) & x2 in ( sum F) & ( Product x1) = ( Product x2) holds x1 = x2 by A71, A95, Th15;

      hence F is internal DirectSumComponents of G, I by A73, A85, A96, GROUP_19: 54;

    end;

    begin

    theorem :: GROUP_20:17

    for I be non empty set, G be commutative Group, F be Group-Family of I holds F is internal DirectSumComponents of G, I iff (for i be Element of I holds (F . i) is Subgroup of G) & (for i,j be Element of I st i <> j holds (( [#] (F . i)) /\ ( [#] (F . j))) = {( 1_ G)}) & (for y be Element of G holds ex x be finite-support Function of I, G st x in ( sum F) & y = ( Product x)) & (for x1,x2 be finite-support Function of I, G st x1 in ( sum F) & x2 in ( sum F) & ( Product x1) = ( Product x2) holds x1 = x2)

    proof

      let I be non empty set, G be commutative Group, F be Group-Family of I;

      hereby

        assume

         A1: F is internal DirectSumComponents of G, I;

        then

         A2: (for i be Element of I holds (F . i) is Subgroup of G) & (for i,j be Element of I, gi,gj be Element of G st i <> j & gi in (F . i) & gj in (F . j) holds (gi * gj) = (gj * gi)) & (for y be Element of G holds ex x be finite-support Function of I, G st x in ( sum F) & y = ( Product x)) & (for x1,x2 be finite-support Function of I, G st x1 in ( sum F) & x2 in ( sum F) & ( Product x1) = ( Product x2) holds x1 = x2) by GROUP_19: 54;

        

         A3: for i be object st i in I holds (F . i) is Subgroup of G by A1, GROUP_19: 54;

        

         A4: for i,j be Element of I st i <> j holds (( [#] (F . i)) /\ ( [#] (F . j))) = {( 1_ G)}

        proof

          let i,j be Element of I;

          assume

           A5: i <> j;

          

           A6: (F . i) is Subgroup of G by A1, GROUP_19: 54;

          then

           A7: ( 1_ G) in (F . i) by GROUP_2: 46;

          

           A8: (F . j) is Subgroup of G by A1, GROUP_19: 54;

          then ( 1_ G) in (F . j) by GROUP_2: 46;

          then ( 1_ G) in (( [#] (F . j)) /\ ( [#] (F . i))) by A7, XBOOLE_0:def 4;

          then

           A9: {( 1_ G)} c= (( [#] (F . i)) /\ ( [#] (F . j))) by ZFMISC_1: 31;

          for x be object st x in (( [#] (F . i)) /\ ( [#] (F . j))) holds x in {( 1_ G)}

          proof

            let x be object;

            assume

             A10: x in (( [#] (F . i)) /\ ( [#] (F . j)));

            reconsider gi = x as Element of (F . i) by A10, XBOOLE_0:def 4;

            reconsider gj = x as Element of (F . j) by A10;

            gi in G by A6, GROUP_2: 41;

            then

            reconsider ggi = gi as Element of G;

            gj in G by A8, GROUP_2: 41;

            then

            reconsider ggj = gj as Element of G;

            x = ( 1_ G)

            proof

              assume

               A11: x <> ( 1_ G);

              set xi = (( 1_ ( product F)) +* (i,gi));

              set xj = (( 1_ ( product F)) +* (j,gj));

              

               A12: xi in ( sum F) by GROUP_19: 25, GROUP_2: 46;

              then

              reconsider xi as finite-support Function of I, G by A3, GROUP_19: 10;

              

               A13: xj in ( sum F) by GROUP_19: 25, GROUP_2: 46;

              then

              reconsider xj as finite-support Function of I, G by A3, GROUP_19: 10;

              

               A14: ( 1_ ( product F)) = (I --> ( 1_ G)) by A2, GROUP_19: 13;

              

              then ( Product xi) = ggj by GROUP_19: 21

              .= ( Product xj) by A14, GROUP_19: 21;

              then

               A15: xi = xj by A1, A12, A13, GROUP_19: 54;

              

               A16: ( dom ( 1_ ( product F))) = I by GROUP_19: 3;

              (xj . i) = (( 1_ ( product F)) . i) by A5, FUNCT_7: 32

              .= ( 1_ (F . i)) by GROUP_7: 6

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

              hence contradiction by A11, A15, A16, FUNCT_7: 31;

            end;

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

          end;

          then (( [#] (F . i)) /\ ( [#] (F . j))) c= {( 1_ G)};

          hence thesis by A9, XBOOLE_0:def 10;

        end;

        thus (for i be Element of I holds (F . i) is Subgroup of G) & (for i,j be Element of I st i <> j holds (( [#] (F . i)) /\ ( [#] (F . j))) = {( 1_ G)}) & (for y be Element of G holds ex x be finite-support Function of I, G st x in ( sum F) & y = ( Product x)) & (for x1,x2 be finite-support Function of I, G st x1 in ( sum F) & x2 in ( sum F) & ( Product x1) = ( Product x2) holds x1 = x2) by A1, A4, GROUP_19: 54;

      end;

      assume

       A17: (for i be Element of I holds (F . i) is Subgroup of G) & (for i,j be Element of I st i <> j holds (( [#] (F . i)) /\ ( [#] (F . j))) = {( 1_ G)}) & (for y be Element of G holds ex x be finite-support Function of I, G st x in ( sum F) & y = ( Product x)) & (for x1,x2 be finite-support Function of I, G st x1 in ( sum F) & x2 in ( sum F) & ( Product x1) = ( Product x2) holds x1 = x2);

      for i,j be Element of I, gi,gj be Element of G st i <> j & gi in (F . i) & gj in (F . j) holds (gi * gj) = (gj * gi);

      hence F is internal DirectSumComponents of G, I by A17, GROUP_19: 54;

    end;

    begin

    theorem :: GROUP_20:18

    

     Th19: for I be non empty set, G be Group, F be Subgroup-Family of I, G, h be Homomorphism of ( sum F), G, a be finite-support Function of I, G st a in ( sum F) & for i be Element of I, x be Element of (F . i) holds (h . (( 1ProdHom (F,i)) . x)) = x holds (h . a) = ( Product a)

    proof

      let I be non empty set, G be Group, F be Subgroup-Family of I, G, h be Homomorphism of ( sum F), G, a be finite-support Function of I, G;

      assume that

       A1: a in ( sum F) and

       A2: for i be Element of I, x be Element of (F . i) holds (h . (( 1ProdHom (F,i)) . x)) = x;

      

       A3: for i be object st i in I holds (F . i) is Subgroup of G by Def1;

      defpred P[ Nat] means for b be finite-support Function of I, G st b in ( sum F) holds ( card ( support b)) = $1 implies (h . b) = ( Product b);

      

       A4: P[ 0 ]

      proof

        let b be finite-support Function of I, G;

        assume b in ( sum F);

        assume ( card ( support b)) = 0 ;

        then

         A5: ( support b) = {} ;

        

        then b = ( 1_ ( product F)) by A3, GROUP_19: 14

        .= ( 1_ ( sum F)) by GROUP_2: 44;

        then (h . b) = ( 1_ G) by GROUP_6: 31;

        hence thesis by A5, GROUP_19: 15;

      end;

      

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

      proof

        let k be Nat;

        assume

         A7: P[k];

        let b be finite-support Function of I, G;

        assume

         A8: b in ( sum F);

        assume

         A9: ( card ( support b)) = (k + 1);

        then not ( support b) is empty;

        then

        consider i be object such that

         A10: i in ( support b) by XBOOLE_0:def 1;

        

         A11: (b . i) <> ( 1_ G) & i in I by A10, GROUP_19:def 2;

        reconsider i as Element of I by A10;

        set c = (b +* (i,( 1_ (F . i))));

        c in ( sum F) by A8, GROUP_19: 25;

        then

        reconsider c as Element of ( sum F);

        (F . i) is Subgroup of G by Def1;

        then

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

        then

        reconsider c0 = c as finite-support Function of I, G by GROUP_19: 26;

        

         A13: b in ( product F) by A8, GROUP_2: 40;

        

         A14: (b . i) in (F . i) by A8, GROUP_19: 5, GROUP_2: 40;

        then (( 1ProdHom (F,i)) . (b . i)) in ( ProjGroup (F,i)) by FUNCT_2: 5;

        then (( 1ProdHom (F,i)) . (b . i)) in ( sum F) by GROUP_2: 40;

        then

        reconsider d = (( 1ProdHom (F,i)) . (b . i)) as Element of ( sum F);

        

         A15: d = (( 1_ ( product F)) +* (i,(b . i))) by A14, GROUP_12:def 3;

        

         A16: d is Element of ( product F) by GROUP_2: 42;

        

         A17: ( support (d,F)) = {i} by A11, A12, A14, A15, A16, GROUP_19: 18;

        

         A18: i in ( dom b) by A11, A13, GROUP_19: 3;

        

         A19: b = (c * d)

        proof

          reconsider c1 = c, d1 = d as Element of ( product F) by GROUP_2: 42;

          

           A20: ( support (c1,F)) misses ( support (d1,F))

          proof

            (c . i) = ( 1_ (F . i)) by A18, FUNCT_7: 31;

            then not ex G be Group st G = (F . i) & (c . i) <> ( 1_ G) & i in I;

            then not i in ( support (c,F)) by GROUP_19:def 1;

            hence thesis by A17, ZFMISC_1: 50;

          end;

          

           A21: ( dom (i .--> (b . i))) = {i};

          

           A22: ( dom ( 1_ ( product F))) = I by GROUP_19: 3;

          

           A23: (d1 | ( support (d1,F))) = ((( 1_ ( product F)) +* (i,(b . i))) | {i}) by A11, A12, A14, A15, GROUP_19: 18

          .= ((( 1_ ( product F)) +* (i .--> (b . i))) | {i}) by A22, FUNCT_7:def 3

          .= (i .--> (b . i)) by A21, FUNCT_4: 23;

          

           A24: i in ( dom c) by A18, FUNCT_7: 30;

          

          thus b = (c1 +* (i,(b . i))) by Th7

          .= (c1 +* (d1 | ( support (d1,F)))) by A23, A24, FUNCT_7:def 3

          .= (c1 * d1) by A20, GROUP_19: 31

          .= (c * d) by GROUP_2: 43;

        end;

        

         A25: (h . c0) = ( Product c0)

        proof

          

           A26: c0 in ( sum F);

          ( card ( support c0)) = (( card ( support b)) - 1) by A10, A12, GROUP_19: 30

          .= k by A9;

          hence thesis by A7, A26;

        end;

        for i,j be Element of I, gi,gj be Element of G st i <> j & gi in (F . i) & gj in (F . j) holds (gi * gj) = (gj * gi)

        proof

          let i,j be Element of I;

          let gi,gj be Element of G;

          assume that

           A27: i <> j and

           A28: gi in (F . i) and

           A29: gj in (F . j);

          set ai = (( 1ProdHom (F,i)) . gi);

          

           A30: ai in ( ProjGroup (F,i)) by A28, FUNCT_2: 5;

          then ai in ( sum F) by GROUP_2: 40;

          then

          reconsider ai as Element of ( sum F);

          reconsider bi = ai as Element of ( product F) by GROUP_2: 42;

          set aj = (( 1ProdHom (F,j)) . gj);

          

           A31: aj in ( ProjGroup (F,j)) by A29, FUNCT_2: 5;

          then aj in ( sum F) by GROUP_2: 40;

          then

          reconsider aj as Element of ( sum F);

          reconsider bj = aj as Element of ( product F) by GROUP_2: 42;

          

           A32: gi = (h . ai) by A2, A28;

          (gi * gj) = ((h . ai) * (h . aj)) by A2, A29, A32

          .= (h . (ai * aj)) by GROUP_6:def 6

          .= (h . (bi * bj)) by GROUP_2: 43

          .= (h . (bj * bi)) by A27, A30, A31, GROUP_12: 7

          .= (h . (aj * ai)) by GROUP_2: 43

          .= ((h . aj) * (h . ai)) by GROUP_6:def 6

          .= (gj * gi) by A2, A29, A32;

          hence thesis;

        end;

        then

         A33: F is component-commutative;

        

         A34: b in ( product F) by A8, GROUP_2: 40;

        (h . b) = ((h . c) * (h . d)) by A19, GROUP_6:def 6

        .= (( Product c0) * (b . i)) by A2, A14, A25

        .= ( Product b) by A33, A34, Th8;

        hence thesis;

      end;

      

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

      consider k be Nat such that

       A36: ( card ( support a)) = k;

      thus thesis by A1, A35, A36;

    end;

    theorem :: GROUP_20:19

    for I be non empty set, G be Group, M be DirectSumComponents of G, I holds ex f be Homomorphism of ( sum M), G, N be internal DirectSumComponents of G, I st f is bijective & for i be Element of I holds ex qi be Homomorphism of (M . i), (N . i) st qi = (f * ( 1ProdHom (M,i))) & qi is bijective

    proof

      let I be non empty set;

      let G be Group;

      let M be DirectSumComponents of G, I;

      consider f be Homomorphism of ( sum M), G such that

       A1: f is bijective by GROUP_19:def 8;

      deffunc FN( Element of I) = (f .: ( ProjGroup (M,$1)));

      consider N be Function such that

       A2: ( dom N) = I and

       A3: for i be Element of I st i in I holds (N . i) = FN(i) from CLASSES1:sch 2;

      

       A4: for i be object st i in I holds (N . i) is strict Subgroup of G

      proof

        let i be object;

        assume i in I;

        then

        reconsider i as Element of I;

        (N . i) = (f .: ( ProjGroup (M,i))) by A3;

        hence thesis;

      end;

      then for i be object st i in I holds (N . i) is Group;

      then

      reconsider N as Group-Family of I by A2, GROUP_19: 2;

      for i be object st i in I holds (N . i) is Subgroup of G by A4;

      then

      reconsider N as Subgroup-Family of I, G by Def1;

      

       A5: for i be Element of I holds (N . i) is Subgroup of G by A4;

      deffunc FQ( Element of I) = (f * ( 1ProdHom (M,$1)));

      consider q be Function such that

       A6: ( dom q) = I and

       A7: for i be Element of I st i in I holds (q . i) = FQ(i) from CLASSES1:sch 2;

      reconsider q as non empty Function by A6;

       A8:

      now

        let i be Element of I;

        

         A9: ( rng ( 1ProdHom (M,i))) = ( [#] ( ProjGroup (M,i))) by FUNCT_2:def 3;

        reconsider fi = (f | ( ProjGroup (M,i))) as Homomorphism of ( ProjGroup (M,i)), G;

        ( dom fi) = ( [#] ( ProjGroup (M,i))) by FUNCT_2:def 1;

        then

         A10: (f * ( 1ProdHom (M,i))) = (fi * ( 1ProdHom (M,i))) by A9, RELAT_1: 165;

        

         A11: ( rng fi) = (f .: ( [#] ( ProjGroup (M,i)))) by RELAT_1: 115

        .= ( [#] (f .: ( ProjGroup (M,i)))) by GRSOLV_1: 8

        .= ( [#] (N . i)) by A3;

        ( Image fi) = (f .: ( ProjGroup (M,i)))

        .= (N . i) by A3;

        then

        reconsider fi as Homomorphism of ( ProjGroup (M,i)), (N . i) by GROUP_6: 49;

        

         A12: fi is one-to-one by A1, FUNCT_1: 52;

        

         A13: fi is onto by A11, FUNCT_2:def 3;

        reconsider qi = (fi * ( 1ProdHom (M,i))) as Homomorphism of (M . i), (N . i);

        take qi;

        thus qi = (q . i) by A7, A10;

        thus qi is bijective by A12, A13, GROUP_6: 64;

      end;

      then

       A14: for i be Element of I holds ex qi be Homomorphism of (M . i), (N . i) st qi = (q . i) & qi is bijective;

      reconsider r = ( SumMap (M,N,q)) as Homomorphism of ( sum M), ( sum N);

      

       A15: r is bijective by A6, A14, GROUP_19: 41;

      reconsider s = (r " ) as Homomorphism of ( sum N), ( sum M) by A6, A14, GROUP_19: 41, GROUP_6: 62;

      

       A16: s is bijective by A15, GROUP_6: 63;

      reconsider g = (f * s) as Function;

      reconsider g as Homomorphism of ( sum N), G;

      

       A17: g is bijective by A1, A16, GROUP_6: 64;

      then

      reconsider N as DirectSumComponents of G, I by GROUP_19:def 8;

      for i be Element of I, n be Element of (N . i) holds (g . (( 1ProdHom (N,i)) . n)) = n

      proof

        let i be Element of I;

        let n be Element of (N . i);

        consider qi be Homomorphism of (M . i), (N . i) such that

         A18: qi = (q . i) and

         A19: qi is bijective by A8;

        

         A20: ( dom qi) = ( [#] (M . i)) by FUNCT_2:def 1;

        ( rng qi) = ( [#] (N . i)) by A19, FUNCT_2:def 3;

        then

        consider m be object such that

         A21: m in ( [#] (M . i)) and

         A22: (qi . m) = n by A20, FUNCT_1:def 3;

        reconsider m as Element of (M . i) by A21;

        for i be Element of I holds (q . i) is Homomorphism of (M . i), (N . i)

        proof

          let i be Element of I;

          ex qi be Homomorphism of (M . i), (N . i) st qi = (q . i) & qi is bijective by A8;

          hence thesis;

        end;

        then

         A24: (r . (( 1ProdHom (M,i)) . m)) = (( 1ProdHom (N,i)) . n) by A6, A18, A22, GROUP_19: 42;

        

         A25: ( dom r) = ( [#] ( sum M)) by FUNCT_2:def 1;

        (( 1ProdHom (M,i)) . m) in ( ProjGroup (M,i));

        then

         A26: (( 1ProdHom (M,i)) . m) in ( sum M) by GROUP_2: 40;

        

         A27: ( dom s) = ( [#] ( sum N)) by FUNCT_2:def 1;

        (( 1ProdHom (N,i)) . n) in ( ProjGroup (N,i));

        then

         A28: (( 1ProdHom (N,i)) . n) in ( sum N) by GROUP_2: 40;

        

         A29: qi = (f * ( 1ProdHom (M,i))) by A7, A18;

        

         A30: m in ( dom ( 1ProdHom (M,i))) by A21, FUNCT_2:def 1;

        (g . (( 1ProdHom (N,i)) . n)) = (f . (s . (( 1ProdHom (N,i)) . n))) by A27, A28, FUNCT_1: 13

        .= (f . (( 1ProdHom (M,i)) . m)) by A15, A24, A25, A26, FUNCT_1: 34

        .= n by A22, A29, A30, FUNCT_1: 13;

        hence thesis;

      end;

      then for a be finite-support Function of I, G st a in ( sum N) holds (g . a) = ( Product a) by Th19;

      then

      reconsider N as internal DirectSumComponents of G, I by A5, A17, GROUP_19:def 9;

      take f, N;

      for i be Element of I holds ex qi be Homomorphism of (M . i), (N . i) st qi = (f * ( 1ProdHom (M,i))) & qi is bijective

      proof

        let i be Element of I;

        consider qi be Homomorphism of (M . i), (N . i) such that

         A31: qi = (q . i) and

         A32: qi is bijective by A8;

        take qi;

        thus thesis by A7, A31, A32;

      end;

      hence thesis by A1;

    end;