group_21.miz



    begin

    definition

      let I,J be non empty set, a be Function of I, J, F be multMagma-Family of J;

      :: original: *

      redefine

      func F * a -> multMagma-Family of I ;

      correctness

      proof

        reconsider E = (F * a) as ManySortedSet of I;

        

         A1: ( dom a) = I by FUNCT_2:def 1;

        

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

        now

          let x be set;

          assume x in ( rng E);

          then

          consider i be object such that

           A3: i in I and

           A4: (E . i) = x by A2, FUNCT_1:def 3;

          reconsider j = (a . i) as Element of J by A3, FUNCT_2: 5;

          (F . j) is non empty multMagma;

          hence x is non empty multMagma by A1, A3, A4, FUNCT_1: 13;

        end;

        hence thesis by GROUP_7:def 1;

      end;

    end

    definition

      let I,J be non empty set, a be Function of I, J, F be Group-Family of J;

      :: original: *

      redefine

      func F * a -> Group-Family of I ;

      correctness

      proof

        reconsider E = (F * a) as ManySortedSet of I;

        

         A1: ( dom a) = I by FUNCT_2:def 1;

        

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

        now

          let i be object;

          assume i in I;

          then

          reconsider i1 = i as Element of I;

          (E . i1) = (F . (a . i1)) by A1, FUNCT_1: 13;

          hence (E . i) is Group;

        end;

        hence thesis by A2, GROUP_19: 2;

      end;

    end

    definition

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

      :: GROUP_21:def1

      func F * a -> Subgroup-Family of I, G equals (F * a);

      correctness

      proof

        now

          let i be object;

          assume

           A1: i in I;

          then

          reconsider j = (a . i) as Element of J by FUNCT_2: 5;

          

           A2: (F . j) is Subgroup of G by GROUP_20:def 1;

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

          hence ((F * a) . i) is Subgroup of G by A1, A2, FUNCT_1: 13;

        end;

        hence thesis by GROUP_20:def 1;

      end;

    end

    scheme :: GROUP_21:sch1

    Sch1 { A() -> set , B() -> 1-sorted , F( Element of B()) -> set } :

ex f be Function st ( dom f) = A() & for x be Element of B() st x in A() holds (f . x) = F(x);

      defpred P[ object, object] means ($1 is Element of B() implies ex x be Element of B() st x = $1 & $2 = F(x)) & ( not $1 is Element of B() implies $2 = 0 );

      

       A1: for x be object st x in A() holds ex y be object st P[x, y]

      proof

        let x be object;

        assume x in A();

        per cases ;

          suppose x is Element of B();

          then

          reconsider z = x as Element of B();

          take F(z);

          thus thesis;

        end;

          suppose not x is Element of B();

          hence thesis;

        end;

      end;

      consider f be Function such that

       A2: ( dom f) = A() and

       A3: for x be object st x in A() holds P[x, (f . x)] from CLASSES1:sch 1( A1);

      take f;

      thus ( dom f) = A() by A2;

      let x be Element of B();

      assume x in A();

      then P[x, (f . x)] by A3;

      hence (f . x) = F(x);

    end;

    registration

      let I be set;

      cluster non-empty disjoint_valued for ManySortedSet of I;

      correctness

      proof

        deffunc DF( object) = {$1};

        consider f be Function such that

         A1: ( dom f) = I & for i be set st i in I holds (f . i) = DF(i) from FUNCT_1:sch 5;

        reconsider f as ManySortedSet of I by A1, PARTFUN1:def 2, RELAT_1:def 18;

        take f;

         not {} in ( rng f)

        proof

          assume {} in ( rng f);

          then

          consider x be object such that

           A2: x in ( dom f) & {} = (f . x) by FUNCT_1:def 3;

           {} = {x} by A1, A2;

          hence contradiction;

        end;

        hence f is non-empty;

        for x,y be object st x <> y holds (f . x) misses (f . y)

        proof

          let x,y be object;

          assume

           A3: x <> y;

          per cases ;

            suppose not x in ( dom f) or not y in ( dom f);

            then (f . x) = {} or (f . y) = {} by FUNCT_1:def 2;

            then ((f . x) /\ (f . y)) = {} ;

            hence (f . x) misses (f . y) by XBOOLE_0:def 7;

          end;

            suppose x in ( dom f) & y in ( dom f);

            then

             A4: (f . x) = {x} & (f . y) = {y} by A1;

            ( {x} /\ {y}) = {}

            proof

              assume ( {x} /\ {y}) <> {} ;

              then

              consider z be object such that

               A5: z in ( {x} /\ {y}) by XBOOLE_0:def 1;

              z in {x} & z in {y} by A5, XBOOLE_0:def 4;

              then z = x & z = y by TARSKI:def 1;

              hence contradiction by A3;

            end;

            hence (f . x) misses (f . y) by A4, XBOOLE_0:def 7;

          end;

        end;

        hence f is disjoint_valued;

      end;

    end

    theorem :: GROUP_21:1

    

     Th30: for f be non-empty disjoint_valued Function st ( Union f) is finite holds ( dom f) is finite

    proof

      let f be non-empty disjoint_valued Function;

      assume ( Union f) is finite;

      then

       A1: ( rng f) is finite & for X be set st X in ( rng f) holds X is finite by FINSET_1: 7;

      for x,y be object st x in ( dom f) & y in ( dom f) & (f . x) = (f . y) holds x = y

      proof

        let x,y be object;

        assume

         A2: x in ( dom f) & y in ( dom f) & (f . x) = (f . y);

        assume x <> y;

        then

         A3: ((f . x) /\ (f . y)) = {} by PROB_2:def 2, XBOOLE_0:def 7;

        (f . x) in ( rng f) by A2, FUNCT_1: 3;

        then

        consider i be object such that

         A4: i in (f . x) by XBOOLE_0:def 1;

        thus contradiction by A2, A3, A4;

      end;

      then f is one-to-one;

      hence ( dom f) is finite by A1, CARD_1: 59;

    end;

    theorem :: GROUP_21:2

    

     Th35: for X,Y be non empty set, X0,Y0 be set, f be Function of X, Y st f is bijective & ( rng (f | X0)) = Y0 holds ((f | X0) " ) = ((f " ) | Y0)

    proof

      let X,Y be non empty set, X0,Y0 be set, f be Function of X, Y;

      assume that

       A1: f is bijective and

       A2: ( rng (f | X0)) = Y0;

      

       A3: ( rng f) = ( dom (f " )) & ( dom f) = ( rng (f " )) by A1, FUNCT_1: 33;

      

       A4: ( rng f) = Y & Y = ( dom (f " )) by A1, A3, FUNCT_2:def 3;

      

       A5: ( dom ((f " ) | Y0)) = Y0 by A2, A4, RELAT_1: 62;

      

       A6: (f | X0) is one-to-one by A1, FUNCT_1: 52;

      then

       A7: ( rng (f | X0)) = ( dom ((f | X0) " )) & ( dom (f | X0)) = ( rng ((f | X0) " )) by FUNCT_1: 33;

      

       A8: ( dom ((f | X0) " )) = Y0 by A2, A6, FUNCT_1: 33;

      for x be object st x in ( dom ((f " ) | Y0)) holds (((f " ) | Y0) . x) = (((f | X0) " ) . x)

      proof

        let x be object;

        assume x in ( dom ((f " ) | Y0));

        then

         A9: x in Y0 by A2, A4, RELAT_1: 62;

        then

         A10: (((f " ) | Y0) . x) = ((f " ) . x) by FUNCT_1: 49;

        

         A11: x in ( dom ((f | X0) " )) by A2, A6, A9, FUNCT_1: 33;

        

         A12: (f | X0) c= f by RELAT_1: 59;

        for z be object st z in ((f | X0) " ) holds z in (f " )

        proof

          let z be object;

          assume

           A13: z in ((f | X0) " );

          then

          consider x,y be object such that

           A14: z = [x, y] by RELAT_1:def 1;

          

           A15: x in ( dom ((f | X0) " )) & y = (((f | X0) " ) . x) by A13, A14, FUNCT_1: 1;

          

           A16: x = ((f | X0) . y) by A6, A7, A15, FUNCT_1: 32;

          y in ( rng ((f | X0) " )) by A13, A14, XTUPLE_0:def 13;

          then

           A17: [y, x] in f by A7, A12, A16, FUNCT_1: 1;

          then

           A18: y in ( dom f) & x = (f . y) by FUNCT_1: 1;

          x in ( rng f) by A17, XTUPLE_0:def 13;

          then x in ( dom (f " )) & y = ((f " ) . x) by A1, A18, FUNCT_1: 32;

          hence thesis by A14, FUNCT_1: 1;

        end;

        then [x, (((f | X0) " ) . x)] in (f " ) by A11, FUNCT_1: 1;

        hence thesis by A10, FUNCT_1: 1;

      end;

      hence thesis by A5, A8;

    end;

    begin

    theorem :: GROUP_21:3

    

     Th1: for I,J be non empty set, a be Function of I, J, F be multMagma-Family of J, x be Element of ( product F) holds (x * a) in ( product (F * a))

    proof

      let I,J be non empty set, a be Function of I, J, F be multMagma-Family of J, x be Element of ( product F);

      ( dom x) = J by GROUP_19: 3;

      then ( rng a) c= ( dom x);

      then ( dom (x * a)) = ( dom a) by RELAT_1: 27;

      then ( dom (x * a)) = I by PARTFUN1:def 2;

      then

      reconsider y = (x * a) as ManySortedSet of I by PARTFUN1:def 2;

      reconsider z = ( Carrier (F * a)) as ManySortedSet of I;

      

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

      

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

      

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

      for i be object st i in I holds (y . i) in (z . i)

      proof

        let i be object;

        assume i in I;

        then

        reconsider i as Element of I;

        reconsider j = (a . i) as Element of J;

        

         A4: (z . i) = ( [#] ((F * a) . i)) by PENCIL_3: 7

        .= ( [#] (F . j)) by A3, FUNCT_1: 13;

        x in ( product F);

        then (x . j) in (F . j) by GROUP_19: 5;

        hence thesis by A3, A4, FUNCT_1: 13;

      end;

      then y in ( product z) by A1, A2, CARD_3:def 5;

      hence thesis by GROUP_7:def 2;

    end;

    definition

      let I,J be non empty set;

      let a be Function of I, J;

      let F be multMagma-Family of J;

      :: GROUP_21:def2

      func trans_prod (F,a) -> Function of ( product F), ( product (F * a)) means

      : Def2: for x be Element of ( product F) holds (it . x) = (x * a);

      existence

      proof

        deffunc DF( Element of ( product F)) = ($1 * a);

        consider f be Function such that

         A1: ( dom f) = ( [#] ( product F)) and

         A2: for x be Element of ( product F) st x in ( [#] ( product F)) holds (f . x) = DF(x) from Sch1;

        now

          let y be object;

          assume y in ( rng f);

          then

          consider x be object such that

           A3: x in ( dom f) and

           A4: (f . x) = y by FUNCT_1:def 3;

          reconsider x as Element of ( product F) by A1, A3;

          (x * a) in ( product (F * a)) by Th1;

          hence y in ( [#] ( product (F * a))) by A2, A4;

        end;

        then ( rng f) c= ( [#] ( product (F * a)));

        then

        reconsider f as Function of ( product F), ( product (F * a)) by A1, FUNCT_2: 2;

        take f;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let f0,f1 be Function of ( product F), ( product (F * a));

        assume

         A5: for x be Element of ( product F) holds (f0 . x) = (x * a);

        assume

         A6: for x be Element of ( product F) holds (f1 . x) = (x * a);

        

         A7: ( dom f1) = ( [#] ( product F)) by PARTFUN1:def 2;

        for x be object st x in ( dom f0) holds (f0 . x) = (f1 . x)

        proof

          let x be object;

          assume x in ( dom f0);

          then

          reconsider x as Element of ( product F);

          (f0 . x) = (x * a) by A5

          .= (f1 . x) by A6;

          hence thesis;

        end;

        hence f0 = f1 by A7, PARTFUN1:def 2;

      end;

    end

    theorem :: GROUP_21:4

    

     Th2: for I,J be non empty set, a be Function of I, J, F be multMagma-Family of J holds ( trans_prod (F,a)) is multiplicative

    proof

      let I,J be non empty set, a be Function of I, J, F be multMagma-Family of J;

      reconsider f = ( trans_prod (F,a)) as Function of ( product F), ( product (F * a));

      for x,y be Element of ( product F) holds (f . (x * y)) = ((f . x) * (f . y))

      proof

        let x,y be Element of ( product F);

        

         A1: (f . (x * y)) = ((x * y) * a) by Def2;

        

         A2: (f . x) = (x * a) by Def2;

        (x * a) in ( product (F * a)) by Th1;

        then

        reconsider xa = (x * a) as Element of ( product (F * a));

        (y * a) in ( product (F * a)) by Th1;

        then

        reconsider ya = (y * a) as Element of ( product (F * a));

        

         A3: ( dom (xa * ya)) = I by GROUP_19: 3;

        

         A4: ( dom a) = I by FUNCT_2:def 1;

        ( dom (x * y)) = J by GROUP_19: 3;

        then

         A5: ( rng a) c= ( dom (x * y));

        for i be object st i in I holds ((xa * ya) . i) = (((x * y) * a) . i)

        proof

          let i be object;

          assume i in I;

          then

          reconsider i as Element of I;

          reconsider Fai = ((F * a) . i) as multMagma;

          reconsider j = (a . i) as Element of J;

          reconsider Fj = (F . j) as multMagma;

          xa in ( product (F * a));

          then (xa . i) in ((F * a) . i) by GROUP_19: 5;

          then

          reconsider xai = (xa . i) as Element of Fai;

          ya in ( product (F * a));

          then (ya . i) in ((F * a) . i) by GROUP_19: 5;

          then

          reconsider yai = (ya . i) as Element of Fai;

          x in ( product F);

          then (x . j) in (F . j) by GROUP_19: 5;

          then

          reconsider xj = (x . j) as Element of Fj;

          y in ( product F);

          then (y . j) in (F . j) by GROUP_19: 5;

          then

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

          

           A6: (xa . i) = (x . j) by A4, FUNCT_1: 13;

          

           A7: (ya . i) = (y . j) by A4, FUNCT_1: 13;

          (((x * y) * a) . i) = ((x * y) . j) by A4, FUNCT_1: 13

          .= (xj * yj) by GROUP_7: 1

          .= (xai * yai) by A4, A6, A7, FUNCT_1: 13

          .= ((xa * ya) . i) by GROUP_7: 1;

          hence thesis;

        end;

        then (xa * ya) = ((x * y) * a) by A3, A4, A5, RELAT_1: 27;

        hence thesis by A1, A2, Def2;

      end;

      hence thesis by GROUP_6:def 6;

    end;

    definition

      let I,J be non empty set;

      let a be Function of I, J;

      let F be Group-Family of J;

      :: original: trans_prod

      redefine

      func trans_prod (F,a) -> Homomorphism of ( product F), ( product (F * a)) ;

      correctness by Th2;

    end

    theorem :: GROUP_21:5

    

     Th3: for I,J be non empty set, a be Function of I, J, F be multMagma-Family of J, y be Element of ( product (F * a)) st a is bijective holds (y * (a " )) in ( product F)

    proof

      let I,J be non empty set, a be Function of I, J, F be multMagma-Family of J, y be Element of ( product (F * a));

      assume

       A1: a is bijective;

      then

       A2: ( dom a) = I & ( rng a) = J by GROUP_6: 61;

      then

       A3: ( dom (a " )) = J & ( rng (a " )) = I by A1, FUNCT_1: 33;

      set x = (y * (a " ));

      ( dom y) = I by GROUP_19: 3;

      then

       A4: ( dom x) = J by A3, RELAT_1: 27;

      

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

      for j be object st j in J holds (x . j) in (( Carrier F) . j)

      proof

        let j be object;

        assume j in J;

        then

        reconsider j as Element of J;

        consider i be object such that

         A6: i in I & j = (a . i) by A2, FUNCT_1:def 3;

        reconsider i as Element of I by A6;

        i = ((a " ) . j) by A1, A2, A6, FUNCT_1: 32;

        then

         A7: (x . j) = (y . i) by A3, FUNCT_1: 13;

        

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

        y in ( product (F * a));

        then (y . i) in ((F * a) . i) by GROUP_19: 5;

        hence thesis by A2, A6, A7, A8, FUNCT_1: 13;

      end;

      then x in ( product ( Carrier F)) by A4, A5, CARD_3:def 5;

      hence thesis by GROUP_7:def 2;

    end;

    theorem :: GROUP_21:6

    

     Th4: for I,J be non empty set, a be Function of I, J, x,y be Function st ( dom x) = I & ( dom y) = J & a is bijective holds x = (y * a) iff y = (x * (a " ))

    proof

      let I,J be non empty set, a be Function of I, J, x,y be Function;

      assume that

       A1: ( dom x) = I and

       A2: ( dom y) = J and

       A3: a is bijective;

      

       A4: ( dom a) = I & ( rng a) = J by A3, GROUP_6: 61;

      hereby

        assume

         A5: x = (y * a);

        

        thus y = (y * ( id J)) by A2, RELAT_1: 51

        .= (y * (a * (a " ))) by A3, A4, FUNCT_2: 29

        .= (x * (a " )) by A5, RELAT_1: 36;

      end;

      assume

       A6: y = (x * (a " ));

      

      thus x = (x * ( id I)) by A1, RELAT_1: 51

      .= (x * ((a " ) * a)) by A3, A4, FUNCT_2: 29

      .= (y * a) by A6, RELAT_1: 36;

    end;

    theorem :: GROUP_21:7

    

     Th5: for I,J be non empty set, F be multMagma-Family of J, a be Function of I, J st a is bijective holds ( dom ( trans_prod (F,a))) = ( [#] ( product F)) & ( rng ( trans_prod (F,a))) = ( [#] ( product (F * a)))

    proof

      let I,J be non empty set, F be multMagma-Family of J, a be Function of I, J;

      assume

       A1: a is bijective;

      set f = ( trans_prod (F,a));

      for y be object st y in ( [#] ( product (F * a))) holds ex x be object st x in ( [#] ( product F)) & y = (f . x)

      proof

        let y be object;

        assume y in ( [#] ( product (F * a)));

        then

        reconsider y as Element of ( product (F * a));

        set x = (y * (a " ));

        x in ( product F) by A1, Th3;

        then

        reconsider x as Element of ( product F);

        ( dom x) = J & ( dom y) = I by GROUP_19: 3;

        then y = (x * a) by A1, Th4;

        then y = (f . x) by Def2;

        hence thesis;

      end;

      hence thesis by FUNCT_2: 10, FUNCT_2:def 1;

    end;

    theorem :: GROUP_21:8

    

     Th6: for I,J be non empty set, a be Function of I, J, F be multMagma-Family of J st a is bijective holds ( trans_prod (F,a)) is bijective

    proof

      let I,J be non empty set, a be Function of I, J, F be multMagma-Family of J;

      assume

       A1: a is bijective;

      reconsider f = ( trans_prod (F,a)) as Function of ( product F), ( product (F * a));

      

       A2: ( dom f) = ( [#] ( product F)) & ( rng f) = ( [#] ( product (F * a))) by A1, Th5;

      for x,y be object st x in ( dom f) & y in ( dom f) & (f . x) = (f . y) holds x = y

      proof

        let x,y be object;

        assume that

         A3: x in ( dom f) and

         A4: y in ( dom f) and

         A5: (f . x) = (f . y);

        reconsider x as Element of ( product F) by A3;

        reconsider y as Element of ( product F) by A4;

        

         A6: ( dom x) = J & ( dom y) = J by GROUP_19: 3;

        

         A7: ( rng a) = J by A1, FUNCT_2:def 3;

        (f . x) = (x * a) by Def2;

        then (x * a) = (y * a) by A5, Def2;

        hence thesis by A6, A7, FUNCT_1: 86;

      end;

      then

       A8: f is one-to-one;

      f is onto by A2, FUNCT_2:def 3;

      hence thesis by A8;

    end;

    theorem :: GROUP_21:9

    

     Th7: for I,J be non empty set, a be Function of I, J, F be Group-Family of J, x be Function holds (a .: ( support ((x * a),(F * a)))) c= ( support (x,F))

    proof

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

      for j be object st j in (a .: ( support ((x * a),(F * a)))) holds j in ( support (x,F))

      proof

        let j be object;

        assume j in (a .: ( support ((x * a),(F * a))));

        then

        consider i be object such that

         A1: i in ( dom a) and

         A2: i in ( support ((x * a),(F * a))) and

         A3: j = (a . i) by FUNCT_1:def 6;

        consider Z be Group such that

         B1: Z = ((F * a) . i) & ((x * a) . i) <> ( 1_ Z) & i in I by A2, GROUP_19:def 1;

        reconsider y = (x * a) as Function;

        reconsider G = (F * a) as Group-Family of I;

        reconsider i as Element of I by B1;

        j = (a . i) by A3;

        then

        reconsider j as Element of J;

        

         A5: ( 1_ (G . i)) = ( 1_ (F . j)) by A1, A3, FUNCT_1: 13;

        (x . j) <> ( 1_ (F . j)) by A1, A3, B1, A5, FUNCT_1: 13;

        hence thesis by GROUP_19:def 1;

      end;

      hence thesis;

    end;

    theorem :: GROUP_21:10

    

     Th8: for I,J be non empty set, a be Function of I, J, F be Group-Family of J, x be Function st a is onto holds ( support (x,F)) c= (a .: ( support ((x * a),(F * a))))

    proof

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

      assume

       A1: a is onto;

      for j be object st j in ( support (x,F)) holds j in (a .: ( support ((x * a),(F * a))))

      proof

        let j be object;

        assume

         A2: j in ( support (x,F));

        

         A3: ( dom a) = I by FUNCT_2:def 1;

        ( rng a) = J by A1, FUNCT_2:def 3;

        then

        consider i be object such that

         A4: i in I and

         A5: j = (a . i) by A2, FUNCT_2: 11;

        reconsider y = (x * a) as Function;

        reconsider G = (F * a) as Group-Family of I;

        consider Z be Group such that

         B1: Z = (F . j) & (x . j) <> ( 1_ Z) & j in J by A2, GROUP_19:def 1;

        reconsider j as Element of J by B1;

        reconsider i as Element of I by A4;

        

         A6: ( 1_ (G . i)) = ( 1_ (F . j)) by A3, A5, FUNCT_1: 13;

        (x . j) = (y . i) by A3, A5, FUNCT_1: 13;

        then i in ( support (y,G)) by A6, B1, GROUP_19:def 1;

        hence thesis by A3, A5, FUNCT_1:def 6;

      end;

      hence thesis;

    end;

    theorem :: GROUP_21:11

    

     Th9: for I,J be non empty set, a be Function of I, J, F be Group-Family of J, x be Function st a is one-to-one holds x in ( sum F) implies (x * a) in ( sum (F * a))

    proof

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

      assume

       A1: a is one-to-one;

      assume

       A2: x in ( sum F);

      then x in ( product F) by GROUP_2: 40;

      then

      reconsider x as Element of ( product F);

      reconsider Fa = (F * a) as Group-Family of I;

      (x * a) in ( product (F * a)) by Th1;

      then

      reconsider xa = (x * a) as Element of ( product (F * a));

      

       A3: ( dom a) = I by FUNCT_2:def 1;

      

       A4: (a .: ( support (xa,Fa))) c= ( support (x,F)) by Th7;

      ((a .: ( support (xa,Fa))),( support (xa,Fa))) are_equipotent by A1, A3, CARD_1: 33;

      then ( support (xa,Fa)) is finite by A2, A4, CARD_1: 38;

      hence thesis by GROUP_19: 8;

    end;

    theorem :: GROUP_21:12

    

     Th10: for I,J be non empty set, a be Function of I, J, F be Group-Family of J, x be Function st a is bijective holds x in ( sum F) iff (x * a) in ( sum (F * a)) & ( dom x) = J

    proof

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

      assume

       A1: a is bijective;

      hereby

        assume

         A2: x in ( sum F);

        then x in ( product F) by GROUP_2: 40;

        hence (x * a) in ( sum (F * a)) & ( dom x) = J by A1, A2, Th9, GROUP_19: 3;

      end;

      assume

       A3: (x * a) in ( sum (F * a)) & ( dom x) = J;

      

       A4: ( rng a) = J & a is one-to-one by A1, FUNCT_2:def 3;

      then

      reconsider b = (a " ) as Function of J, I by FUNCT_2: 25;

      

       A5: (a * b) = ( id J) & (b * a) = ( id I) by A4, FUNCT_2: 29;

      

       A6: ( dom F) = J by PARTFUN1:def 2;

      ((x * a) * b) in ( sum ((F * a) * b)) by A3, A1, Th9;

      then (x * (a * b)) in ( sum ((F * a) * b)) by RELAT_1: 36;

      then (x * ( id J)) in ( sum (F * ( id J))) by A5, RELAT_1: 36;

      then x in ( sum (F * ( id J))) by A3, RELAT_1: 52;

      hence x in ( sum F) by A6, RELAT_1: 52;

    end;

    definition

      let I,J be non empty set;

      let a be Function of I, J;

      let F be Group-Family of J;

      assume

       A1: a is bijective;

      :: GROUP_21:def3

      func trans_sum (F,a) -> Function of ( sum F), ( sum (F * a)) equals

      : Def3: (( trans_prod (F,a)) | ( sum F));

      correctness

      proof

        set f = ( trans_prod (F,a));

        set g = (f | ( sum F));

        set G = (F * a);

        

         A2: ( dom g) = ( [#] ( sum F)) by FUNCT_2:def 1;

        for y be object st y in ( rng g) holds y in ( [#] ( sum G))

        proof

          let y be object;

          assume

           A3: y in ( rng g);

          then

          consider x be object such that

           A4: x in ( dom g) and

           A5: y = (g . x) by FUNCT_1:def 3;

          ( [#] ( sum F)) c= ( [#] ( product F)) by GROUP_2:def 5;

          then

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

          reconsider y as Element of ( product G) by A3;

          

           A6: ( dom a) = I by FUNCT_2:def 1;

          y = (f . x) by A4, A5, FUNCT_1: 49;

          then

           A7: y = (x * a) by Def2;

          then

           A8: (a .: ( support (y,G))) c= ( support (x,F)) by Th7;

          ( support (x,F)) c= (a .: ( support (y,G))) by A1, A7, Th8;

          then ((a " ) .: ( support (x,F))) = ((a " ) .: (a .: ( support (y,G)))) by A8, XBOOLE_0:def 10;

          then ( support (y,G)) is finite by A1, A4, A6, FUNCT_1: 107;

          then y in ( sum G) by GROUP_19: 8;

          hence thesis;

        end;

        hence thesis by A2, FUNCT_2: 2, TARSKI:def 3;

      end;

    end

    theorem :: GROUP_21:13

    

     Th11: for G,H be Group, H0 be Subgroup of H, f be Homomorphism of G, H st ( rng f) c= ( [#] H0) holds f is Homomorphism of G, H0

    proof

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

      assume ( rng f) c= ( [#] H0);

      then

      reconsider g = f as Function of G, H0 by FUNCT_2: 6;

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

      proof

        let a,b be Element of G;

        (g . (a * b)) = ((f . a) * (f . b)) by GROUP_6:def 6

        .= ((g . a) * (g . b)) by GROUP_2: 43;

        hence thesis;

      end;

      hence thesis by GROUP_6:def 6;

    end;

    theorem :: GROUP_21:14

    

     TT: for I,J be non empty set holds for a be Function of I, J holds for F be Group-Family of J st a is bijective holds ( trans_sum (F,a)) is Homomorphism of ( sum F), ( sum (F * a))

    proof

      let I,J be non empty set;

      let a be Function of I, J;

      let F be Group-Family of J;

      assume

       A1: a is bijective;

      set f = ( trans_sum (F,a));

      

       A2: f = (( trans_prod (F,a)) | ( sum F)) by A1, Def3;

      ( rng f) c= ( [#] ( sum (F * a)));

      hence thesis by A2, Th11;

    end;

    theorem :: GROUP_21:15

    

     Th12: for I,J be non empty set, a be Function of I, J, F be Group-Family of J st a is bijective holds ( trans_sum (F,a)) is bijective

    proof

      let I,J be non empty set, a be Function of I, J, F be Group-Family of J;

      assume

       A1: a is bijective;

      reconsider f = ( trans_prod (F,a)) as Homomorphism of ( product F), ( product (F * a));

      reconsider g = ( trans_sum (F,a)) as Homomorphism of ( sum F), ( sum (F * a)) by A1, TT;

      

       A2: g = (f | ( sum F)) by A1, Def3;

      f is bijective by A1, Th6;

      then

       A3: g is one-to-one by A2, FUNCT_1: 52;

      for y be object st y in ( [#] ( sum (F * a))) holds y in ( rng g)

      proof

        let y be object;

        assume

         A4: y in ( [#] ( sum (F * a)));

        then

        reconsider y as Element of ( product (F * a)) by GROUP_2: 42;

        set x = (y * (a " ));

        x in ( product F) by A1, Th3;

        then

        reconsider x as Element of ( product F);

        

         A5: ( dom g) = ( [#] ( sum F)) by FUNCT_2:def 1;

        

         A6: ( dom x) = J & ( dom y) = I by GROUP_19: 3;

        then

         A7: y = (x * a) by A1, Th4;

        y in ( sum (F * a)) by A4;

        then

         A8: x in ( sum F) by A1, A6, A7, Th10;

        y = (f . x) by A7, Def2;

        then y = (g . x) by A2, A8, FUNCT_1: 49;

        hence thesis by A5, A8, FUNCT_1:def 3;

      end;

      then ( [#] ( sum (F * a))) c= ( rng g);

      then g is onto by FUNCT_2:def 3, XBOOLE_0:def 10;

      hence thesis by A3;

    end;

    theorem :: GROUP_21:16

    

     Th13: for G be Group, I,J be non empty set, F be DirectSumComponents of G, J, a be Function of I, J st a is bijective holds (F * a) is DirectSumComponents of G, I

    proof

      let G be Group, I,J be non empty set, F be DirectSumComponents of G, J, a be Function of I, J;

      assume

       A1: a is bijective;

      consider h1 be Homomorphism of ( sum F), G such that

       A2: h1 is bijective by GROUP_19:def 8;

      reconsider h2 = ( trans_sum (F,a)) as Homomorphism of ( sum F), ( sum (F * a)) by A1, TT;

      

       A3: h2 is bijective by A1, Th12;

      then

      reconsider h3 = (h2 " ) as Homomorphism of ( sum (F * a)), ( sum F) by GROUP_6: 62;

      reconsider h = (h1 * h3) as Homomorphism of ( sum (F * a)), G;

      h3 is bijective by A3, GROUP_6: 63;

      then h is bijective by A2, GROUP_6: 64;

      hence thesis by GROUP_19:def 8;

    end;

    theorem :: GROUP_21:17

    for I be non empty set, G be Group, F be internal DirectSumComponents of G, I holds F is Subgroup-Family of I, G

    proof

      let I be non empty set, G be Group, F be internal DirectSumComponents of G, I;

      for i be object st i in I holds (F . i) is Subgroup of G by GROUP_19:def 9;

      hence thesis by GROUP_20:def 1;

    end;

    theorem :: GROUP_21:18

    

     Th15: for I,J be non empty set, G be Group, x be Function of I, G, y be Function of J, G, a be Function of I, J st a is onto & x = (y * a) holds ( support y) = (a .: ( support x))

    proof

      let I,J be non empty set, G be Group, x be Function of I, G, y be Function of J, G, a be Function of I, J;

      assume that

       A1: a is onto and

       A2: x = (y * a);

      

       A3: ( rng a) = J by A1, FUNCT_2:def 3;

      now

        let j be object;

        assume

         A4: j in ( support y);

        then

        consider i be object such that

         A5: i in ( dom a) and

         A6: j = (a . i) by A3, FUNCT_1:def 3;

        (x . i) = (y . j) by A2, A5, A6, FUNCT_1: 13;

        then (x . i) <> ( 1_ G) by A4, GROUP_19:def 2;

        then i in ( support x) by A5, GROUP_19:def 2;

        hence j in (a .: ( support x)) by A5, A6, FUNCT_1:def 6;

      end;

      then

       A7: ( support y) c= (a .: ( support x));

      now

        let j be object;

        assume j in (a .: ( support x));

        then

        consider i be object such that

         A8: i in ( dom a) and

         A9: i in ( support x) and

         A10: j = (a . i) by FUNCT_1:def 6;

        

         A11: j in J by A8, A10, FUNCT_2: 5;

        (x . i) = (y . j) by A2, A8, A10, FUNCT_1: 13;

        then (y . j) <> ( 1_ G) by A9, GROUP_19:def 2;

        hence j in ( support y) by A11, GROUP_19:def 2;

      end;

      then (a .: ( support x)) c= ( support y);

      hence thesis by A7, XBOOLE_0:def 10;

    end;

    theorem :: GROUP_21:19

    

     Th16: for I,J be non empty set, G be commutative Group, x be finite-support Function of I, G, y be finite-support Function of J, G, a be Function of I, J st a is bijective & x = (y * a) holds ( Product x) = ( Product y)

    proof

      let I,J be non empty set, G be commutative Group, x be finite-support Function of I, G, y be finite-support Function of J, G, a be Function of I, J;

      assume that

       A1: a is bijective and

       A2: x = (y * a);

      

       A3: ( dom a) = I by FUNCT_2:def 1;

      

       A4: ( rng a) = J by A1, FUNCT_2:def 3;

      reconsider Sx = ( support x) as finite set;

      reconsider Sy = ( support y) as finite set;

      reconsider cx = ( canFS Sx) as FinSequence of Sx;

      reconsider cy = ( canFS Sy) as FinSequence of Sy;

      reconsider x1 = (x | Sx) as Function of Sx, G by FUNCT_2: 32;

      consider x2 be FinSequence of G such that

       A5: ( Product x1) = ( Product x2) and

       A6: x2 = (x1 * cx) by GROUP_17:def 1;

      reconsider y1 = (y | Sy) as Function of Sy, G by FUNCT_2: 32;

      consider y2 be FinSequence of G such that

       A7: ( Product y1) = ( Product y2) and

       A8: y2 = (y1 * cy) by GROUP_17:def 1;

      

       A9: Sy = (a .: Sx) by A1, A2, Th15;

      

       A10: ( card Sx) = ( card Sy)

      proof

        

         A11: ( card Sy) c= ( card Sx) by A9, CARD_1: 66;

        reconsider ia = (a " ) as Function of J, I by A1, A4, FUNCT_2: 25;

        

         A12: ia is bijective by A1, GROUP_6: 63;

        y = (y * ( id J)) by FUNCT_2: 17

        .= (y * (a * ia)) by A1, A4, FUNCT_2: 29

        .= (x * ia) by A2, RELAT_1: 36;

        then Sx = (ia .: Sy) by A12, Th15;

        then ( card Sx) c= ( card Sy) by CARD_1: 66;

        hence thesis by A11, XBOOLE_0:def 10;

      end;

      reconsider n = ( card Sx) as Nat;

      reconsider a1 = (a | Sx) as Function of Sx, J by FUNCT_2: 32;

      

       A13: ( dom a1) = Sx by FUNCT_2:def 1;

      

       A14: ( rng a1) = Sy by A9, RELAT_1: 115;

      then

      reconsider a1 as Function of Sx, Sy by A13, FUNCT_2: 1;

      

       A15: ( len cx) = n by FINSEQ_1: 93;

      then

       A16: ( dom cx) = ( Seg n) by FINSEQ_1:def 3;

      

       A17: ( rng cx) = Sx by FUNCT_2:def 3;

      then

      reconsider cx as Function of ( Seg n), Sx by A16, FUNCT_2: 1;

      ( len cy) = n by A10, FINSEQ_1: 93;

      then

       A18: ( dom cy) = ( Seg n) by FINSEQ_1:def 3;

      

       A19: ( rng cy) = Sy by FUNCT_2:def 3;

      then

      reconsider cy as Function of ( Seg n), Sy by A18, FUNCT_2: 1;

      reconsider icy = (cy " ) as Function of Sy, ( Seg n) by A10, FINSEQ_1: 95;

      reconsider p = ((icy * a1) * cx) as Function;

      

       A20: ( dom a1) = ( rng cx) by A13, FUNCT_2:def 3;

      

       A21: ( dom icy) = ( rng a1) by A14, A19, FUNCT_1: 33;

      

       A22: ( dom (a1 * cx)) = ( dom cx) by A20, RELAT_1: 27;

      

       A23: ( rng (a1 * cx)) = ( rng a1) by A20, RELAT_1: 28;

      

       A24: ( dom p) = ( dom (icy * (a1 * cx))) by RELAT_1: 36

      .= ( dom (a1 * cx)) by A21, A23, RELAT_1: 27

      .= ( dom cx) by A20, RELAT_1: 27

      .= ( Seg n) by A15, FINSEQ_1:def 3;

      

       A25: ( rng p) = ( rng (icy * (a1 * cx))) by RELAT_1: 36

      .= ( rng icy) by A21, A23, RELAT_1: 28

      .= ( Seg n) by A18, FUNCT_1: 33;

      reconsider p as Function of ( Seg n), ( Seg n) by A24, A25, FUNCT_2: 1;

      ( rng cy) = ( dom y1) by A19, FUNCT_2:def 1;

      then

       A26: ( dom y2) = ( Seg n) by A8, A18, RELAT_1: 27;

      a1 is one-to-one by A1, FUNCT_1: 52;

      then p is one-to-one onto by A25, FUNCT_2:def 3;

      then

      reconsider p as Permutation of ( dom y2) by A26;

      

       A27: not Sy is empty implies x2 = (y2 * p)

      proof

        assume

         A28: not Sy is empty;

        

         A29: ( dom x1) = Sx by FUNCT_2:def 1;

        then

         A30: ( dom x2) = ( Seg n) by A6, A16, A17, RELAT_1: 27;

        for i be object st i in ( dom x2) holds (x2 . i) = ((y2 * p) . i)

        proof

          let i be object;

          assume

           A31: i in ( dom x2);

          then

           A32: i in ( Seg n) by A6, A16, A17, A29, RELAT_1: 27;

          

           A33: (cx . i) in Sx by A16, A17, A30, A31, FUNCT_1: 3;

          

           A34: (x2 . i) = (x1 . (cx . i)) by A6, A31, FUNCT_1: 12

          .= (x . (cx . i)) by A16, A17, A29, A30, A31, FUNCT_1: 3, FUNCT_1: 47;

          

           A35: (y1 * (cy * icy)) = (y1 * ( id Sy)) by A19, A28, FUNCT_2: 29

          .= y1 by FUNCT_2: 17;

          

           A36: (y2 * p) = ((y1 * cy) * (icy * (a1 * cx))) by A8, RELAT_1: 36

          .= (((y1 * cy) * icy) * (a1 * cx)) by RELAT_1: 36

          .= (y1 * (a1 * cx)) by A35, RELAT_1: 36;

          

           A37: ((a1 * cx) . i) = (a1 . (cx . i)) by A16, A32, FUNCT_1: 13

          .= (a . (cx . i)) by A16, A17, A30, A31, FUNCT_1: 3, FUNCT_1: 49;

          ((y2 * p) . i) = (y1 . ((a1 * cx) . i)) by A16, A22, A32, A36, FUNCT_1: 13

          .= (y . (a . (cx . i))) by A14, A16, A22, A23, A32, A37, FUNCT_1: 3, FUNCT_1: 49

          .= (x2 . i) by A2, A3, A33, A34, FUNCT_1: 13;

          hence thesis;

        end;

        hence thesis by A24, A25, A26, A30, RELAT_1: 27;

      end;

      per cases ;

        suppose

         A38: Sy is empty;

        then Sx is empty by A10;

        hence thesis by A38;

      end;

        suppose not Sy is empty;

        hence thesis by A5, A7, A27, GROUP_4: 15;

      end;

    end;

    theorem :: GROUP_21:20

    for I,J be non empty set, G be Group, x be finite-support Function of I, G, y be finite-support Function of J, G, a be Function of I, J st a is bijective & x = (y * a) & for i,j be Element of I holds ((x . i) * (x . j)) = ((x . j) * (x . i)) holds ( Product x) = ( Product y)

    proof

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

      assume that

       A1: a is bijective and

       A2: x = (y * a) and

       A3: for i,j be Element of I holds ((x . i) * (x . j)) = ((x . j) * (x . i));

      reconsider rx = ( rng x) as non empty Subset of G;

      reconsider ry = ( rng y) as non empty Subset of G;

      

       A4: ( dom y) = J by FUNCT_2:def 1;

      

       A5: ( rng a) = J by A1, FUNCT_2:def 3;

      

       A6: ( gr rx) = ( gr ry) by A2, A4, A5, RELAT_1: 28;

      ( rng x) c= ( [#] ( gr rx)) by GROUP_4:def 4;

      then

      reconsider x1 = x as finite-support Function of I, ( gr rx) by GROUP_20: 5;

      ( rng y) c= ( [#] ( gr ry)) by GROUP_4:def 4;

      then

      reconsider y1 = y as finite-support Function of J, ( gr rx) by A6, GROUP_20: 5;

      now

        let a,b be Element of G;

        assume that

         A7: a in rx and

         A8: b in rx;

        consider i be object such that

         A9: i in ( dom x) and

         A10: a = (x . i) by A7, FUNCT_1:def 3;

        consider j be object such that

         A11: j in ( dom x) and

         A12: b = (x . j) by A8, FUNCT_1:def 3;

        reconsider i as Element of I by A9;

        reconsider j as Element of I by A11;

        ((x . i) * (x . j)) = ((x . j) * (x . i)) by A3;

        hence (a * b) = (b * a) by A10, A12;

      end;

      then ( gr rx) is commutative by GROUP_19: 44;

      then

       A14: ( Product x1) = ( Product y1) by A1, A2, Th16;

      ( Product x) = ( Product x1) by GROUP_20: 6;

      hence thesis by A14, GROUP_20: 6;

    end;

    theorem :: GROUP_21:21

    for G be Group, I,J be non empty set, F be internal DirectSumComponents of G, J, a be Function of I, J st a is bijective holds (F * a) is internal DirectSumComponents of G, I

    proof

      let G be Group, I,J be non empty set, F be internal DirectSumComponents of G, J, a be Function of I, J;

      assume

       A1: a is bijective;

      then

      reconsider E = (F * a) as DirectSumComponents of G, I by Th13;

      

       A2: for i be Element of I holds (E . i) is Subgroup of G

      proof

        let i be Element of I;

        

         A3: ( dom a) = I by FUNCT_2:def 1;

        reconsider j = (a . i) as Element of J;

        (F . j) is Subgroup of G by GROUP_19:def 9;

        hence thesis by A3, FUNCT_1: 13;

      end;

      

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

      ex h be Homomorphism of ( sum E), G st h is bijective & for x be finite-support Function of I, G st x in ( sum E) holds (h . x) = ( Product x)

      proof

        consider hFG be Homomorphism of ( sum F), G such that

         A5: hFG is bijective and

         A6: for y be finite-support Function of J, G st y in ( sum F) holds (hFG . y) = ( Product y) by GROUP_19:def 9;

        reconsider hFE = ( trans_sum (F,a)) as Homomorphism of ( sum F), ( sum E) by A1, TT;

        

         A7: hFE is bijective by A1, Th12;

        then

        reconsider hEF = (hFE " ) as Homomorphism of ( sum E), ( sum F) by GROUP_6: 62;

        reconsider h = (hFG * hEF) as Homomorphism of ( sum E), G;

        take h;

        

         A8: hEF is bijective by A7, GROUP_6: 63;

        

         A9: for i be Element of I, g be Element of (E . i) holds (h . (( 1ProdHom (E,i)) . g)) = g

        proof

          let i be Element of I, g be Element of (E . i);

          (( 1_ ( product E)) +* (i,g)) in ( sum E) by GROUP_19: 25, GROUP_2: 46;

          then

          reconsider x = (( 1_ ( product E)) +* (i,g)) as Element of ( sum E);

          reconsider j = (a . i) as Element of J;

          

           A10: ( dom a) = I by FUNCT_2:def 1;

          then

           A11: (E . i) = (F . j) by FUNCT_1: 13;

          reconsider g1 = g as Element of (F . j) by A10, FUNCT_1: 13;

          (F . j) is Subgroup of G by A2, A11;

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

          then

          reconsider g2 = g1 as Element of G;

          reconsider y = (hEF . x) as Element of ( sum F);

          

           A12: for j be object st j in J holds (F . j) is Subgroup of G by GROUP_19:def 9;

          y in ( sum F);

          then

          reconsider y1 = y as finite-support Function of J, G by A12, GROUP_19: 10;

          

           A13: hFE = (( trans_prod (F,a)) | ( sum F)) by A1, Def3;

          

           A14: x = (y * a)

          proof

            reconsider y2 = y1 as Element of ( product F) by GROUP_2: 42;

            

             A15: ( rng hFE) = ( [#] ( sum E)) by A7, FUNCT_2:def 3;

            

             A16: ( dom hEF) = ( [#] ( sum E)) by FUNCT_2:def 1;

            x = (( id ( [#] ( sum E))) . x)

            .= ((hFE * hEF) . x) by A7, A15, FUNCT_2: 29

            .= (hFE . y) by A16, FUNCT_1: 13

            .= (( trans_prod (F,a)) . y2) by A13, FUNCT_1: 49

            .= (y2 * a) by Def2;

            hence thesis;

          end;

          

           A17: y = ((J --> ( 1_ G)) +* (j,g2))

          proof

            reconsider z = ((J --> ( 1_ G)) +* (j,g2)) as Function;

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

            then

             A18: ( dom y) = J by GROUP_19: 3;

            

             A19: ( dom (J --> ( 1_ G))) = J by FUNCOP_1: 13;

            for j0 be object st j0 in J holds (y . j0) = (z . j0)

            proof

              let j0 be object;

              assume j0 in J;

              then

              reconsider j0 as Element of J;

              

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

              per cases ;

                suppose

                 A21: j0 = j;

                

                then (y . j0) = (x . i) by A10, A14, FUNCT_1: 13

                .= g by A20, FUNCT_7: 31;

                hence thesis by A19, A21, FUNCT_7: 31;

              end;

                suppose

                 A22: j0 <> j;

                

                 A23: a is one-to-one & ( rng a) = J by A1, FUNCT_2:def 3;

                then

                reconsider ia = (a " ) as Function of J, I by FUNCT_2: 25;

                reconsider i0 = (ia . j0) as Element of I;

                

                 A24: (ia . j) = ((ia * a) . i) by A10, FUNCT_1: 13

                .= (( id I) . i) by A23, FUNCT_2: 29

                .= i;

                

                 A25: ( dom ia) = J by FUNCT_2:def 1;

                

                 A26: ia is one-to-one by A1;

                

                 A27: j0 = (( id J) . j0)

                .= ((a * ia) . j0) by A23, FUNCT_2: 29

                .= (a . i0) by A25, FUNCT_1: 13;

                

                 A28: (y . j0) = ((y * a) . i0) by A10, A27, FUNCT_1: 13

                .= (( 1_ ( product E)) . i0) by A14, A22, A24, A25, A26, FUNCT_7: 32

                .= ((I --> ( 1_ G)) . i0) by A2, GROUP_19: 13

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

                (z . j0) = ((J --> ( 1_ G)) . j0) by A22, FUNCT_7: 32

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

                hence thesis by A28;

              end;

            end;

            hence thesis by A18, A19, FUNCT_7: 30;

          end;

          y in ( sum F);

          

          then

           A29: (hFG . y) = ( Product y1) by A6

          .= g2 by A17, GROUP_19: 21;

          x in ( sum E);

          then

           A30: x in ( dom hEF) by FUNCT_2:def 1;

          (h . x) = g by A29, A30, FUNCT_1: 13;

          hence thesis by GROUP_12:def 3;

        end;

        E is Subgroup-Family of I, G by A4, GROUP_20:def 1;

        hence thesis by A5, A8, A9, GROUP_20: 18, GROUP_6: 64;

      end;

      hence thesis by A2, GROUP_19:def 9;

    end;

    begin

    definition

      let I be non empty set;

      let J be ManySortedSet of I;

      :: GROUP_21:def4

      mode multMagma-Family of I,J -> ManySortedSet of I means

      : Def4: for i be Element of I holds (it . i) is multMagma-Family of (J . i);

      existence

      proof

        set G = the non empty multMagma;

        deffunc DF( object) = ((J . $1) --> G);

        consider f be Function such that

         A1: ( dom f) = I & for i be set st i in I holds (f . i) = DF(i) from FUNCT_1:sch 5;

        reconsider f as ManySortedSet of I by A1, PARTFUN1:def 2, RELAT_1:def 18;

        take f;

        for i be Element of I holds (f . i) is multMagma-Family of (J . i)

        proof

          let i be Element of I;

          set fi = ((J . i) --> G);

          

           A2: fi = (f . i) by A1;

          for a be set st a in ( rng fi) holds a is non empty multMagma by TARSKI:def 1;

          hence thesis by A2, GROUP_7:def 1;

        end;

        hence thesis;

      end;

    end

    definition

      let I be non empty set;

      let J be ManySortedSet of I;

      :: GROUP_21:def5

      mode Group-Family of I,J -> multMagma-Family of I, J means

      : Def5: for i be Element of I holds (it . i) is Group-Family of (J . i);

      existence

      proof

        set G = the Group;

        deffunc DF( object) = ((J . $1) --> G);

        consider f be Function such that

         A1: ( dom f) = I & for i be set st i in I holds (f . i) = DF(i) from FUNCT_1:sch 5;

        reconsider f as ManySortedSet of I by A1, PARTFUN1:def 2, RELAT_1:def 18;

        

         A2: for i be Element of I holds (f . i) is Group-Family of (J . i)

        proof

          let i be Element of I;

          set fi = ((J . i) --> G);

          

           A3: (f . i) = fi by A1;

          

           A4: ( dom fi) = (J . i) by FUNCOP_1: 13;

          for k be object st k in (J . i) holds (fi . k) is Group by FUNCOP_1: 7;

          hence thesis by A3, A4, GROUP_19: 2;

        end;

        then for i be Element of I holds (f . i) is multMagma-Family of (J . i);

        then

        reconsider f as multMagma-Family of I, J by Def4;

        take f;

        thus thesis by A2;

      end;

    end

    definition

      let I be non empty set;

      let J be ManySortedSet of I;

      let N be multMagma-Family of I, J;

      let i be Element of I;

      :: original: .

      redefine

      func N . i -> multMagma-Family of (J . i) ;

      correctness by Def4;

    end

    definition

      let I be non empty set;

      let J be ManySortedSet of I;

      let N be Group-Family of I, J;

      let i be Element of I;

      :: original: .

      redefine

      func N . i -> Group-Family of (J . i) ;

      correctness by Def5;

    end

    definition

      let I be non empty set;

      let J be disjoint_valued ManySortedSet of I;

      let F be Group-Family of I, J;

      :: original: Union

      redefine

      func Union F -> Group-Family of ( Union J) ;

      correctness

      proof

        set UF = ( Union F);

        

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

        

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

        for x be object st x in UF holds ex y,z be object st x = [y, z]

        proof

          let x be object;

          assume x in UF;

          then

          consider Y be set such that

           A3: x in Y & Y in ( rng F) by TARSKI:def 4;

          consider i be object such that

           A4: i in ( dom F) & Y = (F . i) by A3, FUNCT_1:def 3;

          reconsider i as Element of I by A4;

          (F . i) is Relation;

          hence thesis by A3, A4, RELAT_1:def 1;

        end;

        then

        reconsider UF as Relation by RELAT_1:def 1;

        for x,y1,y2 be object st [x, y1] in UF & [x, y2] in UF holds y1 = y2

        proof

          let x,y1,y2 be object;

          assume

           A5: [x, y1] in UF & [x, y2] in UF;

          then

          consider Y1 be set such that

           A6: [x, y1] in Y1 & Y1 in ( rng F) by TARSKI:def 4;

          consider i1 be object such that

           A7: i1 in ( dom F) & Y1 = (F . i1) by A6, FUNCT_1:def 3;

          reconsider i1 as Element of I by A7;

          reconsider Fi1 = (F . i1) as Function;

          x in ( dom Fi1) by A6, A7, FUNCT_1: 1;

          then

           A8: x in (J . i1) by PARTFUN1:def 2;

          consider Y2 be set such that

           A9: [x, y2] in Y2 & Y2 in ( rng F) by A5, TARSKI:def 4;

          consider i2 be object such that

           A10: i2 in ( dom F) & Y2 = (F . i2) by A9, FUNCT_1:def 3;

          reconsider i2 as Element of I by A10;

          reconsider Fi2 = (F . i2) as Function;

          x in ( dom Fi2) by A9, A10, FUNCT_1: 1;

          then x in (J . i2) by PARTFUN1:def 2;

          then ((J . i1) /\ (J . i2)) <> {} by A8, XBOOLE_0:def 4;

          then [x, y1] in (F . i1) & [x, y2] in (F . i1) by A6, A7, A9, A10, PROB_2:def 2, XBOOLE_0:def 7;

          hence thesis by FUNCT_1:def 1;

        end;

        then

        reconsider UF as Function by FUNCT_1:def 1;

        

         A11: for x be object holds x in ( dom UF) iff x in ( Union J)

        proof

          let x be object;

          hereby

            assume x in ( dom UF);

            then

            consider y be object such that

             A12: [x, y] in UF by XTUPLE_0:def 12;

            consider Y be set such that

             A13: [x, y] in Y & Y in ( rng F) by A12, TARSKI:def 4;

            consider i be object such that

             A14: i in ( dom F) & Y = (F . i) by A13, FUNCT_1:def 3;

            reconsider i as Element of I by A14;

            reconsider Fi = (F . i) as Function;

            x in ( dom Fi) by A13, A14, FUNCT_1: 1;

            then x in (J . i) & (J . i) in ( rng J) by A1, FUNCT_1: 3, PARTFUN1:def 2;

            hence x in ( Union J) by TARSKI:def 4;

          end;

          assume x in ( Union J);

          then

          consider Y be set such that

           A15: x in Y & Y in ( rng J) by TARSKI:def 4;

          consider i be object such that

           A16: i in ( dom J) & Y = (J . i) by A15, FUNCT_1:def 3;

          reconsider i as Element of I by A16;

          reconsider Fi = (F . i) as Function;

          x in ( dom Fi) by A15, A16, PARTFUN1:def 2;

          then

          consider y be object such that

           A17: [x, y] in Fi by XTUPLE_0:def 12;

          Fi in ( rng F) by A2, FUNCT_1: 3;

          then [x, y] in UF by A17, TARSKI:def 4;

          hence x in ( dom UF) by XTUPLE_0:def 12;

        end;

        for x be object st x in ( Union J) holds (UF . x) is Group

        proof

          let x be object;

          assume x in ( Union J);

          then

          consider Y be set such that

           A18: x in Y & Y in ( rng J) by TARSKI:def 4;

          consider i be object such that

           A19: i in ( dom J) & Y = (J . i) by A18, FUNCT_1:def 3;

          reconsider i as Element of I by A19;

          reconsider Fi = (F . i) as Group-Family of (J . i);

          x in ( dom Fi) by A18, A19, PARTFUN1:def 2;

          then

          consider y be object such that

           A20: [x, y] in Fi by XTUPLE_0:def 12;

          

           A21: y = (Fi . x) by A20, FUNCT_1: 1;

          Fi in ( rng F) by A2, FUNCT_1: 3;

          then [x, y] in UF by A20, TARSKI:def 4;

          then y = (UF . x) by FUNCT_1: 1;

          hence thesis by A18, A19, A21, GROUP_19: 1;

        end;

        hence thesis by A11, GROUP_19: 2, TARSKI: 2;

      end;

    end

    theorem :: GROUP_21:22

    

     Th19: for I be non empty set, J be disjoint_valued ManySortedSet of I, F be Group-Family of I, J, j be Element of I, i be object st i in (J . j) holds (( Union F) . i) = ((F . j) . i)

    proof

      let I be non empty set, J be disjoint_valued ManySortedSet of I, F be Group-Family of I, J, j be Element of I, i be object;

      assume

       A1: i in (J . j);

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

      then

       A3: (J . j) c= ( Union J) by FUNCT_1: 3, ZFMISC_1: 74;

      ( dom ( Union F)) = ( Union J) by PARTFUN1:def 2;

      then [i, (( Union F) . i)] in ( Union F) by A1, A3, FUNCT_1: 1;

      then

      consider Y0 be set such that

       A4: [i, (( Union F) . i)] in Y0 & Y0 in ( rng F) by TARSKI:def 4;

      consider k be object such that

       A5: k in ( dom F) & Y0 = (F . k) by A4, FUNCT_1:def 3;

      reconsider k as Element of I by A5;

      reconsider Fk = (F . k) as Function;

      

       A6: ( dom Fk) = (J . k) by PARTFUN1:def 2;

      i in ( dom Fk) by A4, A5, XTUPLE_0:def 12;

      then ((J . k) /\ (J . j)) <> {} by A1, A6, XBOOLE_0:def 4;

      then j = k by PROB_2:def 2, XBOOLE_0:def 7;

      hence thesis by A4, A5, FUNCT_1: 1;

    end;

    definition

      let I be non empty set;

      let J be ManySortedSet of I;

      let F be multMagma-Family of I, J;

      :: GROUP_21:def6

      func prod_bundle F -> multMagma-Family of I means

      : Def6: for i be Element of I holds (it . i) = ( product (F . i));

      existence

      proof

        deffunc DF( object) = ( product (F . ( In ($1,I))));

        consider f be Function such that

         A1: ( dom f) = I & for i be Element of I holds (f . i) = DF(i) from FUNCT_1:sch 4;

        reconsider f as ManySortedSet of I by A1, PARTFUN1:def 2, RELAT_1:def 18;

        

         A2: for i be Element of I holds (f . i) = ( product (F . i))

        proof

          let i be Element of I;

          ( In (i,I)) = i;

          hence (f . i) = ( product (F . i)) by A1;

        end;

        for a be set st a in ( rng f) holds a is non empty multMagma

        proof

          let a be set;

          assume a in ( rng f);

          then

          consider i be object such that

           A3: i in ( dom f) & a = (f . i) by FUNCT_1:def 3;

          reconsider i as Element of I by A3;

          (f . i) = ( product (F . i)) by A2;

          hence thesis by A3;

        end;

        then

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

        take f;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let G1,G2 be multMagma-Family of I such that

         A4: for i be Element of I holds (G1 . i) = ( product (F . i)) and

         A5: for i be Element of I holds (G2 . i) = ( product (F . i));

        

         A6: ( dom G1) = I by PARTFUN1:def 2;

        for i be object st i in ( dom G1) holds (G1 . i) = (G2 . i)

        proof

          let i be object;

          assume i in ( dom G1);

          then

          reconsider i0 = i as Element of I;

          

          thus (G1 . i) = ( product (F . i0)) by A4

          .= (G2 . i) by A5;

        end;

        hence G1 = G2 by A6, PARTFUN1:def 2;

      end;

    end

    definition

      let I be non empty set;

      let J be ManySortedSet of I;

      let F be Group-Family of I, J;

      :: original: prod_bundle

      redefine

      func prod_bundle F -> Group-Family of I ;

      correctness

      proof

        set H = ( prod_bundle F);

        

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

        for i be object st i in I holds (H . i) is Group

        proof

          let i be object;

          assume i in I;

          then

          reconsider i as Element of I;

          (H . i) = ( product (F . i)) by Def6;

          hence thesis;

        end;

        hence thesis by A1, GROUP_19: 2;

      end;

    end

    definition

      let I be non empty set;

      let J be ManySortedSet of I;

      let F be Group-Family of I, J;

      :: GROUP_21:def7

      func sum_bundle F -> Group-Family of I means

      : Def7: for i be Element of I holds (it . i) = ( sum (F . i));

      existence

      proof

        deffunc DF( object) = ( sum (F . ( In ($1,I))));

        consider f be Function such that

         A1: ( dom f) = I & for i be Element of I holds (f . i) = DF(i) from FUNCT_1:sch 4;

        reconsider f as ManySortedSet of I by A1, PARTFUN1:def 2, RELAT_1:def 18;

        

         A2: for i be Element of I holds (f . i) = ( sum (F . i))

        proof

          let i be Element of I;

          ( In (i,I)) = i;

          hence (f . i) = ( sum (F . i)) by A1;

        end;

        for i be object st i in I holds (f . i) is Group

        proof

          let i be object;

          assume i in I;

          then

          reconsider i as Element of I;

          (f . i) = ( sum (F . i)) by A2;

          hence thesis;

        end;

        then f is Group-Family of I by A1, GROUP_19: 2;

        hence thesis by A2;

      end;

      uniqueness

      proof

        let G1,G2 be Group-Family of I such that

         A4: for i be Element of I holds (G1 . i) = ( sum (F . i)) and

         A5: for i be Element of I holds (G2 . i) = ( sum (F . i));

        

         A6: ( dom G1) = I by PARTFUN1:def 2;

        for i be object st i in ( dom G1) holds (G1 . i) = (G2 . i)

        proof

          let i be object;

          assume i in ( dom G1);

          then

          reconsider i0 = i as Element of I;

          

          thus (G1 . i) = ( sum (F . i0)) by A4

          .= (G2 . i) by A5;

        end;

        hence G1 = G2 by A6, PARTFUN1:def 2;

      end;

    end

    definition

      let I be non empty set;

      let J be ManySortedSet of I;

      let F be multMagma-Family of I, J;

      :: GROUP_21:def8

      func dprod F -> multMagma equals ( product ( prod_bundle F));

      correctness ;

    end

    registration

      let I be non empty set;

      let J be non-empty ManySortedSet of I;

      let F be multMagma-Family of I, J;

      cluster ( dprod F) -> non empty constituted-Functions;

      correctness ;

    end

    registration

      let I be non empty set;

      let J be non-empty ManySortedSet of I;

      let F be Group-Family of I, J;

      cluster ( dprod F) -> Group-like associative;

      coherence

      proof

        reconsider H = ( prod_bundle F) as Group-Family of I;

        ( dprod F) = ( product H);

        hence thesis;

      end;

    end

    definition

      let I be non empty set;

      let J be non-empty ManySortedSet of I;

      let F be Group-Family of I, J;

      :: GROUP_21:def9

      func dsum F -> Group equals ( sum ( sum_bundle F));

      correctness ;

    end

    registration

      let I be non empty set;

      let J be non-empty ManySortedSet of I;

      let F be Group-Family of I, J;

      cluster ( dsum F) -> non empty constituted-Functions;

      correctness ;

    end

    theorem :: GROUP_21:23

    

     Th20: for I be non empty set, F1,F2 be Group-Family of I st for i be Element of I holds (F1 . i) is Subgroup of (F2 . i) holds ( product F1) is Subgroup of ( product F2)

    proof

      let I be non empty set, F1,F2 be Group-Family of I;

      assume

       A1: for i be Element of I holds (F1 . i) is Subgroup of (F2 . i);

      

       A2: for x be object st x in ( [#] ( product F1)) holds x in ( [#] ( product F2))

      proof

        let x be object;

        assume x in ( [#] ( product F1));

        then

        reconsider x as Element of ( product F1);

        

         A3: ( dom x) = I by GROUP_19: 3;

        reconsider z = ( Carrier F2) as ManySortedSet of I;

        

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

        for i be object st i in I holds (x . i) in (z . i)

        proof

          let i be object;

          assume i in I;

          then

          reconsider i as Element of I;

          

           A5: (z . i) = ( [#] (F2 . i)) by PENCIL_3: 7;

          x in ( product F1);

          then

           A6: (x . i) in (F1 . i) by GROUP_19: 5;

          (F1 . i) is Subgroup of (F2 . i) by A1;

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

          hence thesis by A5, A6;

        end;

        then x in ( product z) by A3, A4, CARD_3:def 5;

        hence thesis by GROUP_7:def 2;

      end;

      then

       A7: ( [#] ( product F1)) c= ( [#] ( product F2));

      then [:( [#] ( product F1)), ( [#] ( product F1)):] c= [:( [#] ( product F2)), ( [#] ( product F2)):] by ZFMISC_1: 96;

      then

      reconsider f2 = (the multF of ( product F2) || ( [#] ( product F1))) as Function of [:( [#] ( product F1)), ( [#] ( product F1)):], ( [#] ( product F2)) by FUNCT_2: 32;

      reconsider f1 = the multF of ( product F1) as Function of [:( [#] ( product F1)), ( [#] ( product F1)):], ( [#] ( product F2)) by A7, FUNCT_2: 7;

      for x,y be set st x in ( [#] ( product F1)) & y in ( [#] ( product F1)) holds (f1 . (x,y)) = (f2 . (x,y))

      proof

        let x0,y0 be set;

        assume

         A8: x0 in ( [#] ( product F1)) & y0 in ( [#] ( product F1));

        then

        reconsider x1 = x0, y1 = y0 as Element of ( product F1);

        reconsider x2 = x0, y2 = y0 as Element of ( product F2) by A2, A8;

        

         A9: ( dom (x1 * y1)) = I by GROUP_19: 3;

        

         A10: for i be object st i in ( dom (x1 * y1)) holds ((x1 * y1) . i) = ((x2 * y2) . i)

        proof

          let i be object;

          assume i in ( dom (x1 * y1));

          then

          reconsider i as Element of I by GROUP_19: 3;

          x1 in ( product F1);

          then (x1 . i) in (F1 . i) by GROUP_19: 5;

          then

          reconsider x1i = (x1 . i) as Element of (F1 . i);

          x2 in ( product F2);

          then (x2 . i) in (F2 . i) by GROUP_19: 5;

          then

          reconsider x2i = (x2 . i) as Element of (F2 . i);

          y1 in ( product F1);

          then (y1 . i) in (F1 . i) by GROUP_19: 5;

          then

          reconsider y1i = (y1 . i) as Element of (F1 . i);

          y2 in ( product F2);

          then (y2 . i) in (F2 . i) by GROUP_19: 5;

          then

          reconsider y2i = (y2 . i) as Element of (F2 . i);

          

           A11: (F1 . i) is Subgroup of (F2 . i) by A1;

          ((x1 * y1) . i) = (x1i * y1i) by GROUP_7: 1

          .= (x2i * y2i) by A11, GROUP_2: 43

          .= ((x2 * y2) . i) by GROUP_7: 1;

          hence thesis;

        end;

        

         A12: (f2 . (x2,y2)) = ((the multF of ( product F2) | [:( [#] ( product F1)), ( [#] ( product F1)):]) . [x2, y2]) by BINOP_1:def 1

        .= (the multF of ( product F2) . [x2, y2]) by A8, FUNCT_1: 49, ZFMISC_1: 87

        .= (the multF of ( product F2) . (x2,y2)) by BINOP_1:def 1;

        

        thus (f1 . (x0,y0)) = (x1 * y1) by ALGSTR_0:def 18

        .= (x2 * y2) by A9, A10, GROUP_19: 3

        .= (f2 . (x0,y0)) by A12, ALGSTR_0:def 18;

      end;

      hence thesis by A7, BINOP_1:def 21, GROUP_2:def 5;

    end;

    theorem :: GROUP_21:24

    for I be non empty set, F1,F2 be Group-Family of I st for i be Element of I holds (F1 . i) is Subgroup of (F2 . i) holds ( sum F1) is Subgroup of ( sum F2)

    proof

      let I be non empty set, F1,F2 be Group-Family of I;

      assume

       A1: for i be Element of I holds (F1 . i) is Subgroup of (F2 . i);

      for x be object st x in ( [#] ( sum F1)) holds x in ( [#] ( sum F2))

      proof

        let x be object;

        assume

         A2: x in ( [#] ( sum F1));

        then x in ( sum F1);

        then x in ( product F1) by GROUP_2: 40;

        then

        reconsider x as Element of ( product F1);

        ( product F1) is Subgroup of ( product F2) by A1, Th20;

        then

        reconsider y = x as Element of ( product F2) by GROUP_2: 42;

        for i be object holds i in ( support (y,F2)) implies i in ( support (x,F1))

        proof

          let i be object;

          assume i in ( support (y,F2));

          then

          consider Z be Group such that

           A4: Z = (F2 . i) & (y . i) <> ( 1_ Z) & i in I by GROUP_19:def 1;

          reconsider i as Element of I by A4;

          (F1 . i) is Subgroup of (F2 . i) by A1;

          then (x . i) <> ( 1_ (F1 . i)) & i in I by A4, GROUP_2: 44;

          hence thesis by GROUP_19:def 1;

        end;

        then ( support (y,F2)) c= ( support (x,F1));

        then y in ( sum F2) by A2, GROUP_19: 8;

        hence thesis;

      end;

      then

       A5: ( [#] ( sum F1)) c= ( [#] ( sum F2));

      set mp1 = the multF of ( product F1);

      set mp2 = the multF of ( product F2);

      set ms1 = the multF of ( sum F1);

      set ms2 = the multF of ( sum F2);

      set cp1 = ( [#] ( product F1));

      set cp2 = ( [#] ( product F2));

      set cs1 = ( [#] ( sum F1));

      set cs2 = ( [#] ( sum F2));

      cs1 c= cp1 by GROUP_2:def 5;

      then

       A6: [:cs1, cs1:] c= [:cp1, cp1:] by ZFMISC_1: 96;

      

       A7: [:cs1, cs1:] c= [:cs2, cs2:] by A5, ZFMISC_1: 96;

      

       A8: ( product F1) is Subgroup of ( product F2) by A1, Th20;

      ms1 = (mp1 || cs1) by GROUP_2:def 5

      .= ((mp2 || cp1) || cs1) by A8, GROUP_2:def 5

      .= (mp2 || cs1) by A6, FUNCT_1: 51

      .= ((mp2 || cs2) || cs1) by A7, FUNCT_1: 51

      .= (ms2 || cs1) by GROUP_2:def 5;

      hence thesis by A5, GROUP_2:def 5;

    end;

    theorem :: GROUP_21:25

    

     Th22: for I be non empty set, J be non-empty ManySortedSet of I, F be Group-Family of I, J holds ( dsum F) is Subgroup of ( dprod F)

    proof

      let I be non empty set, J be non-empty ManySortedSet of I, F be Group-Family of I, J;

      for i be Element of I holds (( sum_bundle F) . i) is Subgroup of (( prod_bundle F) . i)

      proof

        let i be Element of I;

        (( sum_bundle F) . i) = ( sum (F . i)) by Def7;

        hence thesis by Def6;

      end;

      then ( product ( sum_bundle F)) is Subgroup of ( product ( prod_bundle F)) by Th20;

      hence thesis by GROUP_2: 56;

    end;

    definition

      let I be non empty set;

      let J be non-empty disjoint_valued ManySortedSet of I;

      let F be Group-Family of I, J;

      :: original: dsum

      redefine

      func dsum F -> Subgroup of ( dprod F) ;

      correctness by Th22;

    end

    definition

      let I be non empty set;

      let J be non-empty disjoint_valued ManySortedSet of I;

      let F be Group-Family of I, J;

      :: GROUP_21:def10

      func dprod2prod F -> Homomorphism of ( dprod F), ( product ( Union F)) means

      : Def10: for x be Element of ( dprod F), i be Element of I holds (x . i) = ((it . x) | (J . i));

      existence

      proof

        

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

        defpred P[ Function, Function] means for i be Element of I holds ($1 . i) = ($2 | (J . i));

        

         A2: for x be Element of ( dprod F) holds ex y be Element of ( product ( Union F)) st P[x, y]

        proof

          let x be Element of ( dprod F);

          

           A3: x in ( product ( prod_bundle F));

          

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

          

           A5: for i be Element of I holds (x . i) in ( product (F . i))

          proof

            let i be Element of I;

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

            hence (x . i) in ( product (F . i)) by Def6;

          end;

          set y = ( Union x);

          for z be object st z in y holds ex a,b be object st z = [a, b]

          proof

            let z be object;

            assume z in y;

            then

            consider Y be set such that

             A6: z in Y & Y in ( rng x) by TARSKI:def 4;

            consider i be object such that

             A7: i in ( dom x) & Y = (x . i) by A6, FUNCT_1:def 3;

            reconsider i as Element of I by A7, GROUP_19: 3;

            (x . i) in ( product (F . i)) by A5;

            hence thesis by A6, A7, RELAT_1:def 1;

          end;

          then y is Relation-like;

          then

          reconsider y as Relation;

          for a,b1,b2 be object st [a, b1] in y & [a, b2] in y holds b1 = b2

          proof

            let a,b1,b2 be object;

            assume

             A8: [a, b1] in y & [a, b2] in y;

            then

            consider Y1 be set such that

             A9: [a, b1] in Y1 & Y1 in ( rng x) by TARSKI:def 4;

            consider i1 be object such that

             A10: i1 in ( dom x) & Y1 = (x . i1) by A9, FUNCT_1:def 3;

            reconsider i1 as Element of I by A10, GROUP_19: 3;

            

             A11: (x . i1) in ( product (F . i1)) by A5;

            reconsider xi1 = (x . i1) as Function by A11;

            

             A12: a in ( dom xi1) by A9, A10, FUNCT_1: 1;

            

             A13: a in (J . i1) by A11, A12, GROUP_19: 3;

            consider Y2 be set such that

             A14: [a, b2] in Y2 & Y2 in ( rng x) by A8, TARSKI:def 4;

            consider i2 be object such that

             A15: i2 in ( dom x) & Y2 = (x . i2) by A14, FUNCT_1:def 3;

            reconsider i2 as Element of I by A15, GROUP_19: 3;

            

             A16: (x . i2) in ( product (F . i2)) by A5;

            reconsider xi2 = (x . i2) as Function by A16;

            

             A17: a in ( dom xi2) by A14, A15, FUNCT_1: 1;

            a in (J . i2) by A16, A17, GROUP_19: 3;

            then

             A18: ((J . i1) /\ (J . i2)) <> {} by A13, XBOOLE_0:def 4;

            i1 = i2 by A18, PROB_2:def 2, XBOOLE_0:def 7;

            hence b1 = b2 by A9, A10, A11, A14, A15, FUNCT_1:def 1;

          end;

          then y is Function-like;

          then

          reconsider y as Function;

          

           A19: for a be object holds a in ( dom y) iff a in ( Union J)

          proof

            let a be object;

            hereby

              assume a in ( dom y);

              then

              consider b be object such that

               A20: [a, b] in y by XTUPLE_0:def 12;

              consider Y be set such that

               A21: [a, b] in Y & Y in ( rng x) by A20, TARSKI:def 4;

              consider i be object such that

               A22: i in ( dom x) & Y = (x . i) by A21, FUNCT_1:def 3;

              reconsider i as Element of I by A22, GROUP_19: 3;

              

               A23: (x . i) in ( product (F . i)) by A5;

              then

              reconsider xi = (x . i) as Function;

              

               A24: a in ( dom xi) by A21, A22, FUNCT_1: 1;

              a in (J . i) & (J . i) in ( rng J) by A1, A23, A24, FUNCT_1: 3, GROUP_19: 3;

              hence a in ( Union J) by TARSKI:def 4;

            end;

            assume a in ( Union J);

            then

            consider Y be set such that

             A25: a in Y & Y in ( rng J) by TARSKI:def 4;

            consider i be object such that

             A26: i in ( dom J) & Y = (J . i) by A25, FUNCT_1:def 3;

            reconsider i as Element of I by A26;

            

             A27: (x . i) in ( product (F . i)) by A5;

            reconsider xi = (x . i) as Function by A27;

            a in ( dom xi) by A25, A26, A27, GROUP_19: 3;

            then

            consider b be object such that

             A28: [a, b] in xi by XTUPLE_0:def 12;

            xi in ( rng x) by A4, FUNCT_1: 3;

            then [a, b] in y by A28, TARSKI:def 4;

            hence a in ( dom y) by XTUPLE_0:def 12;

          end;

          then

           A29: ( dom y) = ( Union J) by TARSKI: 2;

          then

          reconsider y as ManySortedSet of ( Union J) by PARTFUN1:def 2, RELAT_1:def 18;

          reconsider z = ( Carrier ( Union F)) as ManySortedSet of ( Union J);

          

           A30: ( dom z) = ( Union J) by PARTFUN1:def 2;

          for i be object st i in ( Union J) holds (y . i) in (z . i)

          proof

            let i be object;

            assume i in ( Union J);

            then

            reconsider i as Element of ( Union J);

             [i, (y . i)] in y by A19, FUNCT_1: 1;

            then

            consider Yi be set such that

             A31: [i, (y . i)] in Yi & Yi in ( rng x) by TARSKI:def 4;

            consider j be object such that

             A32: j in ( dom x) & Yi = (x . j) by A31, FUNCT_1:def 3;

            reconsider j as Element of I by A32, GROUP_19: 3;

            

             A33: (x . j) in ( product (F . j)) by A5;

            reconsider xj = (x . j) as Function by A33;

            

             A34: i in ( dom xj) & (y . i) = (xj . i) by A31, A32, FUNCT_1: 1;

            

             A35: i in (J . j) by A33, A34, GROUP_19: 3;

            ( dom ( Union F)) = ( Union J) by PARTFUN1:def 2;

            then [i, (( Union F) . i)] in ( Union F) by FUNCT_1: 1;

            then

            consider Y0 be set such that

             A36: [i, (( Union F) . i)] in Y0 & Y0 in ( rng F) by TARSKI:def 4;

            consider k be object such that

             A37: k in ( dom F) & Y0 = (F . k) by A36, FUNCT_1:def 3;

            reconsider k as Element of I by A37;

            reconsider Fk = (F . k) as Function;

            

             A38: ( dom Fk) = (J . k) by PARTFUN1:def 2;

            i in ( dom Fk) by A36, A37, XTUPLE_0:def 12;

            then

             A39: ((J . k) /\ (J . j)) <> {} by A35, A38, XBOOLE_0:def 4;

            reconsider P = ((F . j) . i) as Group by A35, GROUP_19: 1;

            j = k by A39, PROB_2:def 2, XBOOLE_0:def 7;

            then

             A40: ( [#] P) = ( [#] (( Union F) . i)) by A36, A37, FUNCT_1: 1;

            (xj . i) in P by A33, A35, GROUP_19: 5;

            hence thesis by A34, A40, PENCIL_3: 7;

          end;

          then y in ( product z) by A29, A30, CARD_3:def 5;

          then

          reconsider y as Element of ( product ( Union F)) by GROUP_7:def 2;

          take y;

          thus for i be Element of I holds (x . i) = (y | (J . i))

          proof

            let i be Element of I;

            

             A41: (J . i) c= ( Union J) by A1, FUNCT_1: 3, ZFMISC_1: 74;

            then

             A42: ( dom (y | (J . i))) = (J . i) by A29, RELAT_1: 62;

            

             A43: (x . i) in ( product (F . i)) by A5;

            then

            reconsider xi = (x . i) as Function;

            for j be object st j in ( dom xi) holds (xi . j) = ((y | (J . i)) . j)

            proof

              let j be object;

              assume j in ( dom xi);

              then

               A44: j in (J . i) by A43, GROUP_19: 3;

              then

               A45: ((y | (J . i)) . j) = (y . j) by FUNCT_1: 49;

              j in ( dom (y | (J . i))) by A29, A41, A44, RELAT_1: 62;

              then j in (( dom y) /\ (J . i)) by RELAT_1: 61;

              then j in ( dom y) by XBOOLE_0:def 4;

              then [j, (y . j)] in y by FUNCT_1: 1;

              then

              consider Y0 be set such that

               A46: [j, (y . j)] in Y0 & Y0 in ( rng x) by TARSKI:def 4;

              consider k be object such that

               A47: k in ( dom x) & Y0 = (x . k) by A46, FUNCT_1:def 3;

              reconsider k as Element of I by A47, GROUP_19: 3;

              

               A48: (x . k) in ( product (F . k)) by A5;

              then

              reconsider xk = (x . k) as Function;

              

               A49: ( dom xk) = (J . k) by A48, GROUP_19: 3;

              j in ( dom xk) by A46, A47, XTUPLE_0:def 12;

              then

               A50: ((J . k) /\ (J . i)) <> {} by A44, A49, XBOOLE_0:def 4;

              i = k by A50, PROB_2:def 2, XBOOLE_0:def 7;

              hence thesis by A45, A46, A47, FUNCT_1: 1;

            end;

            hence thesis by A42, A43, FUNCT_1: 2, GROUP_19: 3;

          end;

        end;

        consider f be Function of ( dprod F), ( product ( Union F)) such that

         A51: for x be Element of ( dprod F) holds P[x, (f . x)] from FUNCT_2:sch 3( A2);

        for a,b be Element of ( dprod F) holds (f . (a * b)) = ((f . a) * (f . b))

        proof

          let a,b be Element of ( dprod F);

          reconsider fa = (f . a) as Element of ( product ( Union F));

          reconsider fb = (f . b) as Element of ( product ( Union F));

          set fafb = (fa * fb);

          reconsider fab = (f . (a * b)) as Element of ( product ( Union F));

          

           A52: a in ( product ( prod_bundle F)) & b in ( product ( prod_bundle F)) & (a * b) in ( product ( prod_bundle F));

          

           A53: for i be Element of I holds (a . i) in ( product (F . i)) & (b . i) in ( product (F . i)) & ((a * b) . i) in ( product (F . i))

          proof

            let i be Element of I;

            (a . i) in (( prod_bundle F) . i) & (b . i) in (( prod_bundle F) . i) & ((a * b) . i) in (( prod_bundle F) . i) by A52, GROUP_19: 5;

            hence thesis by Def6;

          end;

          

           A54: ( dom fab) = ( Union J) by GROUP_19: 3;

          for j be object st j in ( dom fab) holds (fab . j) = (fafb . j)

          proof

            let j be object;

            assume

             A55: j in ( dom fab);

            then

            consider Y be set such that

             A56: j in Y & Y in ( rng J) by A54, TARSKI:def 4;

            consider i be object such that

             A57: i in ( dom J) & Y = (J . i) by A56, FUNCT_1:def 3;

            reconsider i as Element of I by A57;

            

             A58: (a . i) = ((f . a) | (J . i)) by A51;

            

             A59: (b . i) = ((f . b) | (J . i)) by A51;

            (a . i) in ( product (F . i)) & (b . i) in ( product (F . i)) & ((a * b) . i) in ( product (F . i)) by A53;

            then

            reconsider ai = (a . i), bi = (b . i), abi = ((a * b) . i) as Element of ( product (F . i));

            reconsider P = ((F . i) . j) as Group by A56, A57, GROUP_19: 1;

            (ai . j) in P by A53, A56, A57, GROUP_19: 5;

            then

            reconsider aij = (ai . j) as Element of P;

            (bi . j) in P by A53, A56, A57, GROUP_19: 5;

            then

            reconsider bij = (bi . j) as Element of P;

            

             A60: aij = (fa . j) by A56, A57, A58, FUNCT_1: 49;

            then

            reconsider faj = (fa . j) as Element of P;

            bij = (fb . j) by A56, A57, A59, FUNCT_1: 49;

            then

            reconsider fbj = (fb . j) as Element of P;

            (( prod_bundle F) . i) = ( product (F . i)) by Def6;

            

            then

             A61: (abi . j) = ((ai * bi) . j) by GROUP_7: 1

            .= (aij * bij) by A56, A57, GROUP_7: 1;

            

             A62: j in ( Union J) by A55, GROUP_19: 3;

            ( dom ( Union F)) = ( Union J) by PARTFUN1:def 2;

            then [j, (( Union F) . j)] in ( Union F) by A62, FUNCT_1: 1;

            then

            consider Y0 be set such that

             A63: [j, (( Union F) . j)] in Y0 & Y0 in ( rng F) by TARSKI:def 4;

            consider k be object such that

             A64: k in ( dom F) & Y0 = (F . k) by A63, FUNCT_1:def 3;

            reconsider k as Element of I by A64;

            reconsider Fk = (F . k) as Function;

            j in ( dom Fk) by A63, A64, XTUPLE_0:def 12;

            then j in (J . k) by PARTFUN1:def 2;

            then

             A65: ((J . k) /\ (J . i)) <> {} by A56, A57, XBOOLE_0:def 4;

            i = k by A65, PROB_2:def 2, XBOOLE_0:def 7;

            then

             A66: (( Union F) . j) = ((F . i) . j) by A63, A64, FUNCT_1: 1;

            

            thus (fab . j) = (((f . (a * b)) | (J . i)) . j) by A56, A57, FUNCT_1: 49

            .= (aij * bij) by A51, A61

            .= (faj * fbj) by A56, A57, A59, A60, FUNCT_1: 49

            .= (fafb . j) by A62, A66, GROUP_7: 1;

          end;

          hence thesis by A54, GROUP_19: 3;

        end;

        then

        reconsider f as Homomorphism of ( dprod F), ( product ( Union F)) by GROUP_6:def 6;

        take f;

        thus thesis by A51;

      end;

      uniqueness

      proof

        let H1,H2 be Homomorphism of ( dprod F), ( product ( Union F)) such that

         A67: for x be Element of ( dprod F), i be Element of I holds (x . i) = ((H1 . x) | (J . i)) and

         A68: for x be Element of ( dprod F), i be Element of I holds (x . i) = ((H2 . x) | (J . i));

        for x be Element of ( dprod F) holds (H1 . x) = (H2 . x)

        proof

          let x be Element of ( dprod F);

          

           A69: x in ( product ( prod_bundle F));

          

           A70: for i be Element of I holds (x . i) in ( product (F . i))

          proof

            let i be Element of I;

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

            hence (x . i) in ( product (F . i)) by Def6;

          end;

          reconsider H1x = (H1 . x), H2x = (H2 . x) as Function;

          

           A71: ( dom H1x) = ( Union J) by GROUP_19: 3;

          for j be object st j in ( dom H1x) holds (H1x . j) = (H2x . j)

          proof

            let j be object;

            assume j in ( dom H1x);

            then

            consider Y be set such that

             A72: j in Y & Y in ( rng J) by A71, TARSKI:def 4;

            consider i be object such that

             A73: i in ( dom J) & Y = (J . i) by A72, FUNCT_1:def 3;

            reconsider i as Element of I by A73;

            (x . i) in ( product (F . i)) by A70;

            then

            reconsider xi = (x . i) as Function;

            

            thus (H1x . j) = ((H1x | (J . i)) . j) by A72, A73, FUNCT_1: 49

            .= (xi . j) by A67

            .= ((H2x | (J . i)) . j) by A68

            .= (H2x . j) by A72, A73, FUNCT_1: 49;

          end;

          hence thesis by A71, GROUP_19: 3;

        end;

        hence H1 = H2 by FUNCT_2: 63;

      end;

    end

    theorem :: GROUP_21:26

    

     Th23: for I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I, J, y be Element of ( product ( Union F)), i be Element of I holds (y | (J . i)) in ( product (F . i))

    proof

      let I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I, J, y be Element of ( product ( Union F)), i be Element of I;

      set x = (y | (J . i));

      

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

      

       A2: ( dom ( Union F)) = ( Union J) by PARTFUN1:def 2;

      

       A3: ( dom y) = ( Union J) by GROUP_19: 3;

      

       A4: (J . i) c= ( Union J) by A1, FUNCT_1: 3, ZFMISC_1: 74;

      then

       A5: ( dom x) = (J . i) by A3, RELAT_1: 62;

      set z = ( Carrier (F . i));

      

       A6: ( dom z) = (J . i) by PARTFUN1:def 2;

      for j be object st j in (J . i) holds (x . j) in (z . j)

      proof

        let j be object;

        assume j in (J . i);

        then

        reconsider j as Element of (J . i);

        reconsider j1 = j as Element of ( Union J) by A4;

        reconsider D = ( Union F) as Group-Family of ( Union J);

        y in ( product ( Union F));

        then

         A8: (y . j1) in (D . j1) by GROUP_19: 5;

        

         A9: (x . j) = (y . j) by FUNCT_1: 49;

         [j, (( Union F) . j)] in ( Union F) by A2, A4, FUNCT_1: 1;

        then

        consider Y0 be set such that

         A10: [j, (( Union F) . j)] in Y0 & Y0 in ( rng F) by TARSKI:def 4;

        consider k be object such that

         A11: k in ( dom F) & Y0 = (F . k) by A10, FUNCT_1:def 3;

        reconsider k as Element of I by A11;

        reconsider Fk = (F . k) as Function;

        

         A12: ( dom Fk) = (J . k) by PARTFUN1:def 2;

        j in ( dom Fk) by A10, A11, XTUPLE_0:def 12;

        then

         A13: ((J . k) /\ (J . i)) <> {} by A12, XBOOLE_0:def 4;

        

         A14: i = k by A13, PROB_2:def 2, XBOOLE_0:def 7;

        reconsider T = ((F . i) . j) as Group;

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

        hence thesis by A8, A9, A10, A11, A14, FUNCT_1: 1;

      end;

      then x in ( product z) by A5, A6, CARD_3:def 5;

      hence thesis by GROUP_7:def 2;

    end;

    

     Th24: for I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I, J holds ( dprod2prod F) is bijective

    proof

      let I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I, J;

      set f = ( dprod2prod F);

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

      proof

        let x1,x2 be object such that

         A1: x1 in ( dom f) and

         A2: x2 in ( dom f) and

         A3: (f . x1) = (f . x2);

        reconsider x1, x2 as Element of ( dprod F) by A1, A2;

        

         A4: ( dom x1) = I by GROUP_19: 3;

        for i be object st i in ( dom x1) holds (x1 . i) = (x2 . i)

        proof

          let i be object;

          assume i in ( dom x1);

          then

          reconsider i as Element of I by GROUP_19: 3;

          (x1 . i) = ((f . x2) | (J . i)) by A3, Def10

          .= (x2 . i) by Def10;

          hence thesis;

        end;

        then x1 = x2 by A4, GROUP_19: 3;

        hence thesis;

      end;

      hence f is one-to-one;

      for y be object st y in ( [#] ( product ( Union F))) holds ex x be object st x in ( [#] ( dprod F)) & y = (f . x)

      proof

        let y be object;

        assume y in ( [#] ( product ( Union F)));

        then

        reconsider y as Element of ( product ( Union F));

        deffunc P( object) = (y | (J . $1));

        consider x be Function such that

         A5: ( dom x) = I & for i be object st i in I holds (x . i) = P(i) from FUNCT_1:sch 3;

        reconsider x as ManySortedSet of I by A5, PARTFUN1:def 2, RELAT_1:def 18;

        set z = ( Carrier ( prod_bundle F));

        

         A6: ( dom z) = I by PARTFUN1:def 2;

        for i be object st i in I holds (x . i) in (z . i)

        proof

          let i be object;

          assume i in I;

          then

          reconsider i as Element of I;

          

           A7: (z . i) = ( [#] (( prod_bundle F) . i)) by PENCIL_3: 7

          .= ( [#] ( product (F . i))) by Def6;

          (y | (J . i)) in ( product (F . i)) by Th23;

          hence thesis by A5, A7;

        end;

        then x in ( product z) by A5, A6, CARD_3:def 5;

        then

        reconsider x as Element of ( dprod F) by GROUP_7:def 2;

        take x;

        thus x in ( [#] ( dprod F));

        

         A8: x in ( product ( prod_bundle F));

        

         A9: for i be Element of I holds (x . i) in ( product (F . i))

        proof

          let i be Element of I;

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

          hence thesis by Def6;

        end;

        reconsider H1x = y, H2x = (f . x) as Function;

        

         A10: ( dom H1x) = ( Union J) by GROUP_19: 3;

        for j be object st j in ( dom H1x) holds (H1x . j) = (H2x . j)

        proof

          let j be object;

          assume j in ( dom H1x);

          then

          consider Y be set such that

           A11: j in Y & Y in ( rng J) by A10, TARSKI:def 4;

          consider i be object such that

           A12: i in ( dom J) & Y = (J . i) by A11, FUNCT_1:def 3;

          reconsider i as Element of I by A12;

          (x . i) in ( product (F . i)) by A9;

          then

          reconsider xi = (x . i) as Function;

          

          thus (H1x . j) = ((H1x | (J . i)) . j) by A11, A12, FUNCT_1: 49

          .= (xi . j) by A5

          .= ((H2x | (J . i)) . j) by Def10

          .= (H2x . j) by A11, A12, FUNCT_1: 49;

        end;

        then y = (f . x) by A10, GROUP_19: 3;

        hence thesis;

      end;

      then ( rng f) = ( [#] ( product ( Union F))) by FUNCT_2: 10;

      hence f is onto by FUNCT_2:def 3;

    end;

    registration

      let I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I, J;

      cluster ( dprod2prod F) -> bijective;

      coherence by Th24;

    end

    definition

      let I be non empty set;

      let J be non-empty disjoint_valued ManySortedSet of I;

      let F be Group-Family of I, J;

      :: GROUP_21:def11

      func prod2dprod F -> Homomorphism of ( product ( Union F)), ( dprod F) equals (( dprod2prod F) " );

      correctness by GROUP_6: 62;

    end

    theorem :: GROUP_21:27

    

     Th25: for I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I, J holds for x be Element of ( product ( Union F)), i be Element of I holds (x | (J . i)) = ((( prod2dprod F) . x) . i)

    proof

      let I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I, J;

      set f1 = ( dprod2prod F);

      set f2 = ( prod2dprod F);

      let x be Element of ( product ( Union F)), i be Element of I;

      

       A2: ( rng f1) = the carrier of ( product ( Union F)) by FUNCT_2:def 3;

      reconsider y = (f2 . x) as Element of ( dprod F);

      ((( prod2dprod F) . x) . i) = ((f1 . y) | (J . i)) by Def10

      .= (x | (J . i)) by A2, FUNCT_1: 35;

      hence thesis;

    end;

    registration

      let I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I, J;

      cluster ( prod2dprod F) -> bijective;

      coherence by GROUP_6: 63;

    end

    theorem :: GROUP_21:28

    for I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I, J holds ( prod2dprod F) = (( dprod2prod F) " );

    definition

      let I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I, J, x be Function;

      :: GROUP_21:def12

      func supp_restr (x,F) -> disjoint_valued ManySortedSet of I means

      : Def12: for i be Element of I holds (it . i) = ( support ((x | (J . i)),(F . i)));

      existence

      proof

        deffunc P( object) = ( support ((x | (J . ( In ($1,I)))),(F . ( In ($1,I)))));

        consider sz be Function such that

         A1: ( dom sz) = I & for i be object st i in I holds (sz . i) = P(i) from FUNCT_1:sch 3;

        reconsider sz as ManySortedSet of I by A1, PARTFUN1:def 2, RELAT_1:def 18;

        

         A2: for i be Element of I holds (sz . i) = ( support ((x | (J . i)),(F . i)))

        proof

          let i be Element of I;

          ( In (i,I)) = i;

          hence thesis by A1;

        end;

        

         A3: J is disjoint_valued;

        for i,j be object st i <> j holds (sz . i) misses (sz . j)

        proof

          let i,j be object;

          assume

           A4: i <> j;

          per cases ;

            suppose not i in ( dom sz) or not j in ( dom sz);

            then (sz . i) = {} or (sz . j) = {} by FUNCT_1:def 2;

            then ((sz . i) /\ (sz . j)) = {} ;

            hence (sz . i) misses (sz . j) by XBOOLE_0:def 7;

          end;

            suppose i in ( dom sz) & j in ( dom sz);

            then

            reconsider i, j as Element of I;

            

             A6: (sz . i) = ( support ((x | (J . i)),(F . i))) & (sz . j) = ( support ((x | (J . j)),(F . j))) by A2;

            

             A7: ((sz . i) /\ (sz . j)) c= ((J . i) /\ (J . j)) by A6, XBOOLE_1: 27;

            ((J . i) /\ (J . j)) = {} by A3, A4, XBOOLE_0:def 7;

            then ((sz . i) /\ (sz . j)) = {} by A7;

            hence thesis by XBOOLE_0:def 7;

          end;

        end;

        then sz is disjoint_valued;

        then

        reconsider sz as disjoint_valued ManySortedSet of I;

        take sz;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let f1,f2 be disjoint_valued ManySortedSet of I such that

         A8: for i be Element of I holds (f1 . i) = ( support ((x | (J . i)),(F . i))) and

         A9: for i be Element of I holds (f2 . i) = ( support ((x | (J . i)),(F . i)));

        

         A10: ( dom f1) = I by PARTFUN1:def 2;

        for i be object st i in ( dom f1) holds (f1 . i) = (f2 . i)

        proof

          let i be object;

          assume i in ( dom f1);

          then

          reconsider i0 = i as Element of I;

          

          thus (f1 . i) = ( support ((x | (J . i)),(F . i0))) by A8

          .= (f2 . i) by A9;

        end;

        hence f1 = f2 by A10, PARTFUN1:def 2;

      end;

    end

    theorem :: GROUP_21:29

    

     Th28: for I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I, J, x be Function holds ( support (x,( Union F))) = ( Union ( supp_restr (x,F)))

    proof

      let I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I, J, x be Function;

      set y = ( supp_restr (x,F));

      

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

      

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

      for j be object holds j in ( support (x,( Union F))) iff j in ( Union y)

      proof

        let j be object;

        hereby

          assume j in ( support (x,( Union F)));

          then

          consider Z be Group such that

           A3: Z = (( Union F) . j) & (x . j) <> ( 1_ Z) & j in ( Union J) by GROUP_19:def 1;

          consider Y be set such that

           A4: j in Y & Y in ( rng J) by A3, TARSKI:def 4;

          consider i be object such that

           A5: i in ( dom J) & Y = (J . i) by A4, FUNCT_1:def 3;

          reconsider i as Element of I by A5;

          reconsider j0 = j as Element of (J . i) by A4, A5;

          ((F . i) . j0) = (( Union F) . j0) by Th19;

          then ((x | (J . i)) . j) <> ( 1_ ((F . i) . j0)) by A3, FUNCT_1: 49;

          then j in ( support ((x | (J . i)),(F . i))) by GROUP_19:def 1;

          then

           A6: j in (y . i) by Def12;

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

          hence j in ( Union y) by A6, TARSKI:def 4;

        end;

        assume j in ( Union y);

        then

        consider Y be set such that

         A7: j in Y & Y in ( rng y) by TARSKI:def 4;

        consider i be object such that

         A8: i in ( dom y) & Y = (y . i) by A7, FUNCT_1:def 3;

        reconsider i as Element of I by A8;

        

         A9: (y . i) = ( support ((x | (J . i)),(F . i))) by Def12;

        then

        consider Z be Group such that

         A10: Z = ((F . i) . j) & ((x | (J . i)) . j) <> ( 1_ Z) & j in (J . i) by A7, A8, GROUP_19:def 1;

        

         A11: ((x | (J . i)) . j) = (x . j) by A7, A8, A9, FUNCT_1: 49;

        (J . i) in ( rng J) by A1, FUNCT_1: 3;

        then

        reconsider j0 = j as Element of ( Union J) by A10, TARSKI:def 4;

        reconsider ZZ = (( Union F) . j0) as Group;

        ( 1_ Z) = ( 1_ ZZ) by A10, Th19;

        hence j in ( support (x,( Union F))) by A10, A11, GROUP_19:def 1;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: GROUP_21:30

    

     Th29: for I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I, J, x,y,z be Function st z in ( dprod F) & x = (( dprod2prod F) . z) holds (( supp_restr (x,F)) | ( support (z,( sum_bundle F)))) is non-empty disjoint_valued ManySortedSet of ( support (z,( sum_bundle F))) & ( support (x,( Union F))) = ( Union (( supp_restr (x,F)) | ( support (z,( sum_bundle F)))))

    proof

      let I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I, J, x,y,z be Function;

      assume that

       A1: z in ( dprod F) and

       A2: x = (( dprod2prod F) . z);

      set srx = ( supp_restr (x,F));

      set sz = ( support (z,( sum_bundle F)));

      set f = (srx | sz);

      

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

      ( dom f) = sz by A3, RELAT_1: 62;

      then

      reconsider f as ManySortedSet of sz by PARTFUN1:def 2;

      for s,t be object st s <> t holds (f . s) misses (f . t)

      proof

        let s,t be object;

        assume

         A4: s <> t;

        per cases ;

          suppose not s in ( dom f) or not t in ( dom f);

          then (f . s) = {} or (f . t) = {} by FUNCT_1:def 2;

          then ((f . s) /\ (f . t)) = {} ;

          hence thesis by XBOOLE_0:def 7;

        end;

          suppose s in ( dom f) & t in ( dom f);

          then

           A5: (f . s) = (srx . s) & (f . t) = (srx . t) by FUNCT_1: 47;

          srx is disjoint_valued;

          hence thesis by A4, A5;

        end;

      end;

      then

      reconsider f as disjoint_valued ManySortedSet of sz by PROB_2:def 2;

       not {} in ( rng f)

      proof

        assume {} in ( rng f);

        then

        consider i be object such that

         A6: i in ( dom f) & {} = (f . i) by FUNCT_1:def 3;

        i in sz by A6;

        then

        reconsider i as Element of I;

        

         A7: {} = (srx . i) by A6, FUNCT_1: 47;

        

         A8: ( support ((x | (J . i)),(F . i))) = {} by A7, Def12;

        ex Z be Group st Z = (( sum_bundle F) . i) & (z . i) <> ( 1_ Z) & i in I by A6, GROUP_19:def 1;

        then

         A9: (z . i) <> ( 1_ ( sum (F . i))) by Def7;

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

        then

         A10: (z . i) in ( product (F . i)) by Def6;

        then

        reconsider zi = (z . i) as Function;

        ex j be Element of (J . i) st (zi . j) <> ( 1_ ((F . i) . j))

        proof

          assume

           A11: for j be Element of (J . i) holds (zi . j) = ( 1_ ((F . i) . j));

          ( dom zi) = (J . i) by A10, GROUP_19: 3;

          then

          reconsider zi as ManySortedSet of (J . i) by PARTFUN1:def 2, RELAT_1:def 18;

          for k be set st k in (J . i) holds ex G be Group-like non empty multMagma st G = ((F . i) . k) & (zi . k) = ( 1_ G)

          proof

            let k be set;

            assume k in (J . i);

            then

            reconsider j = k as Element of (J . i);

            take G = ((F . i) . j);

            thus G = ((F . i) . k);

            thus (zi . k) = ( 1_ G) by A11;

          end;

          then zi = ( 1_ ( product (F . i))) by GROUP_7: 5;

          hence contradiction by A9, GROUP_2: 44;

        end;

        then

        consider j be Element of (J . i) such that

         A12: (zi . j) <> ( 1_ ((F . i) . j));

        j in ( support (zi,(F . i))) by A12, GROUP_19:def 1;

        hence contradiction by A1, A2, A8, Def10;

      end;

      then

      reconsider f as non-empty disjoint_valued ManySortedSet of sz by RELAT_1:def 9;

      f = (srx | sz);

      hence (srx | sz) is non-empty disjoint_valued ManySortedSet of sz;

      

       A13: ( support (x,( Union F))) = ( Union srx) by Th28;

      ( Union (srx | sz)) c= ( Union srx) by RELAT_1: 70, ZFMISC_1: 77;

      then

       A14: ( Union (srx | sz)) c= ( support (x,( Union F))) by A13;

      for k be object st k in ( support (x,( Union F))) holds k in ( Union (srx | sz))

      proof

        let k be object;

        assume k in ( support (x,( Union F)));

        then

        consider Y be set such that

         A15: k in Y & Y in ( rng srx) by A13, TARSKI:def 4;

        consider i be object such that

         A16: i in ( dom srx) & Y = (srx . i) by A15, FUNCT_1:def 3;

        reconsider i as Element of I by A16;

        k in ( support ((x | (J . i)),(F . i))) by A15, A16, Def12;

        then

        consider Z be Group such that

         A17: Z = ((F . i) . k) & ((x | (J . i)) . k) <> ( 1_ Z) & k in (J . i) by GROUP_19:def 1;

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

        then

         A18: (z . i) in ( product (F . i)) by Def6;

        then

        reconsider zi = (z . i) as Function;

        ( dom zi) = (J . i) by A18, GROUP_19: 3;

        then

        reconsider zi as ManySortedSet of (J . i) by PARTFUN1:def 2, RELAT_1:def 18;

        

         A19: (zi . k) <> ( 1_ Z) & k in (J . i) by A1, A2, A17, Def10;

        zi <> ( 1_ ( product (F . i))) by A17, A19, GROUP_7: 6;

        then (z . i) <> ( 1_ ( sum (F . i))) by GROUP_2: 44;

        then (z . i) <> ( 1_ (( sum_bundle F) . i)) by Def7;

        then i in ( support (z,( sum_bundle F))) by GROUP_19:def 1;

        then

         A20: i in ( dom (srx | sz)) by A16, RELAT_1: 57;

        then Y = ((srx | sz) . i) by A16, FUNCT_1: 47;

        then Y in ( rng (srx | sz)) by A20, FUNCT_1: 3;

        hence k in ( Union (srx | sz)) by A15, TARSKI:def 4;

      end;

      then ( support (x,( Union F))) c= ( Union (srx | sz));

      hence ( support (x,( Union F))) = ( Union (srx | sz)) by A14, XBOOLE_0:def 10;

    end;

    theorem :: GROUP_21:31

    

     Th31: for I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I, J, y be Function st y in ( sum ( Union F)) holds ex x be Function st y = (( dprod2prod F) . x) & x in ( dsum F)

    proof

      let I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I, J, y be Function;

      

       A1: ( [#] ( sum ( Union F))) c= ( [#] ( product ( Union F))) by GROUP_2:def 5;

      assume

       A2: y in ( sum ( Union F));

      then

      reconsider y as Element of ( product ( Union F)) by A1;

      

       A3: y in ( product ( Union F)) & ( support (y,( Union F))) is finite by A2;

      ( rng ( dprod2prod F)) = ( [#] ( product ( Union F))) by FUNCT_2:def 3;

      then

      consider x be Element of ( [#] ( dprod F)) such that

       A4: y = (( dprod2prod F) . x) by FUNCT_2: 113;

      reconsider x as Function;

      take x;

      

       A5: x in ( dprod F);

      set sry = ( supp_restr (y,F));

      

       A6: ( support (y,( Union F))) = ( Union sry) by Th28;

      

       A7: for i be Element of I holds (x . i) in (( sum_bundle F) . i)

      proof

        let i be Element of I;

        i in I;

        then i in ( dom sry) by PARTFUN1:def 2;

        then

         A8: (sry . i) c= ( Union sry) by FUNCT_1: 3, ZFMISC_1: 74;

        

         A9: ( support ((y | (J . i)),(F . i))) is finite by A2, A6, A8, Def12;

        

         A10: (y | (J . i)) = (x . i) by A4, Def10;

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

        then (x . i) in ( product (F . i)) by Def6;

        then (x . i) in ( sum (F . i)) by A9, A10, GROUP_19: 8;

        hence thesis by Def7;

      end;

      set SBF = ( sum_bundle F);

      

       A11: ( dom x) = I by GROUP_19: 3;

      reconsider W = ( Carrier SBF) as ManySortedSet of I;

      

       A12: ( dom W) = I by PARTFUN1:def 2;

      for i be object st i in I holds (x . i) in (W . i)

      proof

        let i be object;

        assume i in I;

        then

        reconsider i as Element of I;

        

         A13: (W . i) = ( [#] (SBF . i)) by PENCIL_3: 7;

        (x . i) in (SBF . i) by A7;

        hence thesis by A13;

      end;

      then x in ( product W) by A11, A12, CARD_3:def 5;

      then

      reconsider x as Element of ( product ( sum_bundle F)) by GROUP_7:def 2;

      reconsider sry1 = (sry | ( support (x,( sum_bundle F)))) as non-empty disjoint_valued ManySortedSet of ( support (x,( sum_bundle F))) by A4, A5, Th29;

      ( Union sry1) is finite by A3, A4, A5, Th29;

      then ( dom sry1) is finite by Th30;

      then ( support (x,( sum_bundle F))) is finite by PARTFUN1:def 2;

      hence thesis by A4, GROUP_19: 8;

    end;

    theorem :: GROUP_21:32

    

     Th32: for I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I, J, x,y be Function st x in ( dsum F) & x in ( dsum F) holds (( dprod2prod F) . x) in ( sum ( Union F))

    proof

      let I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I, J, x,y be Function;

      assume

       A1: x in ( dsum F);

      then

       A2: x in ( dprod F) by GROUP_2: 40;

      then

      reconsider y = (( dprod2prod F) . x) as Element of ( product ( Union F)) by FUNCT_2: 5;

      deffunc P( object) = ( support ((y | (J . ( In ($1,I)))),(F . ( In ($1,I)))));

      set sry = ( supp_restr (y,F));

      reconsider sry1 = (sry | ( support (x,( sum_bundle F)))) as non-empty disjoint_valued ManySortedSet of ( support (x,( sum_bundle F))) by A2, Th29;

      for i be object st i in ( dom sry1) holds (sry1 . i) is finite

      proof

        let i be object;

        assume

         A3: i in ( dom sry1);

        then i in ( support (x,( sum_bundle F)));

        then

        reconsider i as Element of I;

        

         A4: (y | (J . i)) = (x . i) by A2, Def10;

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

        then

         A5: (x . i) in ( sum (F . i)) by Def7;

        then (x . i) in ( product (F . i)) by GROUP_2: 40;

        then

        reconsider zi = (x . i) as Element of ( product (F . i));

        (sry . i) = ( support ((y | (J . i)),(F . i))) by Def12;

        hence thesis by A3, A4, A5, FUNCT_1: 49;

      end;

      then ( Union sry1) is finite by A1, CARD_2: 88;

      then ( support (y,( Union F))) is finite by A2, Th29;

      hence thesis by GROUP_19: 8;

    end;

    theorem :: GROUP_21:33

    

     Th33: for I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I, J holds ( rng (( dprod2prod F) | ( dsum F))) = ( [#] ( sum ( Union F)))

    proof

      let I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I, J;

      for y be object holds y in ( rng (( dprod2prod F) | ( [#] ( dsum F)))) iff y in ( [#] ( sum ( Union F)))

      proof

        let y be object;

        

         A1: ( dom ( dprod2prod F)) = ( [#] ( dprod F)) by FUNCT_2:def 1;

        hereby

          assume y in ( rng (( dprod2prod F) | ( [#] ( dsum F))));

          then

          consider x be object such that

           A2: x in ( dom (( dprod2prod F) | ( [#] ( dsum F)))) & y = ((( dprod2prod F) | ( [#] ( dsum F))) . x) by FUNCT_1:def 3;

          x in (( dom ( dprod2prod F)) /\ ( [#] ( dsum F))) by A2, RELAT_1: 61;

          then

           A3: x in ( dom ( dprod2prod F)) & x in ( [#] ( dsum F)) by XBOOLE_0:def 4;

          reconsider x as Function by A2;

          x in ( dprod F) & x in ( dsum F) by A3;

          then (( dprod2prod F) . x) in ( sum ( Union F)) by Th32;

          hence y in ( [#] ( sum ( Union F))) by A2, FUNCT_1: 47;

        end;

        assume

         A4: y in ( [#] ( sum ( Union F)));

        then

        reconsider y0 = y as Element of ( sum ( Union F));

        y0 in ( [#] ( product ( Union F))) by GROUP_2:def 5, TARSKI:def 3;

        then

        reconsider y0 = y as Element of ( product ( Union F));

        y0 in ( sum ( Union F)) by A4;

        then

        consider x be Function such that

         A5: y0 = (( dprod2prod F) . x) and

         A6: x in ( dsum F) by Th31;

        

         A7: y = ((( dprod2prod F) | ( [#] ( dsum F))) . x) by A5, A6, FUNCT_1: 49;

        x in ( dom (( dprod2prod F) | ( [#] ( dsum F)))) by A1, A6, GROUP_2:def 5, RELAT_1: 62;

        hence y in ( rng (( dprod2prod F) | ( [#] ( dsum F)))) by A7, FUNCT_1: 3;

      end;

      hence thesis by TARSKI: 2;

    end;

    definition

      let I be non empty set;

      let J be non-empty disjoint_valued ManySortedSet of I;

      let F be Group-Family of I, J;

      :: GROUP_21:def13

      func dsum2sum F -> Homomorphism of ( dsum F), ( sum ( Union F)) equals (( dprod2prod F) | ( dsum F));

      correctness

      proof

        set f = ( dprod2prod F);

        set h = (f | ( dsum F));

        

         A1: ( [#] ( dsum F)) c= ( [#] ( dprod F)) by GROUP_2:def 5;

        reconsider h as Function of ( dsum F), ( product ( Union F));

        

         A2: ( [#] ( sum ( Union F))) c= ( [#] ( product ( Union F))) by GROUP_2:def 5;

        ( rng h) = ( [#] ( sum ( Union F))) by Th33;

        then

        reconsider h as Function of ( dsum F), ( sum ( Union F)) by FUNCT_2: 6;

        for a,b be Element of ( dsum F) holds (h . (a * b)) = ((h . a) * (h . b))

        proof

          let a,b be Element of ( dsum F);

          reconsider a0 = a, b0 = b as Element of ( dprod F) by A1;

          reconsider ha = (h . a), hb = (h . b) as Element of ( product ( Union F)) by A2;

          

           A3: ha = (f . a0) & hb = (f . b0) by FUNCT_1: 49;

          (h . (a * b)) = (f . (a * b)) by FUNCT_1: 49

          .= (f . (a0 * b0)) by GROUP_2: 43

          .= (ha * hb) by A3, GROUP_6:def 6

          .= ((h . a) * (h . b)) by GROUP_2: 43;

          hence thesis;

        end;

        hence thesis by GROUP_6:def 6;

      end;

    end

    

     Th34: for I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I, J holds ( dsum2sum F) is bijective

    proof

      let I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I, J;

      

       A1: ( dsum2sum F) is one-to-one by FUNCT_1: 52;

      ( rng ( dsum2sum F)) = ( [#] ( sum ( Union F))) by Th33;

      then ( dsum2sum F) is onto by FUNCT_2:def 3;

      hence thesis by A1;

    end;

    registration

      let I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I, J;

      cluster ( dsum2sum F) -> bijective;

      coherence by Th34;

    end

    definition

      let I be non empty set;

      let J be non-empty disjoint_valued ManySortedSet of I;

      let F be Group-Family of I, J;

      :: GROUP_21:def14

      func sum2dsum F -> Homomorphism of ( sum ( Union F)), ( dsum F) equals (( dsum2sum F) " );

      correctness by GROUP_6: 62;

    end

    theorem :: GROUP_21:34

    

     Th36: for I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I, J holds ( sum2dsum F) = (( prod2dprod F) | ( sum ( Union F)))

    proof

      let I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I, J;

      ( dsum2sum F) is bijective;

      then ( rng (( dprod2prod F) | ( dsum F))) = ( [#] ( sum ( Union F))) by FUNCT_2:def 3;

      hence thesis by Th35;

    end;

    registration

      let I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I, J;

      cluster ( sum2dsum F) -> bijective;

      coherence by GROUP_6: 63;

    end

    theorem :: GROUP_21:35

    for I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, F be Group-Family of I, J holds ( dsum2sum F) = (( sum2dsum F) " ) by FUNCT_1: 43;

    definition

      let I be non empty set;

      let G be Group;

      let F be internal DirectSumComponents of G, I;

      :: GROUP_21:def15

      func InterHom F -> Homomorphism of ( sum F), G means

      : Def15: it is bijective & for x be finite-support Function of I, G st x in ( sum F) holds (it . x) = ( Product x);

      existence by GROUP_19:def 9;

      uniqueness

      proof

        let h1,h2 be Homomorphism of ( sum F), G such that

         A1: h1 is bijective & for x be finite-support Function of I, G st x in ( sum F) holds (h1 . x) = ( Product x) and

         A2: h2 is bijective & for x be finite-support Function of I, G st x in ( sum F) holds (h2 . x) = ( Product x);

        

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

        for x be Element of ( sum F) holds (h1 . x) = (h2 . x)

        proof

          let x be Element of ( sum F);

          

           A4: x in ( sum F);

          then

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

          

          thus (h1 . x) = ( Product x0) by A1, A4

          .= (h2 . x) by A2, A4;

        end;

        hence h1 = h2 by FUNCT_2: 63;

      end;

    end

    definition

      let I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, G be Group, M be DirectSumComponents of G, I, N be Group-Family of I, J, h be ManySortedSet of I;

      assume

       A2: for i be Element of I holds ex hi be Homomorphism of (( sum_bundle N) . i), (M . i) st hi = (h . i) & hi is bijective;

      :: GROUP_21:def16

      func ProductHom (G,M,N,h) -> Homomorphism of ( dsum N), ( sum M) means

      : Def16: it = ( SumMap (( sum_bundle N),M,h)) & it is bijective;

      existence

      proof

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

        hence thesis by A2, GROUP_19: 41;

      end;

      uniqueness ;

    end

    theorem :: GROUP_21:36

    

     Th39: for I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, G be Group, M be DirectSumComponents of G, I, N be Group-Family of I, J st for i be Element of I holds (N . i) is DirectSumComponents of (M . i), (J . i) holds ( Union N) is DirectSumComponents of G, ( Union J)

    proof

      let I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, G be Group, M be DirectSumComponents of G, I, N be Group-Family of I, J;

      assume

       A1: for i be Element of I holds (N . i) is DirectSumComponents of (M . i), (J . i);

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

       A2: fM2G is bijective by GROUP_19:def 8;

      deffunc P( object) = ( [#] ( sum (N . ( In ($1,I)))));

      consider DS be Function such that

       A3: ( dom DS) = I & for i be object st i in I holds (DS . i) = P(i) from FUNCT_1:sch 3;

      reconsider DS as ManySortedSet of I by A3, PARTFUN1:def 2, RELAT_1:def 18;

      deffunc Q( object) = ( [#] (M . ( In ($1,I))));

      consider RS be Function such that

       A4: ( dom RS) = I & for i be object st i in I holds (RS . i) = Q(i) from FUNCT_1:sch 3;

      reconsider RS as ManySortedSet of I by A4, PARTFUN1:def 2, RELAT_1:def 18;

      defpred R[ object, object] means ex fi be Homomorphism of ( sum (N . ( In ($1,I)))), (M . ( In ($1,I))) st fi = $2 & fi is bijective;

      

       A5: for i be Element of I holds ex y be Element of ( PFuncs (( Union DS),( Union RS))) st R[i, y]

      proof

        let i be Element of I;

        (N . i) is DirectSumComponents of (M . i), (J . i) by A1;

        then

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

         A6: h is bijective by GROUP_19:def 8;

        

         A7: ( In (i,I)) = i;

        (DS . i) = ( [#] ( sum (N . i))) & (RS . i) = ( [#] (M . i)) by A3, A4, A7;

        then ( [#] ( sum (N . i))) c= ( Union DS) & ( [#] (M . i)) c= ( Union RS) by A3, A4, FUNCT_1: 3, ZFMISC_1: 74;

        then ( dom h) c= ( Union DS) & ( rng h) c= ( Union RS);

        then

        reconsider y = h as Element of ( PFuncs (( Union DS),( Union RS))) by PARTFUN1:def 3;

        take y;

        thus thesis by A6;

      end;

      consider fBN2M be Function of I, ( PFuncs (( Union DS),( Union RS))) such that

       A9: for i be Element of I holds R[i, (fBN2M . i)] from FUNCT_2:sch 3( A5);

      reconsider fBN2M as ManySortedSet of I;

      set fDN2M = ( ProductHom (G,M,N,fBN2M));

      for i be Element of I holds ex hi be Homomorphism of (( sum_bundle N) . i), (M . i) st hi = (fBN2M . i) & hi is bijective

      proof

        let i be Element of I;

        consider fi be Homomorphism of ( sum (N . ( In (i,I)))), (M . ( In (i,I))) such that

         A11: fi = (fBN2M . i) & fi is bijective by A9;

        ( sum (N . i)) = (( sum_bundle N) . i) by Def7;

        then

        reconsider fi as Homomorphism of (( sum_bundle N) . i), (M . i);

        take fi;

        thus fi = (fBN2M . i) & fi is bijective by A11;

      end;

      then

       A12: fDN2M is bijective by Def16;

      reconsider h = ((fM2G * fDN2M) * ( sum2dsum N)) as Homomorphism of ( sum ( Union N)), G;

      take h;

      (fM2G * fDN2M) is one-to-one onto by A2, A12, FUNCT_2: 27;

      then h is one-to-one onto by FUNCT_2: 27;

      hence thesis;

    end;

    theorem :: GROUP_21:37

    

     Th40: for I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, G be Group, M be internal DirectSumComponents of G, I, N be Group-Family of I, J st for i be Element of I holds (N . i) is internal DirectSumComponents of (M . i), (J . i) holds ( Union N) is internal DirectSumComponents of G, ( Union J)

    proof

      let I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, G be Group, M be internal DirectSumComponents of G, I, N be Group-Family of I, J;

      assume

       A1: for i be Element of I holds (N . i) is internal DirectSumComponents of (M . i), (J . i);

      

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

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

       A3: fMtoG is bijective and

       A4: for x be finite-support Function of I, G st x in ( sum M) holds (fMtoG . x) = ( Product x) by GROUP_19:def 9;

      defpred Q[ object, object] means ex Ni be internal DirectSumComponents of (M . ( In ($1,I))), (J . ( In ($1,I))) st Ni = (N . $1) & $2 = ( InterHom Ni);

      

       A5: for i,f1,f2 be object st i in I & Q[i, f1] & Q[i, f2] holds f1 = f2;

      

       A6: for x be object st x in I holds ex y be object st Q[x, y]

      proof

        let x be object;

        assume x in I;

        then

        reconsider i = x as Element of I;

        reconsider Ni = (N . i) as internal DirectSumComponents of (M . i), (J . i) by A1;

        take y = ( InterHom Ni);

        thus thesis;

      end;

      consider fBNtoM be Function such that

       A8: ( dom fBNtoM) = I & for i be object st i in I holds Q[i, (fBNtoM . i)] from FUNCT_1:sch 2( A5, A6);

      reconsider fBNtoM as ManySortedSet of I by A8, PARTFUN1:def 2, RELAT_1:def 18;

      set fDNtoM = ( ProductHom (G,M,N,fBNtoM));

      

       A9: for i be Element of I holds ex hi be Homomorphism of (( sum_bundle N) . i), (M . i) st hi = (fBNtoM . i) & hi is bijective & for x be finite-support Function of (J . i), (M . i) st x in (( sum_bundle N) . i) holds (hi . x) = ( Product x)

      proof

        let i be Element of I;

        consider Ni be internal DirectSumComponents of (M . ( In (i,I))), (J . ( In (i,I))) such that

         A11: Ni = (N . i) & (fBNtoM . i) = ( InterHom Ni) by A8;

        

         A12: ( InterHom Ni) is bijective & for x be finite-support Function of (J . i), (M . i) st x in ( sum Ni) holds (( InterHom Ni) . x) = ( Product x) by Def15;

        

         A13: ( sum (N . ( In (i,I)))) = (( sum_bundle N) . i) by Def7;

        then

        reconsider hi = ( InterHom Ni) as Homomorphism of (( sum_bundle N) . i), (M . i) by A11;

        take hi;

        thus hi = (fBNtoM . i) by A11;

        thus hi is bijective by A12;

        thus for x be finite-support Function of (J . i), (M . i) st x in (( sum_bundle N) . i) holds (hi . x) = ( Product x) by A11, A13, Def15;

      end;

      

       A14: for i be Element of I holds ex hi be Homomorphism of (( sum_bundle N) . i), (M . i) st hi = (fBNtoM . i) & hi is bijective

      proof

        let i be Element of I;

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

         A15: hi = (fBNtoM . i) & hi is bijective & for x be finite-support Function of (J . i), (M . i) st x in (( sum_bundle N) . i) holds (hi . x) = ( Product x) by A9;

        take hi;

        thus thesis by A15;

      end;

      

       A16: fDNtoM is bijective by A14, Def16;

      reconsider h = ((fMtoG * fDNtoM) * ( sum2dsum N)) as Homomorphism of ( sum ( Union N)), G;

      (fMtoG * fDNtoM) is one-to-one onto by A3, A16, FUNCT_2: 27;

      then

       A18: h is one-to-one onto by FUNCT_2: 27;

      

       A19: for i be Element of I holds (N . i) is DirectSumComponents of (M . i), (J . i) by A1;

      reconsider UJ = ( Union J) as non empty set;

      reconsider UN = ( Union N) as DirectSumComponents of G, UJ by A19, Th39;

      

       A20: for i be Element of I holds (M . i) is Subgroup of G by GROUP_19:def 9;

      

       A21: for j be object st j in UJ holds (UN . j) is Subgroup of G

      proof

        let j be object;

        assume j in UJ;

        then

        consider Y be set such that

         A22: j in Y & Y in ( rng J) by TARSKI:def 4;

        consider i be object such that

         A23: i in ( dom J) & Y = (J . i) by A22, FUNCT_1:def 3;

        reconsider i as Element of I by A23;

        

         A24: (UN . j) = ((N . i) . j) by A22, A23, Th19;

        (N . i) is internal DirectSumComponents of (M . i), (J . i) by A1;

        then

         A25: ((N . i) . j) is Subgroup of (M . i) by A22, A23, GROUP_19:def 9;

        (M . i) is Subgroup of G by GROUP_19:def 9;

        hence (UN . j) is Subgroup of G by A24, A25, GROUP_2: 56;

      end;

      then

       A26: for j be Element of UJ holds (UN . j) is Subgroup of G;

      reconsider UN as Subgroup-Family of UJ, G by A21, GROUP_20:def 1;

      for x be finite-support Function of UJ, G st x in ( sum UN) holds (h . x) = ( Product x)

      proof

        let x be finite-support Function of UJ, G;

        assume

         A27: x in ( sum UN);

        for j be Element of UJ, g be Element of (UN . j) holds (h . (( 1ProdHom (UN,j)) . g)) = g

        proof

          let j be Element of UJ, g be Element of (UN . j);

          (UN . j) is Subgroup of G by A21;

          then

           A28: g is Element of G by GROUP_2: 42;

          

           A29: (( 1ProdHom (UN,j)) . g) in ( ProjGroup (UN,j));

          then

           A30: (( 1ProdHom (UN,j)) . g) in ( sum UN) by GROUP_2: 40;

          then

           A31: (( 1ProdHom (UN,j)) . g) in ( dom ( sum2dsum N)) by FUNCT_2:def 1;

          then

           A32: (h . (( 1ProdHom (UN,j)) . g)) = ((fMtoG * fDNtoM) . (( sum2dsum N) . (( 1ProdHom (UN,j)) . g))) by FUNCT_1: 13;

          

           A33: (( sum2dsum N) . (( 1ProdHom (UN,j)) . g)) in ( [#] ( dsum N)) by A30, FUNCT_2: 5;

          

           A34: ((fMtoG * fDNtoM) . (( sum2dsum N) . (( 1ProdHom (UN,j)) . g))) = (fMtoG . (fDNtoM . (( sum2dsum N) . (( 1ProdHom (UN,j)) . g)))) by A30, FUNCT_2: 5, FUNCT_2: 15;

          

           A35: (fDNtoM . (( sum2dsum N) . (( 1ProdHom (UN,j)) . g))) in ( sum M) by A33, FUNCT_2: 5;

          for i be object st i in I holds (M . i) is Subgroup of G by GROUP_19:def 9;

          then

          reconsider z = (fDNtoM . (( sum2dsum N) . (( 1ProdHom (UN,j)) . g))) as finite-support Function of I, G by A35, GROUP_19: 10;

          

           A36: ((fMtoG * fDNtoM) . (( sum2dsum N) . (( 1ProdHom (UN,j)) . g))) = ( Product z) by A4, A34, A35;

          consider Y be set such that

           A37: j in Y & Y in ( rng J) by TARSKI:def 4;

          consider k be object such that

           A38: k in ( dom J) & Y = (J . k) by A37, FUNCT_1:def 3;

          reconsider k as Element of I by A38;

          

           A39: (UN . j) = ((N . k) . j) by A37, A38, Th19;

          (N . k) is internal DirectSumComponents of (M . k), (J . k) by A1;

          then

          reconsider K = ((N . k) . j) as Subgroup of (M . k) by A37, A38, GROUP_19:def 9;

          

           A41: g in K by A39;

          

           A42: ( sum2dsum N) = (( prod2dprod N) | ( sum ( Union N))) by Th36;

          

           A43: (( sum2dsum N) . (( 1ProdHom (UN,j)) . g)) = (( prod2dprod N) . (( 1ProdHom (UN,j)) . g)) by A31, A42, FUNCT_1: 47;

          (( 1ProdHom (UN,j)) . g) in ( product UN) by A29, GROUP_2: 40;

          then

          reconsider y = (( 1ProdHom (UN,j)) . g) as Element of ( product ( Union N));

          reconsider t = (( sum2dsum N) . (( 1ProdHom (UN,j)) . g)) as Element of ( dsum N) by A30, FUNCT_2: 5;

          

           A44: for i be Element of I holds (fBNtoM . i) is Homomorphism of (( sum_bundle N) . i), (M . i)

          proof

            let i be Element of I;

            ex hi be Homomorphism of (( sum_bundle N) . i), (M . i) st hi = (fBNtoM . i) & hi is bijective by A14;

            hence thesis;

          end;

          consider hk be Homomorphism of (( sum_bundle N) . k), (M . k) such that

           A45: hk = (fBNtoM . k) & hk is bijective & for x be finite-support Function of (J . k), (M . k) st x in (( sum_bundle N) . k) holds (hk . x) = ( Product x) by A9;

          

           A46: hk is one-to-one & ( rng hk) = ( [#] (M . k)) by A45, FUNCT_2:def 3;

          then

           A47: (hk " ) is Function of ( [#] (M . k)), ( [#] (( sum_bundle N) . k)) by FUNCT_2: 25;

          

           A48: g in (M . k) by A41, GROUP_2: 40;

          then ((hk " ) . g) is Element of (( sum_bundle N) . k) by A47, FUNCT_2: 5;

          then (( SumMap (( sum_bundle N),M,fBNtoM)) . (( 1ProdHom (( sum_bundle N),k)) . ((hk " ) . g))) = (( 1ProdHom (M,k)) . (hk . ((hk " ) . g))) by A8, A44, A45, GROUP_19: 42;

          

          then

           A49: (fDNtoM . (( 1ProdHom (( sum_bundle N),k)) . ((hk " ) . g))) = (( 1ProdHom (M,k)) . (hk . ((hk " ) . g))) by A14, Def16

          .= (( 1ProdHom (M,k)) . g) by A46, A48, FUNCT_1: 35;

          reconsider hkg = ((hk " ) . g) as Element of (( sum_bundle N) . k) by A47, A48, FUNCT_2: 5;

          

           A50: (( 1ProdHom (( sum_bundle N),k)) . hkg) in ( ProjGroup (( sum_bundle N),k));

          then

           A51: (( 1ProdHom (( sum_bundle N),k)) . hkg) in ( product ( sum_bundle N)) by GROUP_2: 40;

          then

          reconsider p = (( 1ProdHom (( sum_bundle N),k)) . hkg) as Function;

          

           A52: t in ( sum ( sum_bundle N));

          then t in ( product ( sum_bundle N)) by GROUP_2: 40;

          then

           A53: ( dom t) = I by GROUP_19: 3;

          for i be object st i in ( dom p) holds (p . i) = (t . i)

          proof

            let i0 be object;

            assume i0 in ( dom p);

            then

            reconsider i = i0 as Element of I by A51, GROUP_19: 3;

            reconsider yi = (y | (J . i)) as Function;

            (p . i) in (( sum_bundle N) . i) by A50, GROUP_2: 40, GROUP_19: 5;

            then

             A54: (p . i) in ( sum (N . i)) by Def7;

            then

             A55: (p . i) in ( product (N . i)) by GROUP_2: 40;

            reconsider xi = (p . i) as Function by A54;

            (y | (J . i)) = (t . i) by A43, Th25;

            then yi in (( sum_bundle N) . i) by A52, GROUP_2: 40, GROUP_19: 5;

            then yi in ( sum (N . i)) by Def7;

            then

             A56: yi in ( product (N . i)) by GROUP_2: 40;

            then

             A57: ( dom yi) = (J . i) by GROUP_19: 3;

            

             A58: p = (( 1_ ( product ( sum_bundle N))) +* (k,hkg)) by GROUP_12:def 3;

            

             A59: y = (( 1_ ( product UN)) +* (j,g)) by GROUP_12:def 3;

            per cases ;

              suppose

               A60: i <> k;

              then xi = ( 1_ (( sum_bundle N) . i)) by A58, GROUP_12: 1;

              then

               A61: xi = ( 1_ ( sum (N . i))) by Def7;

              for n be object st n in ( dom yi) holds (yi . n) = (xi . n)

              proof

                let n0 be object;

                assume

                 A62: n0 in ( dom yi);

                then

                reconsider n = n0 as Element of (J . i) by A56, GROUP_19: 3;

                ((J . i) /\ (J . k)) = {} by A60, PROB_2:def 2, XBOOLE_0:def 7;

                then

                 A63: j <> n by A37, A38, XBOOLE_0:def 4;

                (J . i) c= ( Union J) by A2, FUNCT_1: 3, ZFMISC_1: 74;

                then

                reconsider n1 = n as Element of UJ;

                

                thus (yi . n0) = (y . n) by A62, FUNCT_1: 47

                .= ( 1_ (UN . n1)) by A59, A63, GROUP_12: 1

                .= ( 1_ ((N . i) . n)) by Th19

                .= (( 1_ ( product (N . i))) . n) by GROUP_7: 6

                .= (xi . n0) by A61, GROUP_2: 44;

              end;

              then yi = xi by A55, A57, GROUP_19: 3;

              hence thesis by A43, Th25;

            end;

              suppose

               A65: i = k;

              then

               A66: xi = hkg by A58, GROUP_12: 1;

              for n be object st n in ( dom yi) holds (yi . n) = (xi . n)

              proof

                let n0 be object;

                assume

                 A67: n0 in ( dom yi);

                then

                reconsider n = n0 as Element of (J . i) by A56, GROUP_19: 3;

                (J . i) c= ( Union J) by A2, FUNCT_1: 3, ZFMISC_1: 74;

                then

                reconsider n1 = n as Element of UJ;

                

                 A69: g is Element of K by A37, A38, Th19;

                ( 1_ ( sum (N . k))) in ( sum (N . k));

                then

                 A70: (( 1_ ( sum (N . k))) +* (j,g)) in ( sum (N . k)) by A37, A38, A69, GROUP_19: 25;

                then

                 A71: (( 1_ ( sum (N . k))) +* (j,g)) in (( sum_bundle N) . k) by Def7;

                then (( 1_ ( sum (N . k))) +* (j,g)) in ( dom hk) by FUNCT_2:def 1;

                then

                 A72: (( 1_ ( product (N . k))) +* (j,g)) in ( dom hk) by GROUP_2: 44;

                

                 A73: (N . k) is internal DirectSumComponents of (M . k), (J . k) by A1;

                then

                 A74: for j be Element of (J . k) holds ((N . k) . j) is Subgroup of (M . k) by GROUP_19:def 9;

                

                 A75: ( 1_ ( product (N . k))) = ((J . k) --> ( 1_ (M . k))) by A74, GROUP_19: 13;

                set q = (((J . k) --> ( 1_ (M . k))) +* (j,g));

                

                 A76: q in ( sum (N . k)) by A70, A75, GROUP_2: 44;

                for j be object st j in (J . k) holds ((N . k) . j) is Subgroup of (M . k) by A73, GROUP_19:def 9;

                then

                reconsider q as finite-support Function of (J . k), (M . k) by A76, GROUP_19: 10;

                

                 A77: q = (( 1_ ( product (N . k))) +* (j,g)) by A74, GROUP_19: 13

                .= (( 1_ ( sum (N . k))) +* (j,g)) by GROUP_2: 44;

                ((N . k) . j) is Subgroup of (M . k) by A37, A38, A73, GROUP_19:def 9;

                then g is Element of (M . k) by A39, GROUP_2: 42;

                then

                 A78: ( Product q) = g by A37, A38, GROUP_19: 21;

                (hk . (( 1_ ( sum (N . k))) +* (j,g))) = g by A45, A71, A77, A78;

                then ((hk " ) . (hk . (( 1_ ( product (N . k))) +* (j,g)))) = ((hk " ) . g) by GROUP_2: 44;

                then

                 A79: ((hk " ) . g) = (( 1_ ( product (N . k))) +* (j,g)) by A45, A72, FUNCT_1: 34;

                per cases ;

                  suppose

                   A80: j <> n;

                  

                  thus (yi . n0) = (y . n) by A67, FUNCT_1: 47

                  .= ( 1_ (UN . n1)) by A59, A80, GROUP_12: 1

                  .= ( 1_ ((N . i) . n)) by Th19

                  .= (xi . n0) by A37, A38, A39, A65, A66, A79, A80, GROUP_12: 1;

                end;

                  suppose

                   A81: j = n;

                  

                  thus (yi . n0) = (y . n) by A67, FUNCT_1: 47

                  .= g by A59, A81, GROUP_12: 1

                  .= (xi . n0) by A37, A38, A39, A66, A79, A81, GROUP_12: 1;

                end;

              end;

              then yi = xi by A55, A57, GROUP_19: 3;

              hence thesis by A43, Th25;

            end;

          end;

          then

           A82: z = (( 1ProdHom (M,k)) . g) by A49, A51, A53, FUNCT_1: 2, GROUP_19: 3;

          g in (M . k) by A41, GROUP_2: 40;

          then

           A83: z = (( 1_ ( product M)) +* (k,g)) by A82, GROUP_12:def 3;

          z = ((I --> ( 1_ G)) +* (k,g)) by A20, A83, GROUP_19: 13;

          hence thesis by A28, A32, A36, GROUP_19: 21;

        end;

        hence thesis by A27, GROUP_20: 18;

      end;

      hence thesis by A18, A26, GROUP_19:def 9;

    end;

    begin

    theorem :: GROUP_21:38

    

     Th41: for I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, G be Group, M be Group-Family of I holds for N be Group-Family of I, J st ( Union N) is DirectSumComponents of G, ( Union J) & for i be Element of I holds (N . i) is DirectSumComponents of (M . i), (J . i) holds M is DirectSumComponents of G, I

    proof

      let I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, G be Group, M be Group-Family of I;

      let N be Group-Family of I, J;

      assume that

       A1: ( Union N) is DirectSumComponents of G, ( Union J) and

       A2: for i be Element of I holds (N . i) is DirectSumComponents of (M . i), (J . i);

      set UN = ( Union N);

      consider fNtoG be Homomorphism of ( sum UN), G such that

       A3: fNtoG is bijective by A1, GROUP_19:def 8;

      deffunc P( object) = the carrier of ( sum (N . ( In ($1,I))));

      consider DS be Function such that

       A4: ( dom DS) = I & for i be object st i in I holds (DS . i) = P(i) from FUNCT_1:sch 3;

      reconsider DS as ManySortedSet of I by A4, PARTFUN1:def 2, RELAT_1:def 18;

      deffunc Q( object) = the carrier of (M . ( In ($1,I)));

      consider RS be Function such that

       A5: ( dom RS) = I & for i be object st i in I holds (RS . i) = Q(i) from FUNCT_1:sch 3;

      reconsider RS as ManySortedSet of I by A5, PARTFUN1:def 2, RELAT_1:def 18;

      defpred R[ object, object] means ex fi be Homomorphism of (M . ( In ($1,I))), ( sum (N . ( In ($1,I)))) st fi = $2 & fi is bijective;

      

       A6: for i be Element of I holds ex y be Element of ( PFuncs (( Union RS),( Union DS))) st R[i, y]

      proof

        let i be Element of I;

        (N . i) is DirectSumComponents of (M . i), (J . i) by A2;

        then

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

         A7: g is bijective by GROUP_19:def 8;

        reconsider h = (g " ) as Homomorphism of (M . i), ( sum (N . i)) by A7, GROUP_6: 62;

        

         A8: h is bijective by A7, GROUP_6: 63;

        

         A9: ( In (i,I)) = i;

        (DS . i) in ( rng DS) & (RS . i) in ( rng RS) by A4, A5, FUNCT_1: 3;

        then the carrier of ( sum (N . i)) in ( rng DS) & the carrier of (M . i) in ( rng RS) by A4, A5, A9;

        then the carrier of ( sum (N . i)) c= ( Union DS) & the carrier of (M . i) c= ( Union RS) by ZFMISC_1: 74;

        then ( dom h) c= ( Union RS) & ( rng h) c= ( Union DS);

        then

        reconsider y = h as Element of ( PFuncs (( Union RS),( Union DS))) by PARTFUN1:def 3;

        take y;

        thus ex h be Homomorphism of (M . ( In (i,I))), ( sum (N . ( In (i,I)))) st h = y & h is bijective by A8;

      end;

      consider fMtoBN be Function of I, ( PFuncs (( Union RS),( Union DS))) such that

       A10: for i be Element of I holds R[i, (fMtoBN . i)] from FUNCT_2:sch 3( A6);

      

       A11: ( dom fMtoBN) = I by FUNCT_2:def 1;

      reconsider fMtoBN as ManySortedSet of I;

      reconsider fMtoDN = ( SumMap (M,( sum_bundle N),fMtoBN)) as Homomorphism of ( sum M), ( dsum N);

      for i be Element of I holds ex hi be Homomorphism of (M . i), (( sum_bundle N) . i) st hi = (fMtoBN . i) & hi is bijective

      proof

        let i be Element of I;

        consider fi be Homomorphism of (M . ( In (i,I))), ( sum (N . ( In (i,I)))) such that

         A13: fi = (fMtoBN . i) & fi is bijective by A10;

        ( sum (N . ( In (i,I)))) = (( sum_bundle N) . i) by Def7;

        hence thesis by A13;

      end;

      then

       A14: fMtoDN is bijective by A11, GROUP_19: 41;

      reconsider h = ((fNtoG * ( dsum2sum N)) * fMtoDN) as Homomorphism of ( sum M), G;

      take h;

      

       A15: (fNtoG * ( dsum2sum N)) is one-to-one onto by A3, FUNCT_2: 27;

      h is one-to-one onto by A14, A15, FUNCT_2: 27;

      hence h is bijective;

    end;

    theorem :: GROUP_21:39

    for I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, G be Group, M be Subgroup-Family of I, G holds for N be Group-Family of I, J st ( Union N) is internal DirectSumComponents of G, ( Union J) & for i be Element of I holds (N . i) is internal DirectSumComponents of (M . i), (J . i) holds M is internal DirectSumComponents of G, I

    proof

      let I be non empty set, J be non-empty disjoint_valued ManySortedSet of I, G be Group, M be Subgroup-Family of I, G;

      let N be Group-Family of I, J;

      assume that

       A1: ( Union N) is internal DirectSumComponents of G, ( Union J) and

       A2: for i be Element of I holds (N . i) is internal DirectSumComponents of (M . i), (J . i);

      reconsider UJ = ( Union J) as non empty set;

      for i be Element of I holds (N . i) is DirectSumComponents of (M . i), (J . i) by A2;

      then

      reconsider M as DirectSumComponents of G, I by A1, Th41;

      

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

      consider fNtoG be Homomorphism of ( sum ( Union N)), G such that

       A4: fNtoG is bijective and

       A5: for x be finite-support Function of UJ, G st x in ( sum ( Union N)) holds (fNtoG . x) = ( Product x) by A1, GROUP_19:def 9;

      defpred Q[ object, object] means ex Ni be internal DirectSumComponents of (M . ( In ($1,I))), (J . ( In ($1,I))) st Ni = (N . $1) & $2 = (( InterHom Ni) " );

      

       A6: for x,y1,y2 be object st x in I & Q[x, y1] & Q[x, y2] holds y1 = y2;

      

       A7: for x be object st x in I holds ex y be object st Q[x, y]

      proof

        let x be object;

        assume x in I;

        then

        reconsider i = x as Element of I;

        reconsider Ni = (N . i) as internal DirectSumComponents of (M . i), (J . i) by A2;

        take y = (( InterHom Ni) " );

        thus thesis;

      end;

      consider fMtoBN be Function such that

       A9: ( dom fMtoBN) = I & for i be object st i in I holds Q[i, (fMtoBN . i)] from FUNCT_1:sch 2( A6, A7);

      reconsider fMtoBN as ManySortedSet of I by A9, PARTFUN1:def 2, RELAT_1:def 18;

      reconsider fMtoDN = ( SumMap (M,( sum_bundle N),fMtoBN)) as Homomorphism of ( sum M), ( dsum N);

      for i be Element of I holds ex hi be Homomorphism of (M . i), (( sum_bundle N) . i) st hi = (fMtoBN . i) & hi is bijective

      proof

        let i be Element of I;

        consider Ni be internal DirectSumComponents of (M . ( In (i,I))), (J . ( In (i,I))) such that

         A11: Ni = (N . i) & (fMtoBN . i) = (( InterHom Ni) " ) by A9;

        reconsider g = ( InterHom Ni) as Homomorphism of ( sum (N . i)), (M . i) by A11;

        reconsider fi = (g " ) as Homomorphism of (M . i), ( sum (N . i)) by A11, Def15, GROUP_6: 62;

        g is bijective by A11, Def15;

        then

         A12: fi = (fMtoBN . i) & fi is bijective by A11, GROUP_6: 63;

        ( sum (N . ( In (i,I)))) = (( sum_bundle N) . i) by Def7;

        hence thesis by A12;

      end;

      then

       A13: fMtoDN is bijective by A9, GROUP_19: 41;

      reconsider h = ((fNtoG * ( dsum2sum N)) * fMtoDN) as Homomorphism of ( sum M), G;

      

       A14: for i be Element of I holds ex hi be Homomorphism of (( sum_bundle N) . i), (M . i) st (hi " ) = (fMtoBN . i) & hi is bijective & for x be finite-support Function of (J . i), (M . i) st x in (( sum_bundle N) . i) holds (hi . x) = ( Product x)

      proof

        let i be Element of I;

        consider Ni be internal DirectSumComponents of (M . ( In (i,I))), (J . ( In (i,I))) such that

         A16: Ni = (N . i) & (fMtoBN . i) = (( InterHom Ni) " ) by A9;

        

         A17: ( InterHom Ni) is bijective & for x be finite-support Function of (J . i), (M . i) st x in ( sum Ni) holds (( InterHom Ni) . x) = ( Product x) by Def15;

        

         A18: ( sum (N . ( In (i,I)))) = (( sum_bundle N) . i) by Def7;

        then

        reconsider hi = ( InterHom Ni) as Homomorphism of (( sum_bundle N) . i), (M . i) by A16;

        thus thesis by A16, A17, A18;

      end;

      

       A19: for i be Element of I holds ex hi be Homomorphism of (( sum_bundle N) . i), (M . i) st (hi " ) = (fMtoBN . i) & hi is bijective

      proof

        let i be Element of I;

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

         A20: (hi " ) = (fMtoBN . i) & hi is bijective & for x be finite-support Function of (J . i), (M . i) st x in (( sum_bundle N) . i) holds (hi . x) = ( Product x) by A14;

        take hi;

        thus thesis by A20;

      end;

      (fNtoG * ( dsum2sum N)) is one-to-one onto by A4, FUNCT_2: 27;

      then

       A21: h is one-to-one onto by A13, FUNCT_2: 27;

      for i be Element of I holds (N . i) is DirectSumComponents of (M . i), (J . i) by A2;

      then

      reconsider UN = ( Union N) as DirectSumComponents of G, UJ by Th39;

      reconsider UJ = ( Union J) as non empty set;

      

       A22: for j be object st j in UJ holds (UN . j) is Subgroup of G by A1, GROUP_19:def 9;

      

       A23: for i be Element of I holds (M . i) is Subgroup of G by GROUP_20:def 1;

      reconsider UN as Subgroup-Family of UJ, G by A22, GROUP_20:def 1;

      for x be finite-support Function of I, G st x in ( sum M) holds (h . x) = ( Product x)

      proof

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

        assume

         A24: x in ( sum M);

        for i be Element of I, g be Element of (M . i) holds (h . (( 1ProdHom (M,i)) . g)) = g

        proof

          let i be Element of I, g be Element of (M . i);

          

           A25: ( dom ( dsum2sum N)) = the carrier of ( dsum N) by FUNCT_2:def 1;

          

           A26: (( 1ProdHom (M,i)) . g) in ( ProjGroup (M,i));

          then

           A27: (( 1ProdHom (M,i)) . g) in ( sum M) by GROUP_2: 40;

          then (( 1ProdHom (M,i)) . g) in ( dom fMtoDN) by FUNCT_2:def 1;

          then

           A28: (h . (( 1ProdHom (M,i)) . g)) = ((fNtoG * ( dsum2sum N)) . (fMtoDN . (( 1ProdHom (M,i)) . g))) by FUNCT_1: 13;

          

           A29: (fMtoDN . (( 1ProdHom (M,i)) . g)) in the carrier of ( dsum N) by A27, FUNCT_2: 5;

          

           A30: ((fNtoG * ( dsum2sum N)) . (fMtoDN . (( 1ProdHom (M,i)) . g))) = (fNtoG . (( dsum2sum N) . (fMtoDN . (( 1ProdHom (M,i)) . g)))) by A27, FUNCT_2: 5, FUNCT_2: 15;

          

           A31: (( dsum2sum N) . (fMtoDN . (( 1ProdHom (M,i)) . g))) in ( sum UN) by A29, FUNCT_2: 5;

          for j be object st j in UJ holds (UN . j) is Subgroup of G by A1, GROUP_19:def 9;

          then

          reconsider z = (( dsum2sum N) . (fMtoDN . (( 1ProdHom (M,i)) . g))) as finite-support Function of UJ, G by A31, GROUP_19: 10;

          

           A32: ((fNtoG * ( dsum2sum N)) . (fMtoDN . (( 1ProdHom (M,i)) . g))) = ( Product z) by A5, A30, A31;

          

           A33: (( dsum2sum N) . (fMtoDN . (( 1ProdHom (M,i)) . g))) = (( dprod2prod N) . (fMtoDN . (( 1ProdHom (M,i)) . g))) by A25, A27, FUNCT_1: 47, FUNCT_2: 5;

          (( 1ProdHom (M,i)) . g) in ( product M) by A26, GROUP_2: 40;

          then

          reconsider y = (( 1ProdHom (M,i)) . g) as Element of ( product M);

          (fMtoDN . (( 1ProdHom (M,i)) . g)) in ( dsum N) by A27, FUNCT_2: 5;

          then (fMtoDN . (( 1ProdHom (M,i)) . g)) in ( dprod N) by GROUP_2: 40;

          then

          reconsider t = (fMtoDN . (( 1ProdHom (M,i)) . g)) as Element of ( dprod N);

          

           A34: for k be Element of I holds (t . k) = (z | (J . k)) by A33, Def10;

          

           A35: for i be Element of I holds (fMtoBN . i) is Homomorphism of (M . i), (( sum_bundle N) . i)

          proof

            let i be Element of I;

            ex hi be Homomorphism of (( sum_bundle N) . i), (M . i) st (hi " ) = (fMtoBN . i) & hi is bijective by A19;

            hence thesis by GROUP_6: 62;

          end;

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

           A37: (hi " ) = (fMtoBN . i) & hi is bijective & for x be finite-support Function of (J . i), (M . i) st x in (( sum_bundle N) . i) holds (hi . x) = ( Product x) by A14;

          

           A38: hi is one-to-one & ( rng hi) = the carrier of (M . i) by A37, FUNCT_2:def 3;

          then

           A39: (hi " ) is Function of the carrier of (M . i), the carrier of (( sum_bundle N) . i) by FUNCT_2: 25;

          

           A40: (hi " ) is Homomorphism of (M . i), (( sum_bundle N) . i) by A37, GROUP_6: 62;

          

           A41: (fMtoDN . (( 1ProdHom (M,i)) . g)) = (( 1ProdHom (( sum_bundle N),i)) . ((hi " ) . g)) by A9, A35, A37, A40, GROUP_19: 42;

          reconsider hkg = ((hi " ) . g) as Element of (( sum_bundle N) . i) by A39, FUNCT_2: 5;

          (( 1ProdHom (( sum_bundle N),i)) . hkg) in ( ProjGroup (( sum_bundle N),i));

          then (( 1ProdHom (( sum_bundle N),i)) . hkg) in ( product ( sum_bundle N)) by GROUP_2: 40;

          then

          reconsider p = (( 1ProdHom (( sum_bundle N),i)) . hkg) as Function;

          

           A42: ((hi " ) . g) in (( sum_bundle N) . i) by A39, FUNCT_2: 5;

          then

           A43: ((hi " ) . g) in ( sum (N . i)) by Def7;

          then

          reconsider hkg0 = ((hi " ) . g) as Function;

          for j be object st j in (J . i) holds ((N . i) . j) is Subgroup of G

          proof

            let j be object;

            assume

             A44: j in (J . i);

            (N . i) is internal DirectSumComponents of (M . i), (J . i) by A2;

            then

             A45: ((N . i) . j) is Subgroup of (M . i) by A44, GROUP_19:def 9;

            (M . i) is Subgroup of G by GROUP_20:def 1;

            hence thesis by A45, GROUP_2: 56;

          end;

          then

          reconsider hkg0 as finite-support Function of (J . i), G by A43, GROUP_19: 10;

          (J . i) c= ( Union J) by A3, FUNCT_1: 3, ZFMISC_1: 74;

          then

           A46: (J . i) c= UJ;

          

           A47: (p . i) = (z | (J . i)) by A34, A41;

          

           A48: p = (( 1_ ( product ( sum_bundle N))) +* (i,hkg)) by GROUP_12:def 3;

          

           A49: ( dom ( 1_ ( product ( sum_bundle N)))) = I by GROUP_19: 3;

          then

           A50: (z | (J . i)) = hkg0 by A47, A48, FUNCT_7: 31;

          for m be object holds m in ( support z) iff m in ( support hkg0)

          proof

            let m be object;

            hereby

              assume

               QX: m in ( support z);

              then

               A51: (z . m) <> ( 1_ G) & m in UJ by GROUP_19:def 2;

              then

              consider Y be set such that

               A52: m in Y & Y in ( rng J) by TARSKI:def 4;

              consider k be object such that

               A53: k in ( dom J) & Y = (J . k) by A52, FUNCT_1:def 3;

              reconsider k as Element of I by A53;

              

               A54: k = i

              proof

                assume

                 A55: k <> i;

                (UN . m) = ((N . k) . m) by A52, A53, Th19;

                then

                reconsider P = ((N . k) . m) as Subgroup of G by A1, GROUP_19:def 9, QX;

                (p . k) = ( 1_ (( sum_bundle N) . k)) by A48, A55, GROUP_12: 1

                .= ( 1_ ( sum (N . k))) by Def7;

                

                then ((z | (J . k)) . m) = (( 1_ ( sum (N . k))) . m) by A34, A41

                .= (( 1_ ( product (N . k))) . m) by GROUP_2: 44

                .= ( 1_ P) by A52, A53, GROUP_7: 6

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

                hence contradiction by A51, A52, A53, FUNCT_1: 49;

              end;

              

              then (z . m) = ((z | (J . i)) . m) by A52, A53, FUNCT_1: 49

              .= (hkg0 . m) by A47, A48, A49, FUNCT_7: 31;

              hence m in ( support hkg0) by A51, A52, A53, A54, GROUP_19:def 2;

            end;

            assume m in ( support hkg0);

            then

             A57: (hkg0 . m) <> ( 1_ G) & m in (J . i) by GROUP_19:def 2;

            (z . m) <> ( 1_ G) by A50, A57, FUNCT_1: 49;

            hence m in ( support z) by A46, A57, GROUP_19:def 2;

          end;

          then

           A58: ( support z) = ( support hkg0) by TARSKI: 2;

          for j be object st j in (J . i) holds ((N . i) . j) is Subgroup of (M . i)

          proof

            let j be object;

            assume

             A59: j in (J . i);

            (N . i) is internal DirectSumComponents of (M . i), (J . i) by A2;

            hence ((N . i) . j) is Subgroup of (M . i) by A59, GROUP_19:def 9;

          end;

          then

          reconsider hkg01 = hkg0 as finite-support Function of (J . i), (M . i) by A43, GROUP_19: 10;

          

           A60: (M . i) is Subgroup of G by GROUP_20:def 1;

          g = (hi . ((hi " ) . g)) by A38, FUNCT_1: 35

          .= ( Product hkg01) by A37, A42

          .= ( Product hkg0) by A60, GROUP_20: 6;

          hence thesis by A28, A32, A50, A58, RELAT_1: 74;

        end;

        hence thesis by A24, GROUP_20: 18;

      end;

      hence thesis by A21, A23, GROUP_19:def 9;

    end;

    theorem :: GROUP_21:40

    

     Th43: for I2 be non empty set, F2 be Group-Family of I2 st for i be Element of I2 holds ( card (F2 . i)) = 1 holds ( card the carrier of ( sum F2)) = 1

    proof

      let I2 be non empty set, F2 be Group-Family of I2;

      assume

       A1: for i be Element of I2 holds ( card (F2 . i)) = 1;

      

       A2: for x be object holds ( 1_ ( sum F2)) = x implies x in ( [#] ( sum F2));

      for x be object holds x in ( [#] ( sum F2)) implies x = ( 1_ ( sum F2))

      proof

        let x be object;

        assume x in ( [#] ( sum F2));

        then

        reconsider x as Element of ( product F2) by GROUP_2: 42;

        ( dom x) = I2 by GROUP_19: 3;

        then

        reconsider x as ManySortedSet of I2 by PARTFUN1:def 2, RELAT_1:def 18;

        for i be set st i in I2 holds ex G be Group-like non empty multMagma st G = (F2 . i) & (x . i) = ( 1_ G)

        proof

          let i be set;

          assume i in I2;

          then

          reconsider i as Element of I2;

          reconsider G = (F2 . i) as Group;

          take G;

          

           A3: ( card G) = 1 by A1;

          then

           A4: ( [#] G) is finite;

          

           A5: ( card {( 1_ G)}) = 1 by CARD_1: 30;

          

           A6: ( [#] G) = {( 1_ G)} by A3, A4, A5, CARD_2: 102;

          x in ( product F2);

          then (x . i) in (F2 . i) by GROUP_19: 5;

          hence thesis by A6, TARSKI:def 1;

        end;

        then x = ( 1_ ( product F2)) by GROUP_7: 5;

        hence thesis by GROUP_2: 44;

      end;

      then ( [#] ( sum F2)) = {( 1_ ( sum F2))} by A2, TARSKI:def 1;

      hence thesis by CARD_1: 30;

    end;

    theorem :: GROUP_21:41

    

     Th44: for I be non empty set, G be Group, x be finite-support Function of I, G st for i be object st i in I holds (x . i) = ( 1_ G) holds ( Product x) = ( 1_ G)

    proof

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

      assume

       A1: for i be object st i in I holds (x . i) = ( 1_ G);

      ( support x) = {}

      proof

        assume not ( support x) = {} ;

        then

        consider i be object such that

         A2: i in ( support x) by XBOOLE_0:def 1;

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

        hence contradiction by A1;

      end;

      hence thesis by GROUP_19: 15;

    end;

    theorem :: GROUP_21:42

    

     Th45: for I be non empty set, G be Group, x be finite-support Function of I, G, a be Element of G st I = {1, 2} & x = <*a, ( 1_ G)*> holds ( Product x) = a

    proof

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

      assume

       A1: I = {1, 2} & x = <*a, ( 1_ G)*>;

      reconsider i1 = 1 as Element of I by A1, TARSKI:def 2;

      set y = ((I --> ( 1_ G)) +* (i1,a));

      

       A2: ( dom y) = ( dom (I --> ( 1_ G))) by FUNCT_7: 30

      .= I by FUNCOP_1: 13;

      

       A3: ( dom (I --> ( 1_ G))) = I by FUNCOP_1: 13;

      for i be object st i in ( dom x) holds (x . i) = (y . i)

      proof

        let i be object;

        assume

         A4: i in ( dom x);

        then

         A5: i = 1 or i = 2 by A1, TARSKI:def 2;

        reconsider i0 = i as Element of I by A4;

        per cases ;

          suppose

           A6: i = 1;

          

          thus (x . i) = a by A1, A6, FINSEQ_1: 44

          .= (y . i) by A3, A6, FUNCT_7: 31;

        end;

          suppose

           A7: i <> 1;

          

          hence (y . i) = ((I --> ( 1_ G)) . i) by FUNCT_7: 32

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

          .= (x . i) by A1, A5, A7, FINSEQ_1: 44;

        end;

      end;

      then x = ((I --> ( 1_ G)) +* (i1,a)) by A2, FUNCT_2:def 1;

      hence thesis by GROUP_19: 21;

    end;

    theorem :: GROUP_21:43

    for G be Group, I1,I2 be non empty set, F1 be DirectSumComponents of G, I1, F2 be Group-Family of I2 st I1 misses I2 & for i be Element of I2 holds ( card (F2 . i)) = 1 holds (F1 +* F2) is DirectSumComponents of G, (I1 \/ I2)

    proof

      let G be Group, I1,I2 be non empty set, F1 be DirectSumComponents of G, I1, F2 be Group-Family of I2;

      assume that

       A1: I1 misses I2 and

       A2: for i be Element of I2 holds ( card (F2 . i)) = 1;

      reconsider I = {1, 2} as non empty set;

      set J = { [1, I1], [2, I2]};

      for x,y1,y2 be object st [x, y1] in J & [x, y2] in J holds y1 = y2

      proof

        let x,y1,y2 be object;

        assume [x, y1] in J & [x, y2] in J;

        then

         A3: ( [x, y1] = [1, I1] or [x, y1] = [2, I2]) & ( [x, y2] = [1, I1] or [x, y2] = [2, I2]) by TARSKI:def 2;

        per cases by XTUPLE_0: 1;

          suppose x = 1 & y1 = I1;

          hence y1 = y2 by A3, XTUPLE_0: 1;

        end;

          suppose x = 2 & y1 = I2;

          hence y1 = y2 by A3, XTUPLE_0: 1;

        end;

      end;

      then

      reconsider J as Function by FUNCT_1:def 1;

      ( dom J) = I by RELAT_1: 10;

      then

      reconsider J as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

      

       A4: ( rng J) = {I1, I2} by RELAT_1: 10;

       [1, I1] in J by TARSKI:def 2;

      then

       A5: 1 in ( dom J) & (J . 1) = I1 by FUNCT_1: 1;

       [2, I2] in J by TARSKI:def 2;

      then

       A6: 2 in ( dom J) & (J . 2) = I2 by FUNCT_1: 1;

       not {} in ( rng J)

      proof

        assume {} in ( rng J);

        then

        consider x be object such that

         A7: x in ( dom J) & {} = (J . x) by FUNCT_1:def 3;

        thus contradiction by A5, A6, A7, TARSKI:def 2;

      end;

      then J is non-empty;

      then

      reconsider J as non-empty ManySortedSet of I;

      for i,j be object st i <> j holds (J . i) misses (J . j)

      proof

        let i,j be object;

        assume

         A8: i <> j;

        per cases ;

          suppose not i in ( dom J) or not j in ( dom J);

          then (J . i) = {} or (J . j) = {} by FUNCT_1:def 2;

          then ((J . i) /\ (J . j)) = {} ;

          hence (J . i) misses (J . j) by XBOOLE_0:def 7;

        end;

          suppose i in ( dom J) & j in ( dom J);

          then (i = 1 or i = 2) & (j = 1 or j = 2) by TARSKI:def 2;

          hence (J . i) misses (J . j) by A1, A5, A6, A8;

        end;

      end;

      then J is disjoint_valued;

      then

      reconsider J as non-empty disjoint_valued ManySortedSet of I;

      reconsider M = <*( sum F1), ( sum F2)*> as Group-Family of I;

      set w0 = the object;

      ( card ( [#] ( sum F2))) = 1 by A2, Th43;

      then ( card ( [#] ( sum F2))) = ( card {w0}) by CARD_1: 30;

      then

      consider w be object such that

       A9: {w} = ( [#] ( sum F2)) by CARD_1: 29;

      

       A10: for x,y be Function st x in ( [#] ( product M)) & y in ( [#] ( product M)) & (x . 1) = (y . 1) holds x = y

      proof

        let x,y be Function;

        assume that

         A11: x in ( [#] ( product M)) and

         A12: y in ( [#] ( product M)) and

         A13: (x . 1) = (y . 1);

        

         A14: ( dom x) = I & ( dom y) = I by A11, A12, GROUP_19: 3;

        for i be object st i in ( dom x) holds (x . i) = (y . i)

        proof

          let i be object;

          assume i in ( dom x);

          then

           A15: i = 1 or i = 2 by A14, TARSKI:def 2;

          

           A16: x in ( product M) & y in ( product M) by A11, A12;

          reconsider p = x, q = y as Function;

          

           B1: 2 is Element of I by TARSKI:def 2;

          then

          reconsider M2 = (M . 2) as Group by GROUP_19: 1;

          (p . 2) in M2 & (q . 2) in M2 by A16, B1, GROUP_19: 5;

          then (p . 2) in ( sum F2) & (q . 2) in ( sum F2) by FINSEQ_1: 44;

          then (p . 2) = w & (q . 2) = w by A9, TARSKI:def 1;

          hence thesis by A13, A15;

        end;

        hence thesis by A14;

      end;

      consider h1 be Homomorphism of ( sum F1), G such that

       A17: h1 is bijective by GROUP_19:def 8;

      set CS1 = the carrier of ( product M);

      set CS2 = the carrier of G;

      defpred P[ Element of CS1, Element of CS2] means $2 = (h1 . ($1 . 1));

      

       A18: for x be Element of CS1 holds ex y be Element of CS2 st P[x, y]

      proof

        let x be Element of CS1;

        

         A19: x in ( product M);

        reconsider x as Function;

        

         B1: 1 is Element of I by TARSKI:def 2;

        then

        reconsider M1 = (M . 1) as Group by GROUP_19: 1;

        (x . 1) in M1 by B1, A19, GROUP_19: 5;

        then (x . 1) in ( sum F1) by FINSEQ_1: 44;

        then (h1 . (x . 1)) in CS2 by FUNCT_2: 5;

        hence thesis;

      end;

      consider h be Function of CS1, CS2 such that

       A20: for x be Element of CS1 holds P[x, (h . x)] from FUNCT_2:sch 3( A18);

      reconsider h as Function of CS1, CS2;

      for x1,x2 be object st x1 in CS1 & x2 in CS1 & (h . x1) = (h . x2) holds x1 = x2

      proof

        let x1,x2 be object;

        assume

         A21: x1 in CS1 & x2 in CS1 & (h . x1) = (h . x2);

        then

        reconsider x10 = x1, x20 = x2 as Element of CS1;

        

         A22: (h . x10) = (h1 . (x10 . 1)) by A20;

        

         A23: (h . x20) = (h1 . (x20 . 1)) by A20;

        

         A24: x1 in ( product M) & x2 in ( product M) by A21;

        reconsider z1 = x1 as Function by A21;

        reconsider z2 = x2 as Function by A21;

        

         B2: 1 is Element of I by TARSKI:def 2;

        then

        reconsider M1 = (M . 1) as Group by GROUP_19: 1;

        (z1 . 1) in M1 & (z2 . 1) in M1 by A24, B2, GROUP_19: 5;

        then

         A25: (x10 . 1) in the carrier of ( sum F1) & (x20 . 1) in the carrier of ( sum F1) by FINSEQ_1: 44;

        (x10 . 1) = (x20 . 1) by A17, A21, A22, A23, A25, FUNCT_2: 19;

        hence x1 = x2 by A10;

      end;

      then

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

      for y be object st y in CS2 holds ex x be object st x in CS1 & y = (h . x)

      proof

        let y be object;

        assume y in CS2;

        then y in ( rng h1) by A17, FUNCT_2:def 3;

        then

        consider x1 be object such that

         A27: x1 in ( [#] ( sum F1)) & y = (h1 . x1) by FUNCT_2: 11;

        reconsider x1 as Element of ( [#] ( sum F1)) by A27;

        set z1 = the Element of ( [#] ( sum F2));

        reconsider x = <*x1, z1*> as Element of CS1;

        take x;

        (h . x) = (h1 . (x . 1)) by A20

        .= y by A27, FINSEQ_1: 44;

        hence thesis;

      end;

      then ( rng h) = CS2 by FUNCT_2: 10;

      then

       A28: h is onto by FUNCT_2:def 3;

      for a,b be Element of CS1 holds (h . (a * b)) = ((h . a) * (h . b))

      proof

        let a,b be Element of CS1;

        

         A29: 1 in I by TARSKI:def 2;

        

         A30: (M . 1) = ( sum F1) by FINSEQ_1: 44;

        

         A31: a in ( product M) & b in ( product M);

        reconsider a1 = a, b1 = b as Function;

        

         B3: 1 is Element of I by TARSKI:def 2;

        then

        reconsider M1 = (M . 1) as Group by GROUP_19: 1;

        (a1 . 1) in M1 & (b1 . 1) in M1 by B3, A31, GROUP_19: 5;

        then

        reconsider a1 = (a . 1), b1 = (b . 1) as Element of ( sum F1) by FINSEQ_1: 44;

        

        thus (h . (a * b)) = (h1 . ((a * b) . 1)) by A20

        .= (h1 . (a1 * b1)) by A29, A30, GROUP_7: 1

        .= ((h1 . a1) * (h1 . b1)) by GROUP_6:def 6

        .= ((h1 . a1) * (h . b)) by A20

        .= ((h . a) * (h . b)) by A20;

      end;

      then

       A32: h is Homomorphism of ( product M), G by GROUP_6:def 6;

      ( product M) = ( sum M) by GROUP_7: 9;

      then

      reconsider M = <*( sum F1), ( sum F2)*> as DirectSumComponents of G, I by A26, A28, A32, GROUP_19:def 8;

      set N = <*F1, F2*>;

      ( len N) = 2 by FINSEQ_1: 44;

      then ( dom N) = I by FINSEQ_1: 2, FINSEQ_1:def 3;

      then

      reconsider N as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

      

       A33: for i be Element of I holds (N . i) is Group-Family of (J . i)

      proof

        let i be Element of I;

        per cases by TARSKI:def 2;

          suppose i = 1;

          hence (N . i) is Group-Family of (J . i) by A5, FINSEQ_1: 44;

        end;

          suppose i = 2;

          hence (N . i) is Group-Family of (J . i) by A6, FINSEQ_1: 44;

        end;

      end;

      then for i be Element of I holds (N . i) is multMagma-Family of (J . i);

      then

      reconsider N as multMagma-Family of I, J by Def4;

      reconsider N as Group-Family of I, J by A33, Def5;

      

       A34: for i be Element of I holds (N . i) is DirectSumComponents of (M . i), (J . i)

      proof

        let i be Element of I;

        per cases by TARSKI:def 2;

          suppose

           A35: i = 1;

          set h = ( id the carrier of ( sum F1));

          for a,b be Element of ( sum F1) holds (h . (a * b)) = ((h . a) * (h . b));

          then

           A36: h is Homomorphism of ( sum F1), ( sum F1) & h is bijective by GROUP_6:def 6;

          

           A37: (N . i) = F1 & (M . i) = ( sum F1) by A35, FINSEQ_1: 44;

          thus (N . i) is DirectSumComponents of (M . i), (J . i) by A5, A35, A36, A37, GROUP_19:def 8;

        end;

          suppose

           A38: i = 2;

          set h = ( id the carrier of ( sum F2));

          for a,b be Element of ( sum F2) holds (h . (a * b)) = ((h . a) * (h . b));

          then

           A39: h is Homomorphism of ( sum F2), ( sum F2) & h is bijective by GROUP_6:def 6;

          

           A40: (N . i) = F2 & (M . i) = ( sum F2) by A38, FINSEQ_1: 44;

          thus (N . i) is DirectSumComponents of (M . i), (J . i) by A6, A38, A39, A40, GROUP_19:def 8;

        end;

      end;

      

       A41: (I1 \/ I2) = ( Union J) by A4, ZFMISC_1: 75;

      

       A42: ( dom ( Union N)) = ( Union J) by PARTFUN1:def 2

      .= (( dom F1) \/ I2) by A41, PARTFUN1:def 2

      .= (( dom F1) \/ ( dom F2)) by PARTFUN1:def 2;

      for x be object st x in (( dom F1) \/ ( dom F2)) holds (x in ( dom F2) implies (( Union N) . x) = (F2 . x)) & ( not x in ( dom F2) implies (( Union N) . x) = (F1 . x))

      proof

        let x be object;

        assume x in (( dom F1) \/ ( dom F2));

        then

         A43: x in (I1 \/ ( dom F2)) by PARTFUN1:def 2;

        then

         A44: x in (I1 \/ I2) by PARTFUN1:def 2;

        thus x in ( dom F2) implies (( Union N) . x) = (F2 . x)

        proof

          assume

           A45: x in ( dom F2);

          then

          reconsider i = x as Element of ( Union J) by A41, XBOOLE_0:def 3;

          reconsider j = 2 as Element of I by TARSKI:def 2;

          (( Union N) . i) = ((N . j) . i) by A6, A45, Th19

          .= (F2 . i) by FINSEQ_1: 44;

          hence thesis;

        end;

        thus not x in ( dom F2) implies (( Union N) . x) = (F1 . x)

        proof

          assume

           A46: not x in ( dom F2);

          reconsider i = x as Element of ( Union J) by A41, A43, PARTFUN1:def 2;

          reconsider j = 1 as Element of I by TARSKI:def 2;

           not (x in I2) by A46, PARTFUN1:def 2;

          then i in (J . j) by A5, A44, XBOOLE_0:def 3;

          

          then (( Union N) . i) = ((N . j) . i) by Th19

          .= (F1 . i) by FINSEQ_1: 44;

          hence thesis;

        end;

      end;

      then (F1 +* F2) = ( Union N) by A42, FUNCT_4:def 1;

      hence thesis by A34, A41, Th39;

    end;

    theorem :: GROUP_21:44

    for G be Group, I1,I2 be non empty set, F1 be internal DirectSumComponents of G, I1, F2 be Subgroup-Family of I2, G st I1 misses I2 & F2 = (I2 --> ( (1). G)) holds (F1 +* F2) is internal DirectSumComponents of G, (I1 \/ I2)

    proof

      let G be Group, I1,I2 be non empty set, F1 be internal DirectSumComponents of G, I1, F2 be Subgroup-Family of I2, G;

      assume that

       A1: I1 misses I2 and

       A2: F2 = (I2 --> ( (1). G));

      reconsider I = {1, 2} as non empty set;

      set J = { [1, I1], [2, I2]};

      for x,y1,y2 be object st [x, y1] in J & [x, y2] in J holds y1 = y2

      proof

        let x,y1,y2 be object;

        assume [x, y1] in J & [x, y2] in J;

        then

         A3: ( [x, y1] = [1, I1] or [x, y1] = [2, I2]) & ( [x, y2] = [1, I1] or [x, y2] = [2, I2]) by TARSKI:def 2;

        per cases by XTUPLE_0: 1;

          suppose x = 1 & y1 = I1;

          hence y1 = y2 by A3, XTUPLE_0: 1;

        end;

          suppose x = 2 & y1 = I2;

          hence y1 = y2 by A3, XTUPLE_0: 1;

        end;

      end;

      then

      reconsider J as Function by FUNCT_1:def 1;

      ( dom J) = I by RELAT_1: 10;

      then

      reconsider J as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

      

       A4: ( rng J) = {I1, I2} by RELAT_1: 10;

       [1, I1] in J & [2, I2] in J by TARSKI:def 2;

      then

       A5: 1 in ( dom J) & (J . 1) = I1 & 2 in ( dom J) & (J . 2) = I2 by FUNCT_1: 1;

       not {} in ( rng J)

      proof

        assume {} in ( rng J);

        then

        consider x be object such that

         A6: x in ( dom J) & {} = (J . x) by FUNCT_1:def 3;

        thus contradiction by A5, A6, TARSKI:def 2;

      end;

      then J is non-empty;

      then

      reconsider J as non-empty ManySortedSet of I;

      for i,j be object st i <> j holds (J . i) misses (J . j)

      proof

        let i,j be object;

        assume

         A7: i <> j;

        per cases ;

          suppose not i in ( dom J) or not j in ( dom J);

          then (J . i) = {} or (J . j) = {} by FUNCT_1:def 2;

          then ((J . i) /\ (J . j)) = {} ;

          hence (J . i) misses (J . j) by XBOOLE_0:def 7;

        end;

          suppose i in ( dom J) & j in ( dom J);

          then (i = 1 or i = 2) & (j = 1 or j = 2) by TARSKI:def 2;

          hence (J . i) misses (J . j) by A1, A5, A7;

        end;

      end;

      then J is disjoint_valued;

      then

      reconsider J as non-empty disjoint_valued ManySortedSet of I;

      reconsider M = <*G, ( (1). G)*> as Group-Family of I;

      

       A8: for x,y be Function st x in ( [#] ( product M)) & y in ( [#] ( product M)) & (x . 1) = (y . 1) holds x = y

      proof

        let x,y be Function;

        assume that

         A9: x in ( [#] ( product M)) and

         A10: y in ( [#] ( product M)) and

         A11: (x . 1) = (y . 1);

        

         A12: ( dom x) = I & ( dom y) = I by A9, A10, GROUP_19: 3;

        for i be object st i in ( dom x) holds (x . i) = (y . i)

        proof

          let i be object;

          assume i in ( dom x);

          then

           A13: i = 1 or i = 2 by A12, TARSKI:def 2;

          

           A14: x in ( product M) & y in ( product M) by A9, A10;

          reconsider p = x, q = y as Function;

          

           B4: 2 is Element of I by TARSKI:def 2;

          then

          reconsider M2 = (M . 2) as Group by GROUP_19: 1;

          (p . 2) in M2 & (q . 2) in M2 by A14, B4, GROUP_19: 5;

          then (p . 2) in ( (1). G) & (q . 2) in ( (1). G) by FINSEQ_1: 44;

          then (p . 2) in {( 1_ G)} & (q . 2) in {( 1_ G)} by GROUP_2:def 7;

          then (p . 2) = ( 1_ G) & (q . 2) = ( 1_ G) by TARSKI:def 1;

          hence thesis by A11, A13;

        end;

        hence thesis by A12;

      end;

      set h1 = ( id the carrier of G);

      for a,b be Element of G holds (h1 . (a * b)) = ((h1 . a) * (h1 . b));

      then

      reconsider h1 as Homomorphism of G, G by GROUP_6:def 6;

      set CS1 = the carrier of ( product M);

      set CS2 = the carrier of G;

      defpred P[ Element of CS1, Element of CS2] means $2 = (h1 . ($1 . 1));

      

       A15: for x be Element of CS1 holds ex y be Element of CS2 st P[x, y]

      proof

        let x be Element of CS1;

        

         A16: x in ( product M);

        reconsider z = x as Function;

        

         B5: 1 is Element of I by TARSKI:def 2;

        then

        reconsider M1 = (M . 1) as Group by GROUP_19: 1;

        (z . 1) in M1 by A16, B5, GROUP_19: 5;

        then (z . 1) in G by FINSEQ_1: 44;

        then (h1 . (z . 1)) in CS2 by FUNCT_2: 5;

        hence thesis;

      end;

      consider h be Function of CS1, CS2 such that

       A17: for x be Element of CS1 holds P[x, (h . x)] from FUNCT_2:sch 3( A15);

      reconsider h as Function of CS1, CS2;

      

       A18: for x1,x2 be object st x1 in CS1 & x2 in CS1 & (h . x1) = (h . x2) holds x1 = x2

      proof

        let x1,x2 be object;

        assume

         A19: x1 in CS1 & x2 in CS1 & (h . x1) = (h . x2);

        then

        reconsider x10 = x1, x20 = x2 as Element of CS1;

        

         A20: (h . x10) = (h1 . (x10 . 1)) & (h . x20) = (h1 . (x20 . 1)) by A17;

        

         A21: x1 in ( product M) by A19;

        reconsider z1 = x1 as Function by A19;

        

         B6: 1 is Element of I by TARSKI:def 2;

        then

        reconsider M1 = (M . 1) as Group by GROUP_19: 1;

        (z1 . 1) in M1 by A21, B6, GROUP_19: 5;

        then

         A22: (x10 . 1) in the carrier of G by FINSEQ_1: 44;

        

         A23: x2 in ( product M) by A19;

        reconsider z2 = x2 as Function by A19;

        (z2 . 1) in M1 by A23, B6, GROUP_19: 5;

        then

         A24: (x20 . 1) in the carrier of G by FINSEQ_1: 44;

        (x10 . 1) = (x20 . 1) by A19, A20, A22, A24, FUNCT_2: 19;

        hence x1 = x2 by A8;

      end;

      then

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

      for y be object st y in CS2 holds ex x be object st x in CS1 & y = (h . x)

      proof

        let y be object;

        assume y in CS2;

        then y in ( rng h1);

        then

        consider x1 be object such that

         A26: x1 in the carrier of G & y = (h1 . x1) by FUNCT_2: 11;

        reconsider x1 as Element of G by A26;

        set z1 = the Element of the carrier of ( (1). G);

        reconsider x = <*x1, z1*> as Element of CS1;

        take x;

        (h . x) = (h1 . (x . 1)) by A17

        .= y by A26, FINSEQ_1: 44;

        hence thesis;

      end;

      then ( rng h) = CS2 by FUNCT_2: 10;

      then

       A27: h is onto by FUNCT_2:def 3;

      

       A28: for a,b be Element of CS1 holds (h . (a * b)) = ((h . a) * (h . b))

      proof

        let a,b be Element of CS1;

        

         A29: (h . a) = (h1 . (a . 1)) & (h . b) = (h1 . (b . 1)) by A17;

        

         A30: 1 in I by TARSKI:def 2;

        

         A31: (M . 1) = G by FINSEQ_1: 44;

        

         A32: a in ( product M) & b in ( product M);

        reconsider a1 = a, b1 = b as Function;

        

         B8: 1 is Element of I by TARSKI:def 2;

        then

        reconsider M1 = (M . 1) as Group by GROUP_19: 1;

        (a1 . 1) in M1 & (b1 . 1) in M1 by A32, B8, GROUP_19: 5;

        then

        reconsider a1 = (a . 1), b1 = (b . 1) as Element of G by FINSEQ_1: 44;

        

        thus (h . (a * b)) = (h1 . ((a * b) . 1)) by A17

        .= (h1 . (a1 * b1)) by A30, A31, GROUP_7: 1

        .= ((h . a) * (h . b)) by A29;

      end;

      ( product M) = ( sum M) by GROUP_7: 9;

      then

       A33: h is Homomorphism of ( sum M), G by A28, GROUP_6:def 6;

      then

      reconsider M = <*G, ( (1). G)*> as DirectSumComponents of G, I by A25, A27, GROUP_19:def 8;

      

       A34: for i be Element of I holds (M . i) is Subgroup of G

      proof

        let i be Element of I;

        

         A35: i = 1 or i = 2 by TARSKI:def 2;

        (M . 1) = G by FINSEQ_1: 44;

        hence thesis by A35, FINSEQ_1: 44, GROUP_2: 54;

      end;

      for x be finite-support Function of I, G st x in ( sum M) holds (h . x) = ( Product x)

      proof

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

        assume

         NN: x in ( sum M);

        then

         A36: x in ( product M) by GROUP_7: 9;

        reconsider x0 = x as Element of CS1 by GROUP_7: 9, NN;

        

         B10: 1 in I by TARSKI:def 2;

        then

        reconsider M1 = (M . 1) as Group by GROUP_19: 1;

        (x0 . 1) in M1 by A36, B10, GROUP_19: 5;

        then

        reconsider x01 = (x0 . 1) as Element of G by FINSEQ_1: 44;

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

        then

        reconsider z1 = ( 1_ G) as Element of ( (1). G) by GROUP_2:def 7;

        reconsider xx = <*x01, z1*> as Element of CS1;

        

         A37: (h . xx) = (h1 . (xx . 1)) by A17

        .= (h1 . x01) by FINSEQ_1: 44

        .= x01;

        (h . x) = (h1 . (x0 . 1)) by A17

        .= x01;

        then

         A38: x = <*x01, ( 1_ G)*> by A18, A37;

        

        thus (h . x) = (h1 . (x0 . 1)) by A17

        .= ( Product x) by A38, Th45;

      end;

      then

      reconsider M as internal DirectSumComponents of G, I by A25, A27, A33, A34, GROUP_19:def 9;

      set N = <*F1, F2*>;

      ( len N) = 2 by FINSEQ_1: 44;

      then ( dom N) = I by FINSEQ_1: 2, FINSEQ_1:def 3;

      then

      reconsider N as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

      

       A39: for i be Element of I holds (N . i) is Group-Family of (J . i)

      proof

        let i be Element of I;

        per cases by TARSKI:def 2;

          suppose i = 1;

          hence (N . i) is Group-Family of (J . i) by A5, FINSEQ_1: 44;

        end;

          suppose i = 2;

          hence (N . i) is Group-Family of (J . i) by A5, FINSEQ_1: 44;

        end;

      end;

      then for i be Element of I holds (N . i) is multMagma-Family of (J . i);

      then

      reconsider N as multMagma-Family of I, J by Def4;

      reconsider N as Group-Family of I, J by A39, Def5;

      

       A40: for i be Element of I holds (N . i) is internal DirectSumComponents of (M . i), (J . i)

      proof

        let i be Element of I;

        per cases by TARSKI:def 2;

          suppose

           A41: i = 1;

          (M . i) = G by A41, FINSEQ_1: 44;

          hence thesis by A5, A41, FINSEQ_1: 44;

        end;

          suppose

           A42: i = 2;

          for i be Element of I2 holds ( card (F2 . i)) = 1

          proof

            let i be Element of I2;

            the carrier of (F2 . i) = the carrier of ( (1). G) by A2, FUNCOP_1: 7

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

            hence thesis by CARD_1: 30;

          end;

          then

           A43: ( card the carrier of ( sum F2)) = 1 by Th43;

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

          then

          consider a be object such that

           A44: the carrier of ( sum F2) = {a} by A43, CARD_1: 29;

          

           A45: the carrier of ( sum F2) = {( 1_ ( sum F2))} by A44, TARSKI:def 1;

          reconsider Z = the carrier of ( sum F2) as non empty set;

          set h = (Z --> ( 1_ G));

          

           A46: ( dom h) = the carrier of ( sum F2) & ( rng h) c= {( 1_ G)} by FUNCOP_1: 13;

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

          then

          reconsider h as Function of the carrier of ( sum F2), the carrier of ( (1). G) by A46, FUNCT_2: 2;

          for a,b be Element of the carrier of ( sum F2) holds (h . (a * b)) = ((h . a) * (h . b))

          proof

            let a,b be Element of the carrier of ( sum F2);

            

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

            

            thus (h . (a * b)) = ( 1_ G) by FUNCOP_1: 7

            .= (( 1_ ( (1). G)) * ( 1_ ( (1). G))) by A47, GROUP_1:def 4

            .= ((h . a) * ( 1_ ( (1). G))) by A47, FUNCOP_1: 7

            .= ((h . a) * (h . b)) by A47, FUNCOP_1: 7;

          end;

          then

          reconsider h as Homomorphism of ( sum F2), ( (1). G) by GROUP_6:def 6;

          for x1,x2 be object st x1 in the carrier of ( sum F2) & x2 in the carrier of ( sum F2) & (h . x1) = (h . x2) holds x1 = x2

          proof

            let x1,x2 be object;

            assume

             A48: x1 in the carrier of ( sum F2) & x2 in the carrier of ( sum F2) & (h . x1) = (h . x2);

            

            hence x1 = ( 1_ ( sum F2)) by A45, TARSKI:def 1

            .= x2 by A45, A48, TARSKI:def 1;

          end;

          then

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

          for y be object st y in the carrier of ( (1). G) holds ex x be object st x in the carrier of ( sum F2) & y = (h . x)

          proof

            let y be object;

            assume y in the carrier of ( (1). G);

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

            then

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

            set x = ( 1_ ( sum F2));

            take x;

            thus x in the carrier of ( sum F2);

            thus thesis by A50, FUNCOP_1: 7;

          end;

          then ( rng h) = the carrier of ( (1). G) by FUNCT_2: 10;

          then

           A51: h is onto by FUNCT_2:def 3;

          

           A52: (N . i) = F2 & (M . i) = ( (1). G) by A42, FINSEQ_1: 44;

          then

          reconsider h as Homomorphism of ( sum (N . i)), (M . i) by A5, A42;

          reconsider Ni = (N . i) as DirectSumComponents of (M . i), (J . i) by A5, A42, A49, A51, A52, GROUP_19:def 8;

          

           A53: for j be Element of (J . i) holds (Ni . j) is Subgroup of (M . i)

          proof

            let j be Element of (J . i);

            (F2 . j) = ( (1). G) by A2, A5, A42, FUNCOP_1: 7;

            hence (Ni . j) is Subgroup of (M . i) by A52, GROUP_2: 54;

          end;

          

           A54: for x be finite-support Function of (J . i), (M . i) st x in ( sum Ni) holds (h . x) = ( Product x)

          proof

            let x be finite-support Function of (J . i), (M . i);

            assume

             A55: x in ( sum Ni);

            for k be object st k in (J . i) holds (x . k) = ( 1_ (M . i))

            proof

              let k be object;

              assume

               A56: k in (J . i);

              then

              reconsider k0 = k as Element of (J . i);

              reconsider N = (F2 . k0) as 1-sorted by A2, A5, A42, FUNCOP_1: 7;

              

               A57: (F2 . k) = ( (1). G) by A2, A5, A42, A56, FUNCOP_1: 7;

              x in ( sum F2) by A5, A42, A55, FINSEQ_1: 44;

              then (x . k0) in N by A5, A42, GROUP_2: 40, GROUP_19: 5;

              then

               A58: (x . k) in {( 1_ G)} by A57, GROUP_2:def 7;

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

              .= ( 1_ (M . i)) by A42, FINSEQ_1: 44;

              hence thesis by A58, TARSKI:def 1;

            end;

            

            then ( Product x) = ( 1_ (M . i)) by Th44

            .= ( 1_ ( (1). G)) by A42, FINSEQ_1: 44

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

            hence thesis by A5, A42, A52, A55, FUNCOP_1: 7;

          end;

          Ni is internal by A49, A51, A52, A53, A54;

          hence thesis;

        end;

      end;

      

       A59: (I1 \/ I2) = ( Union J) by A4, ZFMISC_1: 75;

      

       A60: ( dom ( Union N)) = ( Union J) by PARTFUN1:def 2

      .= (( dom F1) \/ I2) by A59, PARTFUN1:def 2

      .= (( dom F1) \/ ( dom F2)) by PARTFUN1:def 2;

      for x be object st x in (( dom F1) \/ ( dom F2)) holds (x in ( dom F2) implies (( Union N) . x) = (F2 . x)) & ( not x in ( dom F2) implies (( Union N) . x) = (F1 . x))

      proof

        let x be object;

        assume x in (( dom F1) \/ ( dom F2));

        then

         A61: x in (I1 \/ ( dom F2)) by PARTFUN1:def 2;

        then

         A62: x in (I1 \/ I2) by PARTFUN1:def 2;

        thus x in ( dom F2) implies (( Union N) . x) = (F2 . x)

        proof

          assume

           B32: x in ( dom F2);

          then

          reconsider i = x as Element of ( Union J) by A59, XBOOLE_0:def 3;

          reconsider j = 2 as Element of I by TARSKI:def 2;

          (( Union N) . i) = ((N . j) . i) by A5, B32, Th19

          .= (F2 . i) by FINSEQ_1: 44;

          hence thesis;

        end;

        thus not x in ( dom F2) implies (( Union N) . x) = (F1 . x)

        proof

          assume not x in ( dom F2);

          then

           A63: not x in I2 by PARTFUN1:def 2;

          reconsider i = x as Element of ( Union J) by A59, A61, PARTFUN1:def 2;

          reconsider j = 1 as Element of I by TARSKI:def 2;

          i in (J . j) by A5, A62, A63, XBOOLE_0:def 3;

          

          then (( Union N) . i) = ((N . j) . i) by Th19

          .= (F1 . i) by FINSEQ_1: 44;

          hence thesis;

        end;

      end;

      then (F1 +* F2) = ( Union N) by A60, FUNCT_4:def 1;

      hence thesis by A40, A59, Th40;

    end;