group_19.miz



    begin

    definition

      let D be non empty set;

      let x be Element of D;

      :: original: <*

      redefine

      func <*x*> -> FinSequence of D ;

      coherence

      proof

        for y be object holds y in ( rng <*x*>) implies y in D;

        hence thesis;

      end;

    end

    definition

      let I be set;

      mode Group-Family of I is associative Group-like multMagma-Family of I;

    end

    registration

      let G be Group;

      cluster commutative for Subgroup of G;

      correctness

      proof

        ( (1). G) is commutative;

        hence thesis;

      end;

    end

    theorem :: GROUP_19:1

    

     Th1: for I be set, F be Group-Family of I holds for i be object st i in I holds (F . i) is Group

    proof

      let I be set;

      let F be Group-Family of I;

      let i be object;

      assume

       A1: i in I;

      then ex Fi be Group-like non empty multMagma st Fi = (F . i) by GROUP_7:def 3;

      hence thesis by A1;

    end;

    definition

      let I be non empty set;

      let F be Group-Family of I;

      let i be Element of I;

      :: original: .

      redefine

      func F . i -> Group ;

      coherence by Th1;

    end

    registration

      let I be set;

      let F be Group-Family of I;

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

      correctness

      proof

        now

          let x be Element of ( sum F);

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

          hence x is Function;

        end;

        hence thesis;

      end;

    end

    theorem :: GROUP_19:2

    

     Th2: for I be set, F be Function st I = ( dom F) & for i be object st i in I holds (F . i) is Group holds F is Group-Family of I

    proof

      let I be set;

      let F be Function;

      assume

       A1: I = ( dom F);

      assume

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

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

      now

        let y be set;

        assume y in ( rng F);

        then

        consider i be object such that

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

        thus y is non empty multMagma by A2, A3;

      end;

      then

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

      

       A4: for i be set st i in I holds ex Fi be Group-like non empty multMagma st Fi = (F . i)

      proof

        let i be set;

        assume i in I;

        then

        reconsider Fi = (F . i) as Group-like non empty multMagma by A2;

        take Fi;

        thus thesis;

      end;

      for i be set st i in I holds ex Fi be associative non empty multMagma st Fi = (F . i)

      proof

        let i be set;

        assume i in I;

        then

        reconsider Fi = (F . i) as associative non empty multMagma by A2;

        take Fi;

        thus thesis;

      end;

      hence thesis by A4, GROUP_7:def 3, GROUP_7:def 4;

    end;

    theorem :: GROUP_19:3

    

     Th3: for I be set, F be multMagma-Family of I, a be Element of ( product F) holds ( dom a) = I

    proof

      let I be set, F be multMagma-Family of I, a be Element of ( product F);

      a in ( product F);

      then a in ( product ( Carrier F)) by GROUP_7:def 2;

      hence thesis by PARTFUN1:def 2;

    end;

    ::$Canceled

    theorem :: GROUP_19:5

    

     Th5: for I be non empty set, F be multMagma-Family of I, x be Function, i be Element of I st x in ( product F) holds (x . i) in (F . i)

    proof

      let I be non empty set;

      let F be multMagma-Family of I;

      let x be Function;

      let i be Element of I;

      assume

       A1: x in ( product F);

      

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

      i in I;

      then

       A4: i in ( dom ( Carrier F)) by PARTFUN1:def 2;

      x in ( product ( Carrier F)) by A1, GROUP_7:def 2;

      hence thesis by A2, A4, CARD_3: 9;

    end;

    theorem :: GROUP_19:6

    

     Th6: for G,H be Group, I be Subgroup of H, f be Homomorphism of G, I holds f is Homomorphism of G, H

    proof

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

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

      then

      reconsider g = f as Function of G, H by FUNCT_2: 7;

      now

        let a,b be Element of G;

        

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

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

      end;

      hence thesis by GROUP_6:def 6;

    end;

    begin

    definition

      let I be set;

      let F be Group-Family of I;

      let a be Function;

      :: GROUP_19:def1

      func support (a,F) -> Subset of I means

      : Def1: for i be object holds i in it iff ex G be Group st G = (F . i) & (a . i) <> ( 1_ G) & i in I;

      existence

      proof

        defpred P[ object] means ex G be Group st G = (F . $1) & (a . $1) <> ( 1_ G);

        consider X be set such that

         A1: for x be object holds x in X iff x in I & P[x] from XBOOLE_0:sch 1;

        for x be object st x in X holds x in I by A1;

        then

        reconsider X as Subset of I by TARSKI:def 3;

        take X;

        let i be object;

        thus i in X implies ex G be Group st G = (F . i) & (a . i) <> ( 1_ G) & i in I

        proof

          assume

           A2: i in X;

          then ex G be Group st G = (F . i) & (a . i) <> ( 1_ G) by A1;

          hence thesis by A2;

        end;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let X1,X2 be Subset of I such that

         A2: for i be object holds i in X1 iff ex G be Group st G = (F . i) & (a . i) <> ( 1_ G) & i in I and

         A3: for i be object holds i in X2 iff ex G be Group st G = (F . i) & (a . i) <> ( 1_ G) & i in I;

        now

          let i be object;

          i in X1 iff ex G be Group st G = (F . i) & (a . i) <> ( 1_ G) & i in I by A2;

          hence i in X1 iff i in X2 by A3;

        end;

        hence X1 = X2 by TARSKI: 2;

      end;

    end

    theorem :: GROUP_19:7

    

     Th7: for I be set, F be Group-Family of I, a be Element of ( sum F) holds ex J be finite Subset of I, b be ManySortedSet of J st J = ( support (a,F)) & a = (( 1_ ( product F)) +* b) & (for j be object, G be Group st j in (I \ J) & G = (F . j) holds (a . j) = ( 1_ G)) & (for j be object st j in J holds (a . j) = (b . j))

    proof

      let I be set, F be Group-Family of I, a be Element of ( sum F);

      consider g be Element of ( product ( Carrier F)), J be finite Subset of I, b be ManySortedSet of J such that

       A1: g = ( 1_ ( product F)) & a = (g +* b) & for j be set st j in J holds ex G be Group-like non empty multMagma st G = (F . j) & (b . j) in the carrier of G & (b . j) <> ( 1_ G) by GROUP_7:def 9;

      take J, b;

      

       A2: ( dom b) = J by PARTFUN1:def 2;

      

       A3: ( dom ( 1_ ( product F))) = I by Th3;

      

       A4: for j be object, G be Group st j in (I \ J) & G = (F . j) holds (a . j) = ( 1_ G)

      proof

        let j be object;

        let G be Group;

        assume that

         A6: j in (I \ J) and

         A7: G = (F . j);

        j in ( dom ( 1_ ( product F))) & not j in ( dom b) by A3, A6, XBOOLE_0:def 5;

        

        hence (a . j) = (( 1_ ( product F)) . j) by A1, FUNCT_4: 11

        .= ( 1_ G) by A6, A7, GROUP_7: 6;

      end;

      for j be object holds j in ( support (a,F)) iff j in J

      proof

        let j be object;

        hereby

          assume

           A11: j in ( support (a,F));

          then

          consider G be Group such that

           A12: G = (F . j) & (a . j) <> ( 1_ G) & j in I by Def1;

          assume not j in J;

          then j in (I \ J) by A11, XBOOLE_0:def 5;

          hence contradiction by A4, A12;

        end;

        assume

         A13: j in J;

        then

        consider G be Group-like non empty multMagma such that

         A14: G = (F . j) & (b . j) in the carrier of G & (b . j) <> ( 1_ G) by A1;

        (a . j) <> ( 1_ G) by A1, A2, A13, A14, FUNCT_4: 13;

        hence j in ( support (a,F)) by A13, A14, Def1;

      end;

      hence thesis by A1, A2, A4, FUNCT_4: 13, TARSKI: 2;

    end;

    registration

      let I be set;

      let F be Group-Family of I;

      let a be Element of ( sum F);

      cluster ( support (a,F)) -> finite;

      correctness

      proof

        ex J be finite Subset of I, f be ManySortedSet of J st J = ( support (a,F)) & a = (( 1_ ( product F)) +* f) & (for j be object, G be Group st j in (I \ J) & G = (F . j) holds (a . j) = ( 1_ G)) & (for j be object st j in J holds (a . j) = (f . j)) by Th7;

        hence thesis;

      end;

    end

    definition

      let I be set;

      let G be Group;

      let a be Function of I, G;

      :: GROUP_19:def2

      func support a -> Subset of I means

      : Def2: for i be object holds i in it iff (a . i) <> ( 1_ G) & i in I;

      existence

      proof

        defpred P[ object] means (a . $1) <> ( 1_ G);

        consider X be set such that

         A1: for x be object holds x in X iff x in I & P[x] from XBOOLE_0:sch 1;

        for x be object st x in X holds x in I by A1;

        then

        reconsider X as Subset of I by TARSKI:def 3;

        take X;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let X1,X2 be Subset of I such that

         A2: for i be object holds i in X1 iff (a . i) <> ( 1_ G) & i in I and

         A3: for i be object holds i in X2 iff (a . i) <> ( 1_ G) & i in I;

        now

          let i be object;

          i in X1 iff (a . i) <> ( 1_ G) & i in I by A2;

          hence i in X1 iff i in X2 by A3;

        end;

        hence X1 = X2 by TARSKI: 2;

      end;

    end

    definition

      let I be set;

      let G be Group;

      let a be Function of I, G;

      :: GROUP_19:def3

      attr a is finite-support means

      : Def3: ( support a) is finite;

    end

    registration

      let I be set;

      let G be Group;

      cluster finite-support for Function of I, G;

      correctness

      proof

        set a = (I --> ( 1_ G));

        take a;

        ( support a) = {}

        proof

          assume ( support a) <> {} ;

          then

          consider x be object such that

           A1: x in ( support a) by XBOOLE_0:def 1;

          (a . x) <> ( 1_ G) & x in I by A1, Def2;

          hence contradiction by FUNCOP_1: 7;

        end;

        hence thesis;

      end;

    end

    registration

      let I be set;

      let G be Group;

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

      cluster ( support a) -> finite;

      correctness by Def3;

    end

    definition

      let I be set;

      let G be Group;

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

      :: GROUP_19:def4

      func Product a -> Element of G equals ( Product (a | ( support a)));

      correctness ;

    end

    theorem :: GROUP_19:8

    

     Th8: for I be set, F be Group-Family of I, a be Element of ( product F) holds a in ( sum F) iff ( support (a,F)) is finite

    proof

      let I be set, F be Group-Family of I, a be Element of ( product F);

      thus a in ( sum F) implies ( support (a,F)) is finite;

      assume ( support (a,F)) is finite;

      then

      reconsider J = ( support (a,F)) as finite Subset of I;

      

       A2: ( [#] ( product F)) = ( product ( Carrier F)) by GROUP_7:def 2;

      set k = (a | J);

      

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

      then

       A4: ( dom k) = J by RELAT_1: 62;

      then

      reconsider k as ManySortedSet of J by PARTFUN1:def 2, RELAT_1:def 18;

      set x = (( 1_ ( product F)) +* k);

      

       A5: ( 1_ ( product F)) is Element of ( product ( Carrier F)) by GROUP_7:def 2;

      for j be set st j in J holds ex G be Group-like non empty multMagma st G = (F . j) & (k . j) in the carrier of G & (k . j) <> ( 1_ G)

      proof

        let j be set;

        assume

         A6: j in J;

        then

        consider G be Group such that

         A: G = (F . j) & (a . j) <> ( 1_ G) & j in I by Def1;

        take G;

        thus G = (F . j) by A;

        a in ( product F);

        then (a . j) in G by A, Th5;

        hence (k . j) in the carrier of G by A6, FUNCT_1: 49;

        thus (k . j) <> ( 1_ G) by A, A6, FUNCT_1: 49;

      end;

      then

      reconsider x as Element of ( sum F) by A5, GROUP_7:def 9;

      x in ( sum F);

      then

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

      then

       A11: ( dom x) = I by Th3;

      for i be object st i in ( dom x) holds (x . i) = (a . i)

      proof

        let i be object;

        assume

         A12: i in ( dom x);

        then

        reconsider G = (F . i) as Group by A11, Th1;

        per cases ;

          suppose

           A15: not i in J;

          then not i in ( dom k);

          

          then (x . i) = (( 1_ ( product F)) . i) by FUNCT_4: 11

          .= ( 1_ G) by A11, A12, GROUP_7: 6;

          hence (x . i) = (a . i) by A11, A12, A15, Def1;

        end;

          suppose

           A16: i in J;

          

          hence (x . i) = (k . i) by A4, FUNCT_4: 13

          .= (a . i) by A16, FUNCT_1: 49;

        end;

      end;

      then x = a by A3, A10, Th3, FUNCT_1: 2;

      hence a in ( sum F);

    end;

    theorem :: GROUP_19:9

    

     Th9: for I be set, G be Group, H be Group-Family of I, x be Function of I, G, y be Element of ( product H) st x = y & for i be object st i in I holds (H . i) is Subgroup of G holds ( support x) = ( support (y,H))

    proof

      let I be set, G be Group, H be Group-Family of I, x be Function of I, G, y be Element of ( product H);

      assume that

       A1: x = y and

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

      

       A5: for i be object, Z be Group st i in I & Z = (H . i) holds ( 1_ Z) = ( 1_ G)

      proof

        let i be object;

        let Z be Group;

        assume i in I;

        then (H . i) is Subgroup of G by A2;

        hence thesis by GROUP_2: 44;

      end;

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

      proof

        let i be object;

        

         A6: i in ( support x) iff ((x . i) <> ( 1_ G) & i in I) by Def2;

        hereby

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

          then ex Z be Group st Z = (H . i) & (y . i) <> ( 1_ Z) & i in I by Def1;

          hence i in ( support x) by A1, A5, A6;

        end;

        assume

         A89: i in ( support x);

        then

         A90: (x . i) <> ( 1_ G) & i in I by Def2;

        reconsider Z = (H . i) as Group by A89, Th1;

        ( 1_ Z) = ( 1_ G) by A5, A89;

        hence i in ( support (y,H)) by A1, A90, Def1;

      end;

      hence ( support x) = ( support (y,H)) by TARSKI: 2;

    end;

    theorem :: GROUP_19:10

    

     Th10: for I be set, G be Group, F be Group-Family of I, a be object st a in ( sum F) & for i be object st i in I holds (F . i) is Subgroup of G holds a is finite-support Function of I, G

    proof

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

      assume that

       A1: a in ( sum F) and

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

      a in ( product F) by A1, GROUP_2: 40;

      then

      reconsider b = a as Element of ( product F);

      

       A8: ( dom b) = I by Th3;

      for z be object st z in ( rng b) holds z in ( [#] G)

      proof

        let z be object;

        assume z in ( rng b);

        then

        consider i be object such that

         A9: i in ( dom b) & z = (b . i) by FUNCT_1:def 3;

        i in I by A9, Th3;

        then

        reconsider Z = (F . i) as Subgroup of G by A2;

        reconsider I as non empty set by A9, Th3;

        reconsider i as Element of I by A9, Th3;

        reconsider F as multMagma-Family of I;

        (b . i) in (F . i) by A1, Th5, GROUP_2: 40;

        then (b . i) in Z;

        then (b . i) in G by GROUP_2: 40;

        hence z in ( [#] G) by A9;

      end;

      then ( rng b) c= ( [#] G);

      then

      reconsider b as Function of I, G by A8, FUNCT_2: 2;

      ( support (b,F)) = ( support b) by A2, Th9;

      hence thesis by A1, Def3;

    end;

    theorem :: GROUP_19:11

    for I be non empty set, F be Group-Family of I holds ( support (( 1_ ( product F)),F)) is empty

    proof

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

      for i be object holds not i in ( support (( 1_ ( product F)),F))

      proof

        let i be object;

        assume i in ( support (( 1_ ( product F)),F));

        then ex Z be Group st Z = (F . i) & (( 1_ ( product F)) . i) <> ( 1_ Z) & i in I by Def1;

        hence contradiction by GROUP_7: 6;

      end;

      hence thesis by XBOOLE_0:def 1;

    end;

    theorem :: GROUP_19:12

    

     Th12: for I be non empty set, G be Group, a be Function of I, G st a = (I --> ( 1_ G)) holds ( support a) is empty

    proof

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

      assume

       A1: a = (I --> ( 1_ G));

      for i be object holds not i in ( support a)

      proof

        let i be object;

        assume

         A2: i in ( support a);

        then (a . i) = ( 1_ G) by A1, FUNCOP_1: 7;

        hence contradiction by A2, Def2;

      end;

      hence thesis by XBOOLE_0:def 1;

    end;

    theorem :: GROUP_19:13

    

     Th13: for I be non empty set, G be Group, F be Group-Family of I st for i be Element of I holds (F . i) is Subgroup of G holds ( 1_ ( product F)) = (I --> ( 1_ G))

    proof

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

      assume

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

      

       A2: ( dom ( 1_ ( product F))) = I by Th3;

      

       A3: ( dom (I --> ( 1_ G))) = I by FUNCOP_1: 13;

      for j be object st j in I holds (( 1_ ( product F)) . j) = ((I --> ( 1_ G)) . j)

      proof

        let j be object;

        assume

         A4: j in I;

        then

        reconsider Z = (F . j) as Group by Th1;

        

         A5: (( 1_ ( product F)) . j) = ( 1_ Z) by A4, GROUP_7: 6;

        

         A6: ((I --> ( 1_ G)) . j) = ( 1_ G) by A4, FUNCOP_1: 7;

        reconsider j as Element of I by A4;

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

        hence thesis by A5, A6, GROUP_2: 44;

      end;

      hence thesis by A2, A3, FUNCT_1: 2;

    end;

    theorem :: GROUP_19:14

    for I be non empty set, F be Group-Family of I, G be Group, x be finite-support Function of I, G st ( support x) = {} & for i be object st i in I holds (F . i) is Subgroup of G holds x = ( 1_ ( product F))

    proof

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

      assume that

       A1: ( support x) = {} and

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

      for i be set st i in I holds ex G be Group-like non empty multMagma st G = (F . i) & (x . i) = ( 1_ G)

      proof

        let i be set;

        assume

         A3: i in I;

        then

         A4: (x . i) = ( 1_ G) by A1, Def2;

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

        take Fi;

        thus Fi = (F . i) & (x . i) = ( 1_ Fi) by A4, GROUP_2: 44;

      end;

      hence x = ( 1_ ( product F)) by GROUP_7: 5;

    end;

    theorem :: GROUP_19:15

    

     Th15: for I be set, G be Group, x be finite-support Function of I, G st ( support x) = {} holds ( Product x) = ( 1_ G)

    proof

      let I be set, G be Group, x be finite-support Function of I, G;

      assume ( support x) = {} ;

      then ((x | ( support x)) * ( canFS ( support x))) = ( <*> the carrier of G);

      

      then ( Product (x | ( support x))) = ( Product ( <*> the carrier of G)) by GROUP_17:def 1

      .= ( 1_ G) by GROUP_4: 8;

      hence thesis;

    end;

    theorem :: GROUP_19:16

    

     Th16: for I be non empty set, G be Group, a be finite-support Function of I, G st a = (I --> ( 1_ G)) holds ( Product a) = ( 1_ G)

    proof

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

      assume a = (I --> ( 1_ G));

      then ( support a) is empty by Th12;

      hence thesis by Th15;

    end;

    theorem :: GROUP_19:17

    

     Th17: for I be non empty set, F be Group-Family of I, x be Element of ( product F), i be Element of I, g be Element of (F . i) st x = (( 1_ ( product F)) +* (i,g)) holds ( support (x,F)) c= {i}

    proof

      let I be non empty set, F be Group-Family of I, x be Element of ( product F), i be Element of I, g be Element of (F . i);

      assume

       A1: x = (( 1_ ( product F)) +* (i,g));

      for j be object holds j in ( support (x,F)) implies j in {i}

      proof

        let j be object;

        assume j in ( support (x,F));

        then ex Z be Group st Z = (F . j) & (x . j) <> ( 1_ Z) & j in I by Def1;

        then j = i by A1, GROUP_12: 1;

        hence thesis by TARSKI:def 1;

      end;

      hence thesis;

    end;

    theorem :: GROUP_19:18

    for I be non empty set, F be Group-Family of I, x be Element of ( product F), i be Element of I, g be Element of (F . i) st x = (( 1_ ( product F)) +* (i,g)) & g <> ( 1_ (F . i)) holds ( support (x,F)) = {i}

    proof

      let I be non empty set, F be Group-Family of I, x be Element of ( product F), i be Element of I, g be Element of (F . i);

      assume that

       A1: x = (( 1_ ( product F)) +* (i,g)) and

       A2: g <> ( 1_ (F . i));

      

       A3: ( dom x) = I & (x . i) = g & for j be Element of I st j <> i holds (x . j) = ( 1_ (F . j)) by A1, GROUP_12: 1;

      

       A4: ( support (x,F)) c= {i} by A1, Th17;

      i in ( support (x,F)) by A2, A3, Def1;

      then {i} c= ( support (x,F)) by ZFMISC_1: 31;

      hence thesis by A4, XBOOLE_0:def 10;

    end;

    theorem :: GROUP_19:19

    

     Th19: for I be non empty set, G be Group, i be Element of I, g be Element of G, a be Function of I, G st a = ((I --> ( 1_ G)) +* (i,g)) holds ( support a) c= {i}

    proof

      let I be non empty set, G be Group, i be Element of I, g be Element of G, a be Function of I, G;

      assume

       A1: a = ((I --> ( 1_ G)) +* (i,g));

      for j be object holds j in ( support a) implies j in {i}

      proof

        let j be object;

        assume

         A2: j in ( support a);

        j = i

        proof

          assume j <> i;

          

          then (a . j) = ((I --> ( 1_ G)) . j) by A1, FUNCT_7: 32

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

          hence contradiction by A2, Def2;

        end;

        hence thesis by TARSKI:def 1;

      end;

      hence thesis;

    end;

    theorem :: GROUP_19:20

    

     Th20: for I be non empty set, G be Group, i be Element of I, g be Element of G, a be Function of I, G st a = ((I --> ( 1_ G)) +* (i,g)) & g <> ( 1_ G) holds ( support a) = {i}

    proof

      let I be non empty set, G be Group, i be Element of I, g be Element of G, a be Function of I, G;

      assume that

       A1: a = ((I --> ( 1_ G)) +* (i,g)) and

       A2: g <> ( 1_ G);

      

       A3: ( support a) c= {i} by A1, Th19;

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

      then (a . i) = g by A1, FUNCT_7: 31;

      then i in ( support a) by A2, Def2;

      then {i} c= ( support a) by ZFMISC_1: 31;

      hence thesis by A3, XBOOLE_0:def 10;

    end;

    theorem :: GROUP_19:21

    

     Th21: for I be non empty set, G be Group, a be finite-support Function of I, G, i be Element of I, g be Element of G st a = ((I --> ( 1_ G)) +* (i,g)) holds ( Product a) = g

    proof

      let I be non empty set, G be Group, a be finite-support Function of I, G, i be Element of I, g be Element of G;

      assume

       A1: a = ((I --> ( 1_ G)) +* (i,g));

      

       A2: ( dom (I --> ( 1_ G))) = I by FUNCOP_1: 13;

      per cases ;

        suppose

         A3: g <> ( 1_ G);

        then ( support a) = {i} by A1, Th20;

        then i in ( support a) by TARSKI:def 1;

        then

         A6: i in ( dom (a | ( support a))) by FUNCT_2:def 1;

        ((a | ( support a)) * ( canFS ( support a))) = ((a | ( support a)) * ( canFS {i})) by A1, A3, Th20

        .= ((a | ( support a)) * <*i*>) by FINSEQ_1: 94

        .= <*((a | ( support a)) . i)*> by A6, FINSEQ_2: 34

        .= <*(a . i)*> by A6, FUNCT_1: 47

        .= <*g*> by A1, A2, FUNCT_7: 31;

        

        hence ( Product a) = ( Product <*g*>) by GROUP_17:def 1

        .= g by GROUP_4: 9;

      end;

        suppose

         A7: g = ( 1_ G);

        a = (I --> ( 1_ G))

        proof

          

           A8: ( dom a) = ( dom (I --> ( 1_ G))) by A1, FUNCT_7: 30;

          for j be object st j in I holds (a . j) = ((I --> ( 1_ G)) . j)

          proof

            let j be object;

            assume

             A9: j in I;

            then

             A10: ((I --> ( 1_ G)) . j) = ( 1_ G) by FUNCOP_1: 7;

            per cases ;

              suppose j = i;

              hence thesis by A1, A2, A7, A10, FUNCT_7: 31;

            end;

              suppose j <> i;

              

              then (a . j) = ((I --> ( 1_ G)) . j) by A1, FUNCT_7: 32

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

              hence thesis by A9, FUNCOP_1: 7;

            end;

          end;

          hence thesis by A2, A8, FUNCT_1: 2;

        end;

        hence thesis by A7, Th16;

      end;

    end;

    theorem :: GROUP_19:22

    for I be non empty set, F be Group-Family of I, x be Function, i be Element of I, g be Element of (F . i) holds ( support (x,F)) is finite implies ( support ((x +* (i,g)),F)) is finite

    proof

      let I be non empty set, F be Group-Family of I, x be Function, i be Element of I, g be Element of (F . i);

      reconsider y = (x +* (i,g)) as Function;

      assume

       A1: ( support (x,F)) is finite;

      for j be object holds j in ( support (y,F)) implies j in (( support (x,F)) \/ {i})

      proof

        let j be object;

        assume j in ( support (y,F));

        then

         A2: ex Z be Group st Z = (F . j) & (y . j) <> ( 1_ Z) & j in I by Def1;

        per cases ;

          suppose j = i;

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

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose j <> i;

          then (y . j) = (x . j) by FUNCT_7: 32;

          then j in ( support (x,F)) by A2, Def1;

          hence thesis by XBOOLE_0:def 3;

        end;

      end;

      then ( support (y,F)) c= (( support (x,F)) \/ {i});

      hence thesis by A1;

    end;

    theorem :: GROUP_19:23

    

     Th23: for I be non empty set, G be Group, a be Function of I, G, i be Element of I, g be Element of G holds ( support a) is finite implies ( support (a +* (i,g))) is finite

    proof

      let I be non empty set, G be Group, a be Function of I, G, i be Element of I, g be Element of G;

      reconsider b = (a +* (i,g)) as Function of I, G;

      assume

       A1: ( support a) is finite;

      for j be object holds j in ( support b) implies j in (( support a) \/ {i})

      proof

        let j be object;

        assume j in ( support b);

        then

         A2: (b . j) <> ( 1_ G) & j in I by Def2;

        per cases ;

          suppose i = j;

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

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose i <> j;

          then (b . j) = (a . j) by FUNCT_7: 32;

          then j in ( support a) by A2, Def2;

          hence thesis by XBOOLE_0:def 3;

        end;

      end;

      then ( support b) c= (( support a) \/ {i});

      hence thesis by A1;

    end;

    theorem :: GROUP_19:24

    

     Th24: for I be non empty set, F be Group-Family of I, x be Function, i be Element of I, g be Element of (F . i) holds x in ( product F) implies (x +* (i,g)) in ( product F)

    proof

      let I be non empty set, F be Group-Family of I, x be Function, i be Element of I, g be Element of (F . i);

      assume

       A1: x in ( product F);

      then

       A2: x in ( product ( Carrier F)) by GROUP_7:def 2;

      then

       A3: ( dom x) = ( dom ( Carrier F)) & for j be object st j in ( dom ( Carrier F)) holds (x . j) in (( Carrier F) . j) by CARD_3: 9;

      

       A4: ( dom x) = I by A1, Th3;

      set y = (x +* (i,g));

      

       A6: ( dom y) = I by A4, FUNCT_7: 30;

      

       A7: for j be object st j in ( dom ( Carrier F)) holds (y . j) in (( Carrier F) . j)

      proof

        let j be object;

        assume

         A8: j in ( dom ( Carrier F));

        per cases ;

          suppose

           A9: j = i;

          then

           A10: (y . j) = g by A4, FUNCT_7: 31;

          g in ( [#] (F . i));

          hence thesis by A9, A10, PENCIL_3: 7;

        end;

          suppose j <> i;

          then (y . j) = (x . j) by FUNCT_7: 32;

          hence thesis by A2, A8, CARD_3: 9;

        end;

      end;

      y in ( product ( Carrier F)) by A3, A4, A6, A7, CARD_3: 9;

      hence thesis by GROUP_7:def 2;

    end;

    theorem :: GROUP_19:25

    

     Th25: for I be non empty set, F be Group-Family of I, x be Function, i be Element of I, g be Element of (F . i) holds x in ( sum F) implies (x +* (i,g)) in ( sum F)

    proof

      let I be non empty set, F be Group-Family of I, x be Function, i be Element of I, g be Element of (F . i);

      set y = (x +* (i,g));

      assume

       A1: x in ( sum F);

      then

       A2: y in ( product F) by Th24, GROUP_2: 40;

      for j be object holds j in ( support (y,F)) implies j in (( support (x,F)) \/ {i})

      proof

        let j be object;

        assume j in ( support (y,F));

        then

        consider Z be Group such that

         A3: Z = (F . j) & (y . j) <> ( 1_ Z) & j in I by Def1;

        per cases ;

          suppose j = i;

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

          hence thesis by TARSKI:def 3, XBOOLE_1: 7;

        end;

          suppose j <> i;

          then (x . j) <> ( 1_ Z) & j in I by A3, FUNCT_7: 32;

          then j in ( support (x,F)) by A3, Def1;

          hence thesis by TARSKI:def 3, XBOOLE_1: 7;

        end;

      end;

      then ( support (y,F)) c= (( support (x,F)) \/ {i});

      hence thesis by A1, A2, Th8;

    end;

    theorem :: GROUP_19:26

    for I be non empty set, G be Group, a be finite-support Function of I, G, i be Element of I, g be Element of G holds (a +* (i,g)) is finite-support Function of I, G

    proof

      let I be non empty set, G be Group, a be finite-support Function of I, G, i be Element of I, g be Element of G;

      reconsider b = (a +* (i,g)) as Function of I, G;

      ( support a) is finite;

      then ( support b) is finite by Th23;

      hence thesis by Def3;

    end;

    theorem :: GROUP_19:27

    

     Th27: for I be non empty set, F be Group-Family of I, i be Element of I, a,b be Function st ( dom a) = I & b = (a +* (i,( 1_ (F . i)))) holds ( support (b,F)) = (( support (a,F)) \ {i})

    proof

      let I be non empty set, F be Group-Family of I, i be Element of I, a,b be Function;

      assume that

       A2: ( dom a) = I and

       A3: b = (a +* (i,( 1_ (F . i))));

      for j be object holds j in ( support (b,F)) iff j in (( support (a,F)) \ {i})

      proof

        let j be object;

        hereby

          assume j in ( support (b,F));

          then

          consider Z be Group such that

           A: Z = (F . j) & (b . j) <> ( 1_ Z) & j in I by Def1;

          

           A8: j <> i by A, A2, A3, FUNCT_7: 31;

          then {j} misses {i} by ZFMISC_1: 11;

          then

           A9: not j in {i} by ZFMISC_1: 48;

          (a . j) = (b . j) by A3, A8, FUNCT_7: 32;

          then j in ( support (a,F)) by A, Def1;

          hence j in (( support (a,F)) \ {i}) by A9, XBOOLE_0:def 5;

        end;

        assume j in (( support (a,F)) \ {i});

        then

         A10: j in ( support (a,F)) & not j in {i} by XBOOLE_0:def 5;

        then

        consider Z be Group such that

         A: Z = (F . j) & (a . j) <> ( 1_ Z) & j in I by Def1;

         {j} misses {i} by A10, ZFMISC_1: 50;

        then (b . j) = (a . j) by A3, FUNCT_7: 32;

        hence j in ( support (b,F)) by A, Def1;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: GROUP_19:28

    

     Th28: for I be non empty set, G be Group, i be object, a,b be Function of I, G st i in ( support a) & b = (a +* (i,( 1_ G))) holds ( support b) = (( support a) \ {i})

    proof

      let I be non empty set, G be Group, i be object, a,b be Function of I, G;

      assume that

       A1: i in ( support a) and

       A2: b = (a +* (i,( 1_ G)));

      

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

      

       A5: (b . i) = ( 1_ G) by A1, A2, A4, FUNCT_7: 31;

      for j be object holds j in ( support b) iff j in (( support a) \ {i})

      proof

        let j be object;

        hereby

          assume j in ( support b);

          then

           A7: (b . j) <> ( 1_ G) & j in I by Def2;

          then {j} misses {i} by A5, ZFMISC_1: 11;

          then

           A9: not j in {i} by ZFMISC_1: 48;

          (a . j) = (b . j) by A2, A5, A7, FUNCT_7: 32;

          then j in ( support a) by A7, Def2;

          hence j in (( support a) \ {i}) by A9, XBOOLE_0:def 5;

        end;

        assume j in (( support a) \ {i});

        then

         A10: j in ( support a) & not j in {i} by XBOOLE_0:def 5;

         {j} misses {i} by A10, ZFMISC_1: 50;

        then

         A11: (b . j) = (a . j) by A2, FUNCT_7: 32;

        (a . j) <> ( 1_ G) & j in I by A10, Def2;

        hence j in ( support b) by A11, Def2;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: GROUP_19:29

    for I be non empty set, F be Group-Family of I, i be Element of I, a be Element of ( sum F), b be Function st i in ( support (a,F)) & b = (a +* (i,( 1_ (F . i)))) holds ( card ( support (b,F))) = (( card ( support (a,F))) - 1)

    proof

      let I be non empty set, F be Group-Family of I, i be Element of I, a be Element of ( sum F), b be Function;

      assume that

       A1: i in ( support (a,F)) and

       A2: b = (a +* (i,( 1_ (F . i))));

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

      then ( dom a) = I by Th3;

      then ( support (b,F)) = (( support (a,F)) \ {i}) by A2, Th27;

      

      then ( card ( support (b,F))) = (( card ( support (a,F))) - ( card {i})) by A1, CARD_2: 44, ZFMISC_1: 31

      .= (( card ( support (a,F))) - 1) by CARD_2: 42;

      hence thesis;

    end;

    theorem :: GROUP_19:30

    for I be non empty set, G be Group, i be object, a be finite-support Function of I, G, b be Function of I, G st i in ( support a) & b = (a +* (i,( 1_ G))) holds ( card ( support b)) = (( card ( support a)) - 1)

    proof

      let I be non empty set, G be Group, i be object, a be finite-support Function of I, G, b be Function of I, G;

      assume

       A1: i in ( support a) & b = (a +* (i,( 1_ G)));

      then ( support b) = (( support a) \ {i}) by Th28;

      

      then ( card ( support b)) = (( card ( support a)) - ( card {i})) by A1, CARD_2: 44, ZFMISC_1: 31

      .= (( card ( support a)) - 1) by CARD_2: 42;

      hence thesis;

    end;

    theorem :: GROUP_19:31

    for I be non empty set, F be Group-Family of I, a,b be Element of ( product F) st ( support (a,F)) misses ( support (b,F)) holds (a +* (b | ( support (b,F)))) = (a * b)

    proof

      let I be non empty set, F be Group-Family of I, a,b be Element of ( product F);

      assume

       A1: ( support (a,F)) misses ( support (b,F));

      reconsider c = (a +* (b | ( support (b,F)))) as Function;

      reconsider d = (a * b) as Element of ( product F);

      

       A2: ( dom a) = I by Th3;

      

       A3: ( dom b) = I by Th3;

      

       A5: ( dom c) = (( dom a) \/ ( dom (b | ( support (b,F))))) by FUNCT_4:def 1

      .= I by A2, A3, RELAT_1: 60, XBOOLE_1: 12;

      

       A6: ( dom d) = I by Th3;

      

       A8: ( dom (b | ( support (b,F)))) = ( support (b,F)) by A3, RELAT_1: 62;

      for i be object st i in I holds (c . i) = (d . i)

      proof

        let i be object;

        assume i in I;

        then

        reconsider i as Element of I;

        a in ( product F) & b in ( product F);

        then (a . i) in (F . i) & (b . i) in (F . i) by Th5;

        then

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

        per cases ;

          suppose

           A9: not i in ( support (b,F));

          (c . i) = (a . i) by A8, A9, FUNCT_4: 11

          .= (ai * ( 1_ (F . i))) by GROUP_1:def 4

          .= (ai * bi) by A9, Def1

          .= (d . i) by GROUP_7: 1;

          hence thesis;

        end;

          suppose

           A11: i in ( support (b,F));

          then

           A12: not i in ( support (a,F)) by A1, XBOOLE_0: 3;

          (c . i) = ((b | ( support (b,F))) . i) by A8, A11, FUNCT_4: 13

          .= bi by A11, FUNCT_1: 49

          .= (( 1_ (F . i)) * bi) by GROUP_1:def 4

          .= (ai * bi) by A12, Def1

          .= (d . i) by GROUP_7: 1;

          hence thesis;

        end;

      end;

      hence thesis by A5, A6, FUNCT_1: 2;

    end;

    theorem :: GROUP_19:32

    

     Th32: for I be non empty set, F be Group-Family of I, a,b be Element of ( product F) st ( support (a,F)) misses ( support (b,F)) holds (a * b) = (b * a)

    proof

      let I be non empty set, F be Group-Family of I, a,b be Element of ( product F);

      assume

       A1: ( support (a,F)) misses ( support (b,F));

      reconsider c = (a * b) as Element of ( product F);

      reconsider d = (b * a) as Element of ( product F);

      

       A2: ( dom c) = I by Th3;

      

       A3: ( dom d) = I by Th3;

      for i be object st i in I holds (c . i) = (d . i)

      proof

        let i be object;

        assume i in I;

        then

        reconsider i as Element of I;

        a in ( product F);

        then (a . i) in (F . i) by Th5;

        then

        reconsider ai = (a . i) as Element of (F . i);

        b in ( product F);

        then (b . i) in (F . i) by Th5;

        then

        reconsider bi = (b . i) as Element of (F . i);

        per cases ;

          suppose i in ( support (a,F));

          then

           A4: not i in ( support (b,F)) by A1, XBOOLE_0: 3;

          (c . i) = (ai * bi) by GROUP_7: 1

          .= (ai * ( 1_ (F . i))) by A4, Def1

          .= ai by GROUP_1:def 4

          .= (( 1_ (F . i)) * ai) by GROUP_1:def 4

          .= (bi * ai) by A4, Def1

          .= (d . i) by GROUP_7: 1;

          hence thesis;

        end;

          suppose

           A5: not i in ( support (a,F));

          (c . i) = (ai * bi) by GROUP_7: 1

          .= (( 1_ (F . i)) * bi) by A5, Def1

          .= bi by GROUP_1:def 4

          .= (bi * ( 1_ (F . i))) by GROUP_1:def 4

          .= (bi * ai) by A5, Def1

          .= (d . i) by GROUP_7: 1;

          hence thesis;

        end;

      end;

      hence thesis by A2, A3, FUNCT_1: 2;

    end;

    theorem :: GROUP_19:33

    

     Th33: for I be non empty set, F be Group-Family of I, i be Element of I holds ( ProjGroup (F,i)) is Subgroup of ( sum F)

    proof

      let I be non empty set, F be Group-Family of I, i be Element of I;

      set S = ( ProjGroup (F,i));

      set G = ( sum F);

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

      proof

        let x be object;

        assume

         A1: x in ( [#] S);

        then x in S;

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

        then

        reconsider x as Element of ( product F);

        x in ( ProjSet (F,i)) by A1, GROUP_12:def 2;

        then

        consider h be Element of (F . i) such that

         A3: x = (( 1_ ( product F)) +* (i,h)) by GROUP_12:def 1;

        ( support (x,F)) c= {i} by A3, Th17;

        then x in ( sum F) by Th8;

        hence thesis;

      end;

      then

       A14: ( [#] S) c= ( [#] G);

      

       A16: the multF of G = (the multF of ( product F) || the carrier of G) by GROUP_2:def 5

      .= (the multF of ( product F) | [:( [#] G), ( [#] G):]) by REALSET1:def 2;

      (the multF of G || ( [#] S)) = ((the multF of ( product F) | [:( [#] G), ( [#] G):]) | [:( [#] S), ( [#] S):]) by A16, REALSET1:def 2

      .= (the multF of ( product F) | [:( [#] S), ( [#] S):]) by A14, RELAT_1: 74, ZFMISC_1: 96

      .= (the multF of ( product F) || ( [#] S)) by REALSET1:def 2

      .= the multF of S by GROUP_2:def 5;

      hence thesis by A14, GROUP_2:def 5;

    end;

    theorem :: GROUP_19:34

    

     Th34: for I be non empty set, F,G be Group-Family of I, x,y be Function st for i be Element of I holds ex hi be Homomorphism of (F . i), (G . i) st (y . i) = (hi . (x . i)) holds ( support (y,G)) c= ( support (x,F))

    proof

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

      assume

       A1: for i be Element of I holds ex hi be Homomorphism of (F . i), (G . i) st (y . i) = (hi . (x . i));

      for i be Element of I holds i in ( support (y,G)) implies i in ( support (x,F))

      proof

        let i be Element of I;

        assume

         A2: i in ( support (y,G));

        consider hi be Homomorphism of (F . i), (G . i) such that

         A3: (y . i) = (hi . (x . i)) by A1;

        ex Z be Group st Z = (G . i) & (hi . (x . i)) <> ( 1_ Z) & i in I by A2, A3, Def1;

        then (x . i) <> ( 1_ (F . i)) by GROUP_6: 31;

        hence thesis by Def1;

      end;

      hence thesis;

    end;

    begin

    definition

      let F,G be non-empty non empty Function, h be non empty Function;

      assume

       A1: ( dom F) = ( dom G) = ( dom h) & for i be object st i in ( dom h) holds (h . i) is Function of (F . i), (G . i);

      :: GROUP_19:def5

      func ProductMap (F,G,h) -> Function of ( product F), ( product G) means

      : Def5: for x be Element of ( product F), i be object st i in ( dom h) holds ex hi be Function of (F . i), (G . i) st hi = (h . i) & ((it . x) . i) = (hi . (x . i));

      existence

      proof

        defpred P[ Element of ( product F), Element of ( product G)] means for i be object st i in ( dom h) holds ex hi be Function of (F . i), (G . i) st hi = (h . i) & ($2 . i) = (hi . ($1 . i));

        

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

        proof

          let x be Element of ( product F);

          defpred Q[ object, object] means ex hi be Function of (F . $1), (G . $1) st hi = (h . $1) & $2 = (hi . (x . $1));

          

           A3: for i be object st i in ( dom h) holds ex y be object st Q[i, y]

          proof

            let i be object;

            assume i in ( dom h);

            then

            reconsider hi = (h . i) as Function of (F . i), (G . i) by A1;

            take (hi . (x . i));

            thus thesis;

          end;

          consider y be Function such that

           A4: ( dom y) = ( dom h) & for i be object st i in ( dom h) holds Q[i, (y . i)] from CLASSES1:sch 1( A3);

          now

            let i be object;

            assume

             A5: i in ( dom G);

            then

            consider hi be Function of (F . i), (G . i) such that

             A7: hi = (h . i) & (y . i) = (hi . (x . i)) by A1, A4;

            thus (y . i) in (G . i) by A1, A5, A7, CARD_3: 9, FUNCT_2: 5;

          end;

          then

          reconsider y as Element of ( product G) by A1, A4, CARD_3: 9;

          take y;

          let i be object;

          assume i in ( dom h);

          hence thesis by A4;

        end;

        thus ex p be Function of ( product F), ( product G) st for x be Element of ( product F) holds P[x, (p . x)] from FUNCT_2:sch 3( A2);

      end;

      uniqueness

      proof

        let p,q be Function of ( product F), ( product G) such that

         A8: for f be Element of ( product F), i be object st i in ( dom h) holds ex hi be Function of (F . i), (G . i) st hi = (h . i) & ((p . f) . i) = (hi . (f . i)) and

         A9: for f be Element of ( product F), i be object st i in ( dom h) holds ex hi be Function of (F . i), (G . i) st hi = (h . i) & ((q . f) . i) = (hi . (f . i));

        now

          let f be Element of ( product F);

          

           A10: ( dom (p . f)) = ( dom G) & ( dom (q . f)) = ( dom G) by CARD_3: 9;

          now

            let i be object;

            assume i in ( dom (p . f));

            then

             A12: i in ( dom h) by A1, CARD_3: 9;

            

             A13: ex hi be Function of (F . i), (G . i) st hi = (h . i) & ((p . f) . i) = (hi . (f . i)) by A8, A12;

            ex hi be Function of (F . i), (G . i) st hi = (h . i) & ((q . f) . i) = (hi . (f . i)) by A9, A12;

            hence ((p . f) . i) = ((q . f) . i) by A13;

          end;

          hence (p . f) = (q . f) by A10, FUNCT_1: 2;

        end;

        hence thesis by FUNCT_2:def 8;

      end;

    end

    theorem :: GROUP_19:35

    

     Th35: for F,G be non-empty non empty Function, h be non empty Function st ( dom F) = ( dom G) = ( dom h) & for i be object st i in ( dom h) holds ex hi be Function of (F . i), (G . i) st hi = (h . i) & hi is onto holds ( ProductMap (F,G,h)) is onto

    proof

      let F,G be non-empty non empty Function, h be non empty Function;

      assume that

       A1: ( dom F) = ( dom G) = ( dom h) and

       A2: for i be object st i in ( dom h) holds ex hi be Function of (F . i), (G . i) st hi = (h . i) & hi is onto;

      set p = ( ProductMap (F,G,h));

      

       A4: for i be object st i in ( dom h) holds (h . i) is Function of (F . i), (G . i)

      proof

        let i be object;

        assume i in ( dom h);

        then ex hi be Function of (F . i), (G . i) st hi = (h . i) & hi is onto by A2;

        hence thesis;

      end;

      for y be object st y in ( product G) holds ex x be object st x in ( product F) & y = (p . x)

      proof

        let y be object;

        assume

         A5: y in ( product G);

        then

        reconsider y as Function;

        

         A6: ( dom y) = ( dom G) & for x be object st x in ( dom G) holds (y . x) in (G . x) by A5, CARD_3: 9;

        defpred P[ object, object] means ex i be Element of ( dom h), hi be Function of (F . i), (G . i) st $1 = i & hi = (h . i) & $2 in (F . i) & (y . i) = (hi . $2);

        

         A7: for i be object st i in ( dom F) holds ex x be object st P[i, x]

        proof

          let i be object;

          assume i in ( dom F);

          then

          reconsider i as Element of ( dom h) by A1;

          consider hi be Function of (F . i), (G . i) such that

           A9: hi = (h . i) & hi is onto by A2;

          ( rng hi) = (G . i) by A9, FUNCT_2:def 3;

          then

          consider x be object such that

           A11: x in (F . i) & (y . i) = (hi . x) by A1, A5, CARD_3: 9, FUNCT_2: 11;

          take x;

          thus thesis by A9, A11;

        end;

        consider x be Function such that

         A12: ( dom x) = ( dom F) & for i be object st i in ( dom F) holds P[i, (x . i)] from CLASSES1:sch 1( A7);

        now

          let i be object;

          assume i in ( dom F);

          then ex i0 be Element of ( dom h), hi be Function of (F . i0), (G . i0) st i = i0 & hi = (h . i0) & (x . i) in (F . i0) & (y . i0) = (hi . (x . i)) by A12;

          hence (x . i) in (F . i);

        end;

        then

        reconsider x as Element of ( product F) by A12, CARD_3: 9;

        take x;

        

         A14: ( dom y) = ( dom (p . x)) by A6, CARD_3: 9;

        now

          let i be object;

          assume i in ( dom y);

          then i in ( dom F) by A1, A5, CARD_3: 9;

          then

          consider i0 be Element of ( dom h), hi be Function of (F . i0), (G . i0) such that

           A16: i = i0 & hi = (h . i0) & (x . i) in (F . i0) & (y . i0) = (hi . (x . i)) by A12;

          ex hi be Function of (F . i0), (G . i0) st hi = (h . i0) & ((p . x) . i0) = (hi . (x . i0)) by A1, A4, Def5;

          hence (y . i) = ((p . x) . i) by A16;

        end;

        hence thesis by A14, FUNCT_1: 2;

      end;

      then ( rng p) = ( product G) by FUNCT_2: 10;

      hence thesis by FUNCT_2:def 3;

    end;

    theorem :: GROUP_19:36

    

     Th36: for F,G be non-empty non empty Function, h be non empty Function st ( dom F) = ( dom G) = ( dom h) & for i be object st i in ( dom h) holds ex hi be Function of (F . i), (G . i) st hi = (h . i) & hi is one-to-one holds ( ProductMap (F,G,h)) is one-to-one

    proof

      let F,G be non-empty non empty Function, h be non empty Function;

      assume that

       A1: ( dom F) = ( dom G) = ( dom h) and

       A2: for i be object st i in ( dom h) holds ex hi be Function of (F . i), (G . i) st hi = (h . i) & hi is one-to-one;

      set p = ( ProductMap (F,G,h));

      

       A4: for i be object st i in ( dom h) holds (h . i) is Function of (F . i), (G . i)

      proof

        let i be object;

        assume i in ( dom h);

        then ex hi be Function of (F . i), (G . i) st hi = (h . i) & hi is one-to-one by A2;

        hence thesis;

      end;

      for x1,x2 be object st x1 in ( product F) & x2 in ( product F) & (p . x1) = (p . x2) holds x1 = x2

      proof

        let x1,x2 be object;

        assume

         A5: x1 in ( product F) & x2 in ( product F) & (p . x1) = (p . x2);

        thus x1 = x2

        proof

          reconsider x1, x2 as Element of ( product F) by A5;

          

           A7: ( dom x2) = ( dom F) by CARD_3: 9;

          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 ( dom h) by A1, CARD_3: 9;

            consider hi1 be Function of (F . i), (G . i) such that

             A9: hi1 = (h . i) & ((p . x1) . i) = (hi1 . (x1 . i)) by A1, A4, Def5;

            consider hi2 be Function of (F . i), (G . i) such that

             A10: hi2 = (h . i) & ((p . x2) . i) = (hi2 . (x2 . i)) by A1, A4, Def5;

            

             A14: ex hi be Function of (F . i), (G . i) st hi = (h . i) & hi is one-to-one by A2;

            

             A15: (x1 . i) in (F . i) by A1, CARD_3: 9;

            (x2 . i) in (F . i) by A1, CARD_3: 9;

            hence thesis by A1, A5, A9, A10, A14, A15, FUNCT_2: 19;

          end;

          hence thesis by A7, CARD_3: 9, FUNCT_1: 2;

        end;

      end;

      hence thesis by FUNCT_2: 19;

    end;

    theorem :: GROUP_19:37

    

     Th37: for F,G be non-empty non empty Function, h be non empty Function st ( dom F) = ( dom G) = ( dom h) & for i be object st i in ( dom h) holds ex hi be Function of (F . i), (G . i) st hi = (h . i) & hi is bijective holds ( ProductMap (F,G,h)) is bijective

    proof

      let F,G be non-empty non empty Function, h be non empty Function;

      assume that

       A1: ( dom F) = ( dom G) = ( dom h) and

       A2: for i be object st i in ( dom h) holds ex hi be Function of (F . i), (G . i) st hi = (h . i) & hi is bijective;

      set p = ( ProductMap (F,G,h));

      now

        let i be object;

        assume i in ( dom h);

        then ex hi be Function of (F . i), (G . i) st hi = (h . i) & hi is bijective by A2;

        hence ex hi be Function of (F . i), (G . i) st hi = (h . i) & hi is onto;

      end;

      then

       A3: p is onto by A1, Th35;

      now

        let i be object;

        assume i in ( dom h);

        then ex hi be Function of (F . i), (G . i) st hi = (h . i) & hi is bijective by A2;

        hence ex hi be Function of (F . i), (G . i) st hi = (h . i) & hi is one-to-one;

      end;

      then p is one-to-one by A1, Th36;

      hence thesis by A3;

    end;

    theorem :: GROUP_19:38

    

     Th38: for I be non empty set, F,G be Group-Family of I, h be non empty Function, x be Element of ( product F), y be Element of ( product G) st I = ( dom h) & y = (( ProductMap (( Carrier F),( Carrier G),h)) . x) & for i be Element of I holds (h . i) is Homomorphism of (F . i), (G . i) holds for i be Element of I holds ex hi be Homomorphism of (F . i), (G . i) st hi = (h . i) & (y . i) = (hi . (x . i))

    proof

      let I be non empty set, F,G be Group-Family of I, h be non empty Function, x be Element of ( product F), y be Element of ( product G);

      assume that

       A1: I = ( dom h) and

       A2: y = (( ProductMap (( Carrier F),( Carrier G),h)) . x) and

       A3: for i be Element of I holds (h . i) is Homomorphism of (F . i), (G . i);

      set p = ( ProductMap (( Carrier F),( Carrier G),h));

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

      then

       A6: ( dom ( Carrier F)) = ( dom ( Carrier G)) = ( dom h) by A1, PARTFUN1:def 2;

      

       A7: for i be object st i in ( dom h) holds (h . i) is Function of (( Carrier F) . i), (( Carrier G) . i)

      proof

        let i be object;

        assume i in ( dom h);

        then

        reconsider i as Element of I by A1;

        

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

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

        hence thesis by A3, A8;

      end;

      for i be Element of I holds ex hi be Homomorphism of (F . i), (G . i) st hi = (h . i) & (y . i) = (hi . (x . i))

      proof

        let i be Element of I;

        reconsider x as Element of ( product ( Carrier F)) by GROUP_7:def 2;

        consider hi be Function of (( Carrier F) . i), (( Carrier G) . i) such that

         A13: hi = (h . i) and

         A14: ((p . x) . i) = (hi . (x . i)) by A1, A6, A7, Def5;

        hi is Homomorphism of (F . i), (G . i) by A3, A13;

        hence thesis by A2, A13, A14;

      end;

      hence thesis;

    end;

    definition

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

      assume

       A1: I = ( dom h) & for i be Element of I holds (h . i) is Homomorphism of (F . i), (G . i);

      :: GROUP_19:def6

      func ProductMap (F,G,h) -> Homomorphism of ( product F), ( product G) equals

      : Def6: ( ProductMap (( Carrier F),( Carrier G),h));

      coherence

      proof

        set p = ( ProductMap (( Carrier F),( Carrier G),h));

        

         A3: ( [#] ( product F)) = ( product ( Carrier F)) by GROUP_7:def 2;

        reconsider p as Function of ( product F), ( product G) by A3, GROUP_7:def 2;

        for a,b be Element of ( product F) holds (p . (a * b)) = ((p . a) * (p . b))

        proof

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

          

           A5: ( dom (p . (a * b))) = I by Th3;

          

           A6: ( dom ((p . a) * (p . b))) = I by Th3;

          for i be object st i in I holds ((p . (a * b)) . i) = (((p . a) * (p . b)) . i)

          proof

            let i be object;

            assume i in I;

            then

            reconsider i as Element of I;

            consider hi be Homomorphism of (F . i), (G . i) such that

             A8: hi = (h . i) & ((p . (a * b)) . i) = (hi . ((a * b) . i)) by A1, Th38;

            consider hi1 be Homomorphism of (F . i), (G . i) such that

             A9: hi1 = (h . i) & ((p . a) . i) = (hi1 . (a . i)) by A1, Th38;

            consider hi2 be Homomorphism of (F . i), (G . i) such that

             A10: hi2 = (h . i) & ((p . b) . i) = (hi2 . (b . i)) by A1, Th38;

            a in ( product F);

            then (a . i) in (F . i) by Th5;

            then

            reconsider ai = (a . i) as Element of (F . i);

            b in ( product F);

            then (b . i) in (F . i) by Th5;

            then

            reconsider bi = (b . i) as Element of (F . i);

            ((p . (a * b)) . i) = (hi . (ai * bi)) by A8, GROUP_7: 1

            .= ((hi . ai) * (hi . bi)) by GROUP_6:def 6

            .= (((p . a) * (p . b)) . i) by A8, A9, A10, GROUP_7: 1;

            hence thesis;

          end;

          hence (p . (a * b)) = ((p . a) * (p . b)) by A5, A6, FUNCT_1: 2;

        end;

        hence thesis by GROUP_6:def 6;

      end;

    end

    theorem :: GROUP_19:39

    

     Th39: for I be non empty set, F,G be Group-Family of I, h be non empty Function, x be Element of ( product F), y be Element of ( product G) st I = ( dom h) & y = (( ProductMap (F,G,h)) . x) & for i be Element of I holds (h . i) is Homomorphism of (F . i), (G . i) holds for i be Element of I holds ex hi be Homomorphism of (F . i), (G . i) st hi = (h . i) & (y . i) = (hi . (x . i))

    proof

      let I be non empty set, F,G be Group-Family of I, h be non empty Function, x be Element of ( product F), y be Element of ( product G);

      assume that

       A1: I = ( dom h) and

       A2: y = (( ProductMap (F,G,h)) . x) and

       A3: for i be Element of I holds (h . i) is Homomorphism of (F . i), (G . i);

      y = (( ProductMap (( Carrier F),( Carrier G),h)) . x) by A1, A2, A3, Def6;

      hence thesis by A1, A3, Th38;

    end;

    theorem :: GROUP_19:40

    

     Th40: for I be non empty set, F,G be Group-Family of I, h be non empty Function st I = ( dom h) & for i be Element of I holds ex hi be Homomorphism of (F . i), (G . i) st hi = (h . i) & hi is bijective holds ( ProductMap (F,G,h)) is bijective

    proof

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

      assume

       A1: I = ( dom h) & for i be Element of I holds ex hi be Homomorphism of (F . i), (G . i) st hi = (h . i) & hi is bijective;

      set p = ( ProductMap (( Carrier F),( Carrier G),h));

      

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

      for i be object st i in I holds ex hi be Function of (( Carrier F) . i), (( Carrier G) . i) st hi = (h . i) & hi is bijective

      proof

        let i be object;

        assume i in I;

        then

        reconsider j = i as Element of I;

        consider hi be Homomorphism of (F . j), (G . j) such that

         A5: hi = (h . j) & hi is bijective by A1;

        

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

        

         A7: (( Carrier G) . j) = ( [#] (G . j)) by PENCIL_3: 7;

        then

        reconsider hi as Function of (( Carrier F) . i), (( Carrier G) . i) by A6;

        take hi;

        thus thesis by A5, A7;

      end;

      then

       A8: p is bijective by A1, A3, Th37;

      

       A9: ( [#] ( product F)) = ( product ( Carrier F)) by GROUP_7:def 2;

      

       A10: ( [#] ( product G)) = ( product ( Carrier G)) by GROUP_7:def 2;

      reconsider p as Function of ( product F), ( product G) by A9, GROUP_7:def 2;

      for i be Element of I holds (h . i) is Homomorphism of (F . i), (G . i)

      proof

        let i be Element of I;

        ex hi be Homomorphism of (F . i), (G . i) st hi = (h . i) & hi is bijective by A1;

        hence thesis;

      end;

      then p = ( ProductMap (F,G,h)) by A1, Def6;

      hence thesis by A8, A10;

    end;

    definition

      let I be non empty set, F be Group-Family of I, i be Element of I;

      :: original: ProjGroup

      redefine

      func ProjGroup (F,i) -> strict Subgroup of ( sum F) ;

      correctness by Th33;

    end

    definition

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

      assume

       A1: I = ( dom h) & for i be Element of I holds (h . i) is Homomorphism of (F . i), (G . i);

      :: GROUP_19:def7

      func SumMap (F,G,h) -> Homomorphism of ( sum F), ( sum G) equals

      : Def7: (( ProductMap (F,G,h)) | ( sum F));

      correctness

      proof

        set p = ( ProductMap (F,G,h));

        set s = (p | ( sum F));

        for y be object holds y in ( rng s) implies y in ( [#] ( sum G))

        proof

          let y be object;

          assume

           A4: y in ( rng s);

          then

          consider x be object such that

           A5: x in ( dom s) and

           A6: y = (s . x) by FUNCT_1:def 3;

          ( dom s) c= ( dom p) by RELAT_1: 60;

          then x in ( dom p) by A5;

          then

          reconsider x as Element of ( product F);

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

          

           A8: y = (p . x) by A5, A6, FUNCT_1: 47;

          for i be Element of I holds ex hi be Homomorphism of (F . i), (G . i) st (y . i) = (hi . (x . i))

          proof

            let i be Element of I;

            consider hi be Homomorphism of (F . i), (G . i) such that

             A9: hi = (h . i) & (y . i) = (hi . (x . i)) by A1, A8, Th39;

            thus thesis by A9;

          end;

          then ( support (y,G)) c= ( support (x,F)) by Th34;

          then y in ( sum G) by A5, Th8;

          hence thesis;

        end;

        then ( rng s) c= ( [#] ( sum G));

        then ( [#] ( Image s)) c= ( [#] ( sum G)) by GROUP_6: 44;

        then

         A10: ( Image s) is Subgroup of ( sum G) by GROUP_2: 57;

        s is Homomorphism of ( sum F), ( Image s) by GROUP_6: 49;

        hence thesis by A10, Th6;

      end;

    end

    theorem :: GROUP_19:41

    for I be non empty set, F,G be Group-Family of I, h be non empty Function st I = ( dom h) & for i be Element of I holds ex hi be Homomorphism of (F . i), (G . i) st hi = (h . i) & hi is bijective holds ( SumMap (F,G,h)) is bijective

    proof

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

      assume that

       A1: I = ( dom h) and

       A2: for i be Element of I holds ex hi be Homomorphism of (F . i), (G . i) st hi = (h . i) & hi is bijective;

      

       A3: for i be Element of I holds (h . i) is Homomorphism of (F . i), (G . i)

      proof

        let i be Element of I;

        consider hi be Homomorphism of (F . i), (G . i) such that

         A4: hi = (h . i) & hi is bijective by A2;

        thus thesis by A4;

      end;

      set p = ( ProductMap (F,G,h));

      set s = ( SumMap (F,G,h));

      

       A5: p is bijective by A1, A2, Th40;

      

       A6: s = (p | ( sum F)) by A1, A3, Def7;

      then

       A7: s is one-to-one by A5, FUNCT_1: 52;

      

       A9: ( rng s) c= ( [#] ( sum G));

      for y be object holds y in ( [#] ( sum G)) implies y in ( rng s)

      proof

        let y be object;

        assume

         A10: y in ( [#] ( sum G));

        then y in ( sum G);

        then

         A11: y in ( product G) by GROUP_2: 40;

        then y in ( rng p) by A5, GROUP_6: 61;

        then

        consider x be object such that

         A12: x in ( dom p) and

         A13: y = (p . x) by FUNCT_1:def 3;

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

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

        

         A15: x in ( sum F)

        proof

          assume

           A16: not x in ( sum F);

          for i be Element of I holds ex ki be Homomorphism of (G . i), (F . i) st (x . i) = (ki . (y . i))

          proof

            let i be Element of I;

            consider hi be Homomorphism of (F . i), (G . i) such that

             A18: hi = (h . i) and

             A19: (y . i) = (hi . (x . i)) by A1, A3, A13, Th39;

            consider li be Homomorphism of (F . i), (G . i) such that

             A20: li = (h . i) & li is bijective by A2;

            reconsider ki = (hi " ) as Homomorphism of (G . i), (F . i) by A18, A20, GROUP_6: 62;

            take ki;

            x in ( product F);

            then (x . i) in (F . i) by Th5;

            hence thesis by A18, A19, A20, FUNCT_2: 26;

          end;

          then ( support (x,F)) c= ( support (y,G)) by Th34;

          hence contradiction by A10, A16, Th8;

        end;

        

         A22: x in ( dom s) by A15, FUNCT_2:def 1;

        then (s . x) = (p . x) by A6, FUNCT_1: 47;

        hence thesis by A13, A22, FUNCT_1: 3;

      end;

      hence thesis by A7, A9, TARSKI: 2, GROUP_6: 60;

    end;

    theorem :: GROUP_19:42

    for I be non empty set, F,G be Group-Family of I, h be non empty Function st I = ( dom h) & for i be Element of I holds (h . i) is Homomorphism of (F . i), (G . i) holds for i be Element of I, f be Element of (F . i), hi be Homomorphism of (F . i), (G . i) st hi = (h . i) holds (( SumMap (F,G,h)) . (( 1ProdHom (F,i)) . f)) = (( 1ProdHom (G,i)) . (hi . f))

    proof

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

      assume that

       A1: I = ( dom h) and

       A2: for i be Element of I holds (h . i) is Homomorphism of (F . i), (G . i);

      let i be Element of I, f be Element of (F . i), hi be Homomorphism of (F . i), (G . i);

      assume

       A3: hi = (h . i);

      set x = (( 1ProdHom (F,i)) . f);

      set y = (( SumMap (F,G,h)) . x);

      x in ( ProjGroup (F,i));

      then

       A6: x in ( sum F) by GROUP_2: 40;

      reconsider x as Element of ( product F) by GROUP_2: 42;

      y in ( sum G) by A6, FUNCT_2: 5;

      then

      reconsider y as Element of ( product G) by GROUP_2: 42;

      

       A8: x in ( dom ( SumMap (F,G,h))) by A6, FUNCT_2:def 1;

      ( SumMap (F,G,h)) = (( ProductMap (F,G,h)) | ( sum F)) by A1, A2, Def7;

      then

       A10: y = (( ProductMap (F,G,h)) . x) by A8, FUNCT_1: 47;

      

       A11: ( dom y) = I by Th3;

      

       A13: x = (( 1_ ( product F)) +* (i,f)) by GROUP_12:def 3;

      consider hi0 be Homomorphism of (F . i), (G . i) such that

       A15: hi0 = (h . i) & (y . i) = (hi0 . (x . i)) by A1, A2, A10, Th39;

      

       A16: (y . i) = (hi . f) by A3, A13, A15, GROUP_12: 1;

      

       A17: for j be Element of I st j <> i holds (y . j) = ( 1_ (G . j))

      proof

        let j be Element of I;

        assume j <> i;

        then

         A18: (x . j) = ( 1_ (F . j)) by A13, GROUP_12: 1;

        consider hj be Homomorphism of (F . j), (G . j) such that

         A19: hj = (h . j) & (y . j) = (hj . (x . j)) by A1, A2, A10, Th39;

        thus thesis by A18, A19, GROUP_6: 31;

      end;

      y = (( 1_ ( product G)) +* (i,(hi . f))) by A11, A16, A17, GROUP_12: 1;

      hence thesis by GROUP_12:def 3;

    end;

    begin

    theorem :: GROUP_19:43

    

     Th43: for I be non empty set, G be Group, i be object st i in I holds ex F be Group-Family of I, h be Homomorphism of ( sum F), G st h is bijective & F = ((I --> ( (1). G)) +* ( {i} --> G)) & (for j be Element of I holds ( 1_ (F . j)) = ( 1_ G)) & (for x be Element of ( sum F) holds (h . x) = (x . i)) & for x be Element of ( sum F) holds ex J be finite Subset of I, a be ManySortedSet of J st J c= {i} & J = ( support (x,F)) & (( support (x,F)) = {} or ( support (x,F)) = {i}) & x = (( 1_ ( product F)) +* a) & (for j be Element of I st j in (I \ J) holds (x . j) = ( 1_ (F . j))) & (for j be object st j in J holds (x . j) = (a . j))

    proof

      let I be non empty set, G be Group, i be object;

      assume

       A1: i in I;

      set v = (I --> ( (1). G));

      set w = ( {i} --> G);

      set F = (v +* w);

      

       A4: ( dom F) = (( dom v) \/ ( dom w)) by FUNCT_4:def 1

      .= (( dom v) \/ {i}) by FUNCOP_1: 13

      .= (I \/ {i}) by FUNCOP_1: 13

      .= I by A1, XBOOLE_1: 12, ZFMISC_1: 31;

      

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

      then i in ( dom w) by FUNCOP_1: 13;

      then

       A7: (F . i) = (w . i) by FUNCT_4: 13;

      then

       A8: (F . i) = G by A5, FUNCOP_1: 7;

      

       A9: for j be object st j in (I \ {i}) holds (F . j) = ( (1). G)

      proof

        let j be object;

        assume

         A10: j in (I \ {i});

        then j in ( dom F) by A4;

        then

         A11: j in (( dom v) \/ ( dom w)) by FUNCT_4:def 1;

         not j in ( dom w) by A10, XBOOLE_0:def 5;

        

        hence (F . j) = (v . j) by A11, FUNCT_4:def 1

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

      end;

      for j be object st j in I holds (F . j) is Group

      proof

        let j be object;

        assume

         A12: j in I;

        per cases ;

          suppose j in {i};

          hence (F . j) is Group by A8, TARSKI:def 1;

        end;

          suppose not j in {i};

          then j in (I \ {i}) by A12, XBOOLE_0:def 5;

          hence (F . j) is Group by A9;

        end;

      end;

      then

      reconsider F as Group-Family of I by A4, Th2;

      

       A17: for j be Element of I holds ( 1_ (F . j)) = ( 1_ G)

      proof

        let j be Element of I;

        per cases ;

          suppose j in {i};

          hence ( 1_ (F . j)) = ( 1_ G) by A8, TARSKI:def 1;

        end;

          suppose not j in {i};

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

          then (F . j) = ( (1). G) by A9;

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

        end;

      end;

      defpred P[ Element of ( sum F), Element of G] means $2 = ($1 . i);

      

       A24: for x be Element of ( sum F) holds ex y be Element of G st P[x, y]

      proof

        let x be Element of ( sum F);

        

         B01: x in ( sum F);

        reconsider i as Element of I by A1;

        

         A25: (x . i) in (F . i) by GROUP_2: 40, Th5, B01;

        

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

        then

         A27: i in ( dom w) by FUNCOP_1: 13;

        then i in (( dom v) \/ ( dom w)) by XBOOLE_0:def 3;

        then (F . i) = (w . i) by A27, FUNCT_4:def 1;

        then

        reconsider y = (x . i) as Element of G by A25, A26, FUNCOP_1: 7;

        take y;

        thus thesis;

      end;

      consider h be Function of ( sum F), G such that

       A29: for x be Element of ( sum F) holds P[x, (h . x)] from FUNCT_2:sch 3( A24);

      for y be object st y in ( [#] G) holds ex x be object st x in ( [#] ( sum F)) & y = (h . x)

      proof

        let y be object;

        assume

         A30: y in ( [#] G);

        reconsider i as Element of I by A1;

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

        

         A32: ( 1_ ( product F)) in ( product F);

        

         A33: y in (F . i) by A5, A7, A30, FUNCOP_1: 7;

        then x in ( product F) by A32, Th24;

        then

        reconsider x as Element of ( product F);

        ( support (x,F)) c= {i} by A33, Th17;

        then

         A35: x in ( sum F) by Th8;

        take x;

        thus x in ( [#] ( sum F)) by A35;

        

         A36: ( dom ( 1_ ( product F))) = I by Th3;

        reconsider x as Element of ( sum F) by A35;

        reconsider y as Element of G by A30;

         P[x, y] by A36, FUNCT_7: 31;

        hence thesis by A29;

      end;

      then ( rng h) = ( [#] G) by FUNCT_2: 10;

      then

       A42: h is onto by FUNCT_2:def 3;

      

       A43: for x be Element of ( sum F) holds ( support (x,F)) c= {i}

      proof

        let x be Element of ( sum F);

        now

          let j be object;

          assume

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

          then

          consider Z be Group such that

           A45: Z = (F . j) & (x . j) <> ( 1_ Z) & j in I by Def1;

          assume not j in {i};

          then j in (I \ {i}) by A44, XBOOLE_0:def 5;

          then

           A46: (F . j) = ( (1). G) by A9;

          x in ( sum F);

          then (x . j) in Z by A45, GROUP_2: 40, Th5;

          then (x . j) in {( 1_ G)} by A45, A46, GROUP_2:def 7;

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

          hence contradiction by A45, A46, GROUP_2: 44;

        end;

        hence thesis;

      end;

      for x1,x2 be object st x1 in ( [#] ( sum F)) & x2 in ( [#] ( sum F)) & (h . x1) = (h . x2) holds x1 = x2

      proof

        let x1,x2 be object;

        assume

         A48: x1 in ( [#] ( sum F)) & x2 in ( [#] ( sum F)) & (h . x1) = (h . x2);

        then

        reconsider x1, x2 as Element of ( sum F);

        x1 in ( sum F) & x2 in ( sum F);

        then

         A49: x1 in ( product F) & x2 in ( product F) by GROUP_2: 40;

        then

         A50: ( dom x1) = I & ( dom x2) = I by Th3;

        consider J1 be finite Subset of I, a1 be ManySortedSet of J1 such that

         A51: J1 = ( support (x1,F)) & x1 = (( 1_ ( product F)) +* a1) & (for j be object, G be Group st j in (I \ J1) & G = (F . j) holds (x1 . j) = ( 1_ G)) & (for j be object st j in J1 holds (x1 . j) = (a1 . j)) by Th7;

        consider J2 be finite Subset of I, a2 be ManySortedSet of J2 such that

         A52: J2 = ( support (x2,F)) & x2 = (( 1_ ( product F)) +* a2) & (for j be object, G be Group st j in (I \ J2) & G = (F . j) holds (x2 . j) = ( 1_ G)) & (for j be object st j in J2 holds (x2 . j) = (a2 . j)) by Th7;

        

         A53: ( support (x1,F)) c= {i} by A43;

        

         A54: ( support (x2,F)) c= {i} by A43;

        for j be object st j in ( dom x1) holds (x1 . j) = (x2 . j)

        proof

          let j be object;

          assume j in ( dom x1);

          then

           A56: j in I by A49, Th3;

          then

          reconsider Z = (F . j) as Group by Th1;

          per cases ;

            suppose not j in {i};

            then not j in J1 & not j in J2 by A51, A52, A53, A54;

            then

             A59: j in (I \ J1) & j in (I \ J2) by A56, XBOOLE_0:def 5;

            

            hence (x1 . j) = ( 1_ Z) by A51

            .= (x2 . j) by A52, A59;

          end;

            suppose j in {i};

            then

             A61: j = i by TARSKI:def 1;

            

            hence (x1 . j) = (h . x2) by A29, A48

            .= (x2 . j) by A29, A61;

          end;

        end;

        hence thesis by A50, FUNCT_1: 2;

      end;

      then

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

      for x,y be Element of ( sum F) holds (h . (x * y)) = ((h . x) * (h . y))

      proof

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

        

         A68: for j be set st j in I holds ex Fi be non empty multMagma, xi,yi be Element of Fi st xi = (x . j) & yi = (y . j) & Fi = (F . j) & ((x * y) . j) = (xi * yi)

        proof

          let j be set;

          assume j in I;

          then

          reconsider j as Element of I;

          x in ( sum F);

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

          then

          reconsider x0 = x as Element of ( product F);

          x0 in ( product F);

          then (x0 . j) in (F . j) by Th5;

          then

          reconsider xi = (x0 . j) as Element of (F . j);

          y in ( sum F);

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

          then

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

          y0 in ( product F);

          then (y0 . j) in (F . j) by Th5;

          then

          reconsider yi = (y0 . j) as Element of (F . j);

          ((x * y) . j) = ((x0 * y0) . j) by GROUP_2: 43

          .= (xi * yi) by GROUP_7: 1;

          hence thesis;

        end;

        (h . (x * y)) = ((h . x) * (h . y))

        proof

          consider Fa be non empty multMagma, xa,ya be Element of Fa such that

           A72: xa = (x . i) & ya = (y . i) & Fa = (F . i) & ((x * y) . i) = (xa * ya) by A1, A68;

          

           A74: xa = (h . x) by A29, A72;

          

          thus (h . (x * y)) = (xa * ya) by A29, A72

          .= ((h . x) * (h . y)) by A8, A29, A72, A74;

        end;

        hence thesis;

      end;

      then

      reconsider h as Homomorphism of ( sum F), G by GROUP_6:def 6;

      take F, h;

      thus h is bijective by A42, A62;

      thus F = ((I --> ( (1). G)) +* ( {i} --> G));

      thus for j be Element of I holds ( 1_ (F . j)) = ( 1_ G) by A17;

      thus for x be Element of ( sum F) holds (h . x) = (x . i) by A29;

      let x be Element of ( sum F);

      

       A78: ( support (x,F)) c= {i} by A43;

      

       A79: ( support (x,F)) = {} or ( support (x,F)) = {i}

      proof

        per cases ;

          suppose ( support (x,F)) = {} ;

          hence thesis;

        end;

          suppose ( support (x,F)) <> {} ;

          then

          consider j be object such that

           A82: j in ( support (x,F)) by XBOOLE_0:def 1;

          

           A83: {j} c= ( support (x,F)) by A82, ZFMISC_1: 31;

          j = i by A78, A82, TARSKI:def 1;

          hence thesis by A78, A83, XBOOLE_0:def 10;

        end;

      end;

      consider J be finite Subset of I, a be ManySortedSet of J such that

       A85: J = ( support (x,F)) & x = (( 1_ ( product F)) +* a) & (for j be object, G be Group st j in (I \ J) & G = (F . j) holds (x . j) = ( 1_ G)) & (for j be object st j in J holds (x . j) = (a . j)) by Th7;

      take J, a;

      thus thesis by A79, A85;

    end;

    definition

      let I be non empty set;

      let G be Group;

      :: GROUP_19:def8

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

      : Def8: ex h be Homomorphism of ( sum it ), G st h is bijective;

      existence

      proof

        consider i be object such that

         A1: i in I by XBOOLE_0:def 1;

        consider F be Group-Family of I, h be Homomorphism of ( sum F), G such that

         A2: h is bijective & F = ((I --> ( (1). G)) +* ( {i} --> G)) & (for j be Element of I holds ( 1_ (F . j)) = ( 1_ G)) & (for x be Element of ( sum F) holds (h . x) = (x . i)) & for x be Element of ( sum F) holds ex J be finite Subset of I, a be ManySortedSet of J st J c= {i} & J = ( support (x,F)) & (( support (x,F)) = {} or ( support (x,F)) = {i}) & x = (( 1_ ( product F)) +* a) & (for j be Element of I st j in (I \ J) holds (x . j) = ( 1_ (F . j))) & (for j be object st j in J holds (x . j) = (a . j)) by A1, Th43;

        thus thesis by A2;

      end;

    end

    definition

      let I be non empty set;

      let G be Group;

      let F be DirectSumComponents of G, I;

      :: GROUP_19:def9

      attr F is internal means

      : Def9: (for i be Element of I holds (F . i) is Subgroup of G) & ex h be Homomorphism of ( sum F), G st h is bijective & for x be finite-support Function of I, G st x in ( sum F) holds (h . x) = ( Product x);

    end

    registration

      let I be non empty set;

      let G be Group;

      cluster internal for DirectSumComponents of G, I;

      existence

      proof

        consider i be object such that

         A1: i in I by XBOOLE_0:def 1;

        consider F be Group-Family of I, h be Homomorphism of ( sum F), ( (Omega). G) such that

         A2: h is bijective & F = ((I --> ( (1). ( (Omega). G))) +* ( {i} --> ( (Omega). G))) & (for j be Element of I holds ( 1_ (F . j)) = ( 1_ ( (Omega). G))) & (for x be Element of ( sum F) holds (h . x) = (x . i)) & for x be Element of ( sum F) holds ex J be finite Subset of I, a be ManySortedSet of J st J c= {i} & J = ( support (x,F)) & (( support (x,F)) = {} or ( support (x,F)) = {i}) & x = (( 1_ ( product F)) +* a) & (for j be Element of I st j in (I \ J) holds (x . j) = ( 1_ (F . j))) & (for j be object st j in J holds (x . j) = (a . j)) by A1, Th43;

        reconsider W = (F . i) as Group by A1, Th1;

        reconsider h as Homomorphism of ( sum F), G by Th6;

        h is bijective by A2;

        then

        reconsider F as DirectSumComponents of G, I by Def8;

        set v = (I --> ( (1). ( (Omega). G)));

        set w = ( {i} --> ( (Omega). G));

        

         A8: ( dom F) = (( dom v) \/ ( dom w)) by A2, FUNCT_4:def 1

        .= (( dom v) \/ {i}) by FUNCOP_1: 13

        .= (I \/ {i}) by FUNCOP_1: 13

        .= I by A1, XBOOLE_1: 12, ZFMISC_1: 31;

        

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

        then i in ( dom w) by FUNCOP_1: 13;

        then

         A11: (F . i) = (w . i) by A2, FUNCT_4: 13;

        then

         A12: (F . i) = ( (Omega). G) by A9, FUNCOP_1: 7;

        

         A13: for j be object st j in (I \ {i}) holds (F . j) = ( (1). ( (Omega). G))

        proof

          let j be object;

          assume

           A14: j in (I \ {i});

          then j in ( dom F) by A8;

          then

           A15: j in (( dom v) \/ ( dom w)) by A2, FUNCT_4:def 1;

           not j in ( dom w) by A14, XBOOLE_0:def 5;

          

          hence (F . j) = (v . j) by A2, A15, FUNCT_4:def 1

          .= ( (1). ( (Omega). G)) by A14, FUNCOP_1: 7;

        end;

        

         A21: for j be object st j in I holds (F . j) is Subgroup of G

        proof

          let j be object;

          assume

           A22: j in I;

          then

          reconsider Z = (F . j) as Group by Th1;

          per cases ;

            suppose j in {i};

            hence thesis by A12, TARSKI:def 1;

          end;

            suppose not j in {i};

            then j in (I \ {i}) by A22, XBOOLE_0:def 5;

            then (F . j) is strict Subgroup of ( (Omega). G) by A13;

            hence thesis;

          end;

        end;

        for x be finite-support Function of I, G st x in ( sum F) holds (h . x) = ( Product x)

        proof

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

          assume

           A23: x in ( sum F);

          then

          reconsider x0 = x as Element of ( sum F);

          set p = (x | ( support x));

          

           A24: ( dom p) = ( support x) by FUNCT_2:def 1;

          

           A28: x0 in ( product F) by A23, GROUP_2: 40;

          then

           A29: ( support (x0,F)) = ( support x) by A21, Th9;

          

           A30: (h . x0) = (x0 . i) by A2;

          consider J be finite Subset of I, a be ManySortedSet of J such that

           A31: J c= {i} & J = ( support (x0,F)) & (( support (x0,F)) = {} or ( support (x0,F)) = {i}) & x0 = (( 1_ ( product F)) +* a) & (for j be Element of I st j in (I \ J) holds (x0 . j) = ( 1_ (F . j))) & (for j be object st j in J holds (x0 . j) = (a . j)) by A2;

          per cases by A31;

            suppose

             A32: ( support (x0,F)) = {} ;

            

             A34: (x . i) = ( 1_ W) by A1, A31, A32

            .= ( 1_ ( (Omega). G)) by A9, A11, FUNCOP_1: 7;

            (p * ( canFS ( support x))) = ( <*> the carrier of G) by A29, A32;

            

            then ( Product p) = ( Product ( <*> the carrier of G)) by GROUP_17:def 1

            .= ( 1_ G) by GROUP_4: 8;

            hence thesis by A30, A34, GROUP_2: 44;

          end;

            suppose

             A36: ( support (x0,F)) = {i};

            reconsider xi = (x0 . i) as Element of G by A30, FUNCT_2: 5;

            

             A37: i in ( dom p) by A24, A29, A36, TARSKI:def 1;

            (p * ( canFS ( support x))) = (p * ( canFS {i})) by A21, A28, A36, Th9

            .= (p * <*i*>) by FINSEQ_1: 94

            .= <*(p . i)*> by A37, FINSEQ_2: 34

            .= <*xi*> by A37, FUNCT_1: 47;

            

            then ( Product p) = ( Product <*xi*>) by GROUP_17:def 1

            .= (x0 . i) by GROUP_4: 9;

            hence thesis by A2;

          end;

        end;

        then F is internal by A2, A21;

        hence thesis;

      end;

    end

    begin

    theorem :: GROUP_19:44

    

     Th44: for G be Group, A be non empty Subset of G st for x,y be Element of G st x in A & y in A holds (x * y) = (y * x) holds ( gr A) is commutative

    proof

      let G be Group, A be non empty Subset of G;

      assume

       A1: for x,y be Element of G st x in A & y in A holds (x * y) = (y * x);

      

       A2: for x,y be Element of G, i,j be Element of INT st x in A & y in A holds ((x |^ i) * (y |^ j)) = ((y |^ j) * (x |^ i))

      proof

        let x,y be Element of G, i,j be Element of INT ;

        assume x in A & y in A;

        then (x * y) = (y * x) by A1;

        hence thesis by GROUP_1: 39;

      end;

      

       A3: for y be Element of G, j be Element of INT st y in A holds for F be FinSequence of G, I be FinSequence of INT st ( len F) = ( len I) & ( rng F) c= A holds (( Product (F |^ I)) * (y |^ j)) = ((y |^ j) * ( Product (F |^ I)))

      proof

        let y be Element of G, j be Element of INT ;

        assume

         A4: y in A;

        set x = (y |^ j);

        defpred P[ Nat] means for F be FinSequence of G, I be FinSequence of INT st ( len F) = $1 & ( len F) = ( len I) & ( rng F) c= A holds (( Product (F |^ I)) * x) = (x * ( Product (F |^ I)));

        

         A5: P[ 0 ]

        proof

          let F be FinSequence of G, I be FinSequence of INT such that

           A6: ( len F) = 0 & ( len F) = ( len I) & ( rng F) c= A;

          F = ( <*> ( [#] G)) & I = ( <*> INT ) by A6;

          then (F |^ I) = ( <*> ( [#] G)) by GROUP_4: 21;

          then

           A7: ( Product (F |^ I)) = ( 1_ G) by GROUP_4: 8;

          

          hence (( Product (F |^ I)) * x) = x by GROUP_1:def 4

          .= (x * ( Product (F |^ I))) by A7, GROUP_1:def 4;

        end;

        

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

        proof

          let k be Nat;

          assume

           A9: P[k];

          let F be FinSequence of G, I be FinSequence of INT such that

           A10: ( len F) = (k + 1) & ( len F) = ( len I) & ( rng F) c= A;

          reconsider g = (F /. (k + 1)) as Element of G;

          reconsider i = (I /. (k + 1)) as Element of INT ;

          reconsider F0 = (F | k) as FinSequence of G;

          reconsider I0 = (I | k) as FinSequence of INT ;

          ( rng F0) c= ( rng F) by RELAT_1: 70;

          then

           A11: ( rng F0) c= A by A10;

          reconsider F1 = <*g*> as FinSequence of G;

          reconsider I1 = <*i*> as FinSequence of INT ;

          

           A12: <*( @ i)*> = I1 by GROUP_4:def 1;

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

          then

           A13: (k + 1) in ( dom F) by A10, FINSEQ_1:def 3;

          then (F /. (k + 1)) = (F . (k + 1)) by PARTFUN1:def 6;

          then

           A14: F = (F0 ^ F1) by A10, FINSEQ_3: 55;

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

          then (k + 1) in ( dom I) by A10, FINSEQ_1:def 3;

          then

           A15: (I /. (k + 1)) = (I . (k + 1)) by PARTFUN1:def 6;

          g = (F . (k + 1)) by A13, PARTFUN1:def 6;

          then

           A17: g in A by A10, A13, FUNCT_1: 3;

          k <= ( len F) & k <= ( len I) by A10, XREAL_1: 31;

          then

           A18: ( len F0) = k & ( len I0) = k by FINSEQ_1: 17;

          

           A19: ( len F1) = 1 & ( len I1) = 1 by FINSEQ_1: 39;

          

           A20: (F |^ I) = ((F0 ^ F1) |^ (I0 ^ I1)) by A10, A14, A15, FINSEQ_3: 55

          .= ((F0 |^ I0) ^ (F1 |^ I1)) by A18, A19, GROUP_4: 19

          .= ((F0 |^ I0) ^ <*(g |^ i)*>) by A12, GROUP_4: 22;

          

          hence (( Product (F |^ I)) * x) = ((( Product (F0 |^ I0)) * (g |^ i)) * x) by GROUP_4: 6

          .= (( Product (F0 |^ I0)) * ((g |^ i) * x)) by GROUP_1:def 3

          .= (( Product (F0 |^ I0)) * (x * (g |^ i))) by A2, A4, A17

          .= ((( Product (F0 |^ I0)) * x) * (g |^ i)) by GROUP_1:def 3

          .= ((x * ( Product (F0 |^ I0))) * (g |^ i)) by A9, A11, A18

          .= (x * (( Product (F0 |^ I0)) * (g |^ i))) by GROUP_1:def 3

          .= (x * ( Product (F |^ I))) by A20, GROUP_4: 6;

        end;

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

        hence thesis;

      end;

      

       A22: for x,g be Element of G, i be Element of INT st x in ( gr A) & g in A holds (x * (g |^ i)) = ((g |^ i) * x)

      proof

        let x,g be Element of G, i be Element of INT such that

         A23: x in ( gr A) & g in A;

        consider F be FinSequence of G, I be FinSequence of INT such that

         A24: ( len F) = ( len I) & ( rng F) c= A & ( Product (F |^ I)) = x by A23, GROUP_4: 28;

        thus (x * (g |^ i)) = ((g |^ i) * x) by A3, A23, A24;

      end;

      

       A25: for x be Element of G st x in ( gr A) holds for F be FinSequence of G, I be FinSequence of INT st ( len F) = ( len I) & ( rng F) c= A holds (( Product (F |^ I)) * x) = (x * ( Product (F |^ I)))

      proof

        let x be Element of G;

        assume

         A26: x in ( gr A);

        defpred P[ Nat] means for x be Element of G st x in ( gr A) holds for F be FinSequence of G, I be FinSequence of INT st ( len F) = $1 & ( len F) = ( len I) & ( rng F) c= A holds (( Product (F |^ I)) * x) = (x * ( Product (F |^ I)));

        

         A27: P[ 0 ]

        proof

          let x be Element of G;

          assume x in ( gr A);

          let F be FinSequence of G, I be FinSequence of INT such that

           A29: ( len F) = 0 & ( len F) = ( len I) & ( rng F) c= A;

          F = ( <*> ( [#] G)) & I = ( <*> INT ) by A29;

          then (F |^ I) = ( <*> the carrier of G) by GROUP_4: 21;

          then

           A30: ( Product (F |^ I)) = ( 1_ G) by GROUP_4: 8;

          

          hence (( Product (F |^ I)) * x) = x by GROUP_1:def 4

          .= (x * ( Product (F |^ I))) by A30, GROUP_1:def 4;

        end;

        

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

        proof

          let k be Nat;

          assume

           A32: P[k];

          let x be Element of G;

          assume

           A33: x in ( gr A);

          let F be FinSequence of G, I be FinSequence of INT such that

           A34: ( len F) = (k + 1) & ( len F) = ( len I) & ( rng F) c= A;

          reconsider g = (F /. (k + 1)) as Element of G;

          reconsider i = (I /. (k + 1)) as Element of INT ;

          reconsider F0 = (F | k) as FinSequence of G;

          reconsider I0 = (I | k) as FinSequence of INT ;

          ( rng F0) c= ( rng F) by RELAT_1: 70;

          then

           A35: ( rng F0) c= A by A34;

          reconsider F1 = <*g*> as FinSequence of G;

          reconsider I1 = <*i*> as FinSequence of INT ;

          

           A36: <*( @ i)*> = I1 by GROUP_4:def 1;

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

          then

           A37: (k + 1) in ( dom F) by A34, FINSEQ_1:def 3;

          then (F /. (k + 1)) = (F . (k + 1)) by PARTFUN1:def 6;

          then

           A38: F = (F0 ^ F1) by A34, FINSEQ_3: 55;

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

          then (k + 1) in ( dom I) by A34, FINSEQ_1:def 3;

          then

           A39: (I /. (k + 1)) = (I . (k + 1)) by PARTFUN1:def 6;

          g = (F . (k + 1)) by A37, PARTFUN1:def 6;

          then

           A40: g in A by A34, A37, FUNCT_1: 3;

          k <= ( len F) & k <= ( len I) by A34, XREAL_1: 31;

          then

           A41: ( len F0) = k & ( len I0) = k by FINSEQ_1: 17;

          

           A42: ( len F1) = 1 & ( len I1) = 1 by FINSEQ_1: 39;

          

           A43: (F |^ I) = ((F0 ^ F1) |^ (I0 ^ I1)) by A34, A38, A39, FINSEQ_3: 55

          .= ((F0 |^ I0) ^ (F1 |^ I1)) by A41, A42, GROUP_4: 19

          .= ((F0 |^ I0) ^ <*(g |^ i)*>) by A36, GROUP_4: 22;

          

          hence (( Product (F |^ I)) * x) = ((( Product (F0 |^ I0)) * (g |^ i)) * x) by GROUP_4: 6

          .= (( Product (F0 |^ I0)) * ((g |^ i) * x)) by GROUP_1:def 3

          .= (( Product (F0 |^ I0)) * (x * (g |^ i))) by A22, A33, A40

          .= ((( Product (F0 |^ I0)) * x) * (g |^ i)) by GROUP_1:def 3

          .= ((x * ( Product (F0 |^ I0))) * (g |^ i)) by A32, A33, A35, A41

          .= (x * (( Product (F0 |^ I0)) * (g |^ i))) by GROUP_1:def 3

          .= (x * ( Product (F |^ I))) by A43, GROUP_4: 6;

        end;

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

        hence thesis by A26;

      end;

      for x,y be Element of ( gr A) holds (x * y) = (y * x)

      proof

        let x be Element of ( gr A);

        let y be Element of ( gr A);

        

         A45: x in ( gr A);

        x in G by GROUP_2: 41;

        then

        reconsider x0 = x as Element of G;

        consider F be FinSequence of G, I be FinSequence of INT such that

         A46: ( len F) = ( len I) & ( rng F) c= A & ( Product (F |^ I)) = x0 by A45, GROUP_4: 28;

        y in G by GROUP_2: 41;

        then

        reconsider z = y as Element of G;

        

         A47: z in ( gr A);

        

        thus (x * y) = (( Product (F |^ I)) * z) by A46, GROUP_2: 43

        .= (z * ( Product (F |^ I))) by A25, A46, A47

        .= (y * x) by A46, GROUP_2: 43;

      end;

      hence ( gr A) is commutative by GROUP_1:def 12;

    end;

    theorem :: GROUP_19:45

    

     Th45: for G be Group, H be Subgroup of G, a be FinSequence of G, b be FinSequence of H st a = b holds ( Product a) = ( Product b)

    proof

      let G be Group, H be Subgroup of G;

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

      

       A1: P[ 0 ]

      proof

        let a be FinSequence of G, b be FinSequence of H;

        assume ( len a) = 0 & a = b;

        then a = ( <*> ( [#] G)) & b = ( <*> ( [#] H));

        then ( Product a) = ( 1_ G) & ( Product b) = ( 1_ H) by GROUP_4: 8;

        hence ( Product a) = ( Product b) by GROUP_2: 44;

      end;

      

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

      proof

        let k be Nat;

        assume

         A5: P[k];

        let a be FinSequence of G, b be FinSequence of H;

        assume

         A6: ( len a) = (k + 1) & a = b;

        reconsider g = (a /. (k + 1)) as Element of G;

        reconsider i = (b /. (k + 1)) as Element of H;

        reconsider a0 = (a | k) as FinSequence of G;

        reconsider b0 = (b | k) as FinSequence of H;

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

        then

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

        then

         A8: (a /. (k + 1)) = (a . (k + 1)) by PARTFUN1:def 6;

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

        then

         A9: (k + 1) in ( dom b) by A6, FINSEQ_1:def 3;

        then

         A10: (b /. (k + 1)) = (b . (k + 1)) by PARTFUN1:def 6;

        k <= ( len a) & k <= ( len b) by A6, XREAL_1: 31;

        then ( len a0) = k & ( len b0) = k by FINSEQ_1: 17;

        then

         A13: ( Product a0) = ( Product b0) by A5, A6;

        

         A14: g = (a . (k + 1)) by A7, PARTFUN1:def 6

        .= i by A6, A9, PARTFUN1:def 6;

        

        thus ( Product a) = ( Product (a0 ^ <*g*>)) by A6, A8, FINSEQ_3: 55

        .= (( Product a0) * g) by GROUP_4: 6

        .= (( Product b0) * i) by A13, A14, GROUP_2: 43

        .= ( Product (b0 ^ <*i*>)) by GROUP_4: 6

        .= ( Product b) by A6, A10, FINSEQ_3: 55;

      end;

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

      hence thesis;

    end;

    theorem :: GROUP_19:46

    

     Th46: for G be Group, h be Element of G holds for F be FinSequence of G st for k be Nat st k in ( dom F) holds (h * (F /. k)) = ((F /. k) * h) holds (h * ( Product F)) = (( Product F) * h)

    proof

      let G be Group, h be Element of G;

      defpred P[ Nat] means for F be FinSequence of G st ( len F) = $1 & for i be Nat st i in ( dom F) holds (h * (F /. i)) = ((F /. i) * h) holds (h * ( Product F)) = (( Product F) * h);

      

       A1: P[ 0 ]

      proof

        let F be FinSequence of G;

        assume ( len F) = 0 & for i be Nat st i in ( dom F) holds (h * (F /. i)) = ((F /. i) * h);

        then F = ( <*> ( [#] G));

        then

         A2: ( Product F) = ( 1_ G) by GROUP_4: 8;

        

        hence (h * ( Product F)) = h by GROUP_1:def 4

        .= (( Product F) * h) by A2, GROUP_1:def 4;

      end;

      

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

      proof

        let k be Nat;

        assume

         A4: P[k];

        let F be FinSequence of G;

        assume

         A5: ( len F) = (k + 1) & for i be Nat st i in ( dom F) holds (h * (F /. i)) = ((F /. i) * h);

        reconsider g = (F /. (k + 1)) as Element of G;

        reconsider F0 = (F | k) as FinSequence of G;

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

        then

         A6: (k + 1) in ( dom F) by A5, FINSEQ_1:def 3;

        then

         A7: (F /. (k + 1)) = (F . (k + 1)) by PARTFUN1:def 6;

        

         A8: k <= ( len F) by A5, XREAL_1: 31;

        then

         A9: ( len F0) = k by FINSEQ_1: 17;

        

         A11: ( Seg k) c= ( Seg (k + 1)) by XREAL_1: 31, FINSEQ_1: 5;

        

         A12: ( dom F0) = ( Seg k) by A8, FINSEQ_1: 17;

        

         A13: ( dom F) = ( Seg (k + 1)) by A5, FINSEQ_1:def 3;

        

         A14: for i be Nat st i in ( dom F0) holds (h * (F0 /. i)) = ((F0 /. i) * h)

        proof

          let i be Nat;

          assume

           A15: i in ( dom F0);

          then (F0 /. i) = (F /. i) by PARTFUN1: 80;

          hence thesis by A5, A11, A12, A13, A15;

        end;

        

         A19: ( Product F) = ( Product (F0 ^ <*g*>)) by A5, A7, FINSEQ_3: 55

        .= (( Product F0) * g) by GROUP_4: 6;

        

        hence (h * ( Product F)) = ((h * ( Product F0)) * g) by GROUP_1:def 3

        .= ((( Product F0) * h) * g) by A4, A9, A14

        .= (( Product F0) * (h * g)) by GROUP_1:def 3

        .= (( Product F0) * (g * h)) by A5, A6

        .= (( Product F) * h) by A19, GROUP_1:def 3;

      end;

      

       A20: for i be Nat holds P[i] from NAT_1:sch 2( A1, A3);

      let F be FinSequence of G;

      assume

       A21: for k be Nat st k in ( dom F) holds (h * (F /. k)) = ((F /. k) * h);

      ( len F) is Nat;

      hence thesis by A20, A21;

    end;

    theorem :: GROUP_19:47

    

     Th47: for G be Group, F,F1,F2 be FinSequence of G st ( len F) = ( len F1) & ( len F) = ( len F2) & (for i,j be Nat st i in ( dom F) & j in ( dom F) & i <> j holds ((F1 /. i) * (F2 /. j)) = ((F2 /. j) * (F1 /. i))) & for k be Nat st k in ( dom F) holds (F . k) = ((F1 /. k) * (F2 /. k)) holds ( Product F) = (( Product F1) * ( Product F2))

    proof

      let G be Group;

      defpred P[ Nat] means for F,F1,F2 be FinSequence of G st ( len F) = $1 & ( len F) = ( len F1) & ( len F) = ( len F2) & (for i,j be Nat st i in ( dom F) & j in ( dom F) & i <> j holds ((F1 /. i) * (F2 /. j)) = ((F2 /. j) * (F1 /. i))) & for k be Nat st k in ( dom F) holds (F . k) = ((F1 /. k) * (F2 /. k)) holds ( Product F) = (( Product F1) * ( Product F2));

      

       A1: P[ 0 ]

      proof

        let F,F1,F2 be FinSequence of G;

        assume ( len F) = 0 & ( len F) = ( len F1) & ( len F) = ( len F2) & (for i,j be Nat st i in ( dom F) & j in ( dom F) & i <> j holds ((F1 /. i) * (F2 /. j)) = ((F2 /. j) * (F1 /. i))) & for k be Nat st k in ( dom F) holds (F . k) = ((F1 /. k) * (F2 /. k));

        then F = ( <*> ( [#] G)) & F1 = ( <*> ( [#] G)) & F2 = ( <*> ( [#] G));

        then ( Product F) = ( 1_ G) & ( Product F1) = ( 1_ G) & ( Product F2) = ( 1_ G) by GROUP_4: 8;

        hence thesis by GROUP_1:def 4;

      end;

      

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

      proof

        let k be Nat;

        assume

         A4: P[k];

        let F,F1,F2 be FinSequence of G;

        assume

         A5: ( len F) = (k + 1) & ( len F) = ( len F1) & ( len F) = ( len F2) & (for i,j be Nat st i in ( dom F) & j in ( dom F) & i <> j holds ((F1 /. i) * (F2 /. j)) = ((F2 /. j) * (F1 /. i))) & for k be Nat st k in ( dom F) holds (F . k) = ((F1 /. k) * (F2 /. k));

        reconsider g = (F /. (k + 1)) as Element of G;

        reconsider h = (F1 /. (k + 1)) as Element of G;

        reconsider i = (F2 /. (k + 1)) as Element of G;

        reconsider F0 = (F | k) as FinSequence of G;

        reconsider F10 = (F1 | k) as FinSequence of G;

        reconsider F20 = (F2 | k) as FinSequence of G;

        

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

        then

         A7: (k + 1) in ( dom F) by A5, FINSEQ_1:def 3;

        then

         A8: (F /. (k + 1)) = (F . (k + 1)) by PARTFUN1:def 6;

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

        then (k + 1) in ( dom F1) by A5, FINSEQ_1:def 3;

        then

         A9: (F1 /. (k + 1)) = (F1 . (k + 1)) by PARTFUN1:def 6;

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

        then (k + 1) in ( dom F2) by A5, FINSEQ_1:def 3;

        then

         A10: (F2 /. (k + 1)) = (F2 . (k + 1)) by PARTFUN1:def 6;

        

         A12: k <= ( len F) & k <= ( len F1) & k <= ( len F2) by A5, XREAL_1: 31;

        then

         A13: ( len F0) = k & ( len F10) = k & ( len F20) = k by FINSEQ_1: 17;

        

         A15: ( Seg k) c= ( Seg (k + 1)) by FINSEQ_1: 5, XREAL_1: 31;

        

         A16: ( dom F0) = ( Seg k) by A12, FINSEQ_1: 17;

        then

         A17: ( dom F10) = ( dom F0) by A12, FINSEQ_1: 17;

        

         A18: ( dom F20) = ( dom F0) by A12, A16, FINSEQ_1: 17;

        

         A19: ( dom F) = ( Seg (k + 1)) by A5, FINSEQ_1:def 3;

        

         A22: for i,j be Nat st i in ( dom F0) & j in ( dom F0) & i <> j holds ((F10 /. i) * (F20 /. j)) = ((F20 /. j) * (F10 /. i))

        proof

          let i,j be Nat;

          assume

           A23: i in ( dom F0) & j in ( dom F0) & i <> j;

          then

           A27: (F10 /. i) = (F1 /. i) by A17, PARTFUN1: 80;

          

          hence ((F10 /. i) * (F20 /. j)) = ((F1 /. i) * (F2 /. j)) by A18, A23, PARTFUN1: 80

          .= ((F2 /. j) * (F1 /. i)) by A5, A15, A16, A19, A23

          .= ((F20 /. j) * (F10 /. i)) by A18, A23, A27, PARTFUN1: 80;

        end;

        

         A29: for k be Nat st k in ( dom F0) holds (F0 . k) = ((F10 /. k) * (F20 /. k))

        proof

          let k be Nat;

          assume

           A30: k in ( dom F0);

          then

           A34: (F10 /. k) = (F1 /. k) by A17, PARTFUN1: 80;

          

          thus (F0 . k) = (F . k) by A30, FUNCT_1: 47

          .= ((F1 /. k) * (F2 /. k)) by A5, A15, A16, A19, A30

          .= ((F10 /. k) * (F20 /. k)) by A18, A30, A34, PARTFUN1: 80;

        end;

        

         A36: for i be Nat st i in ( dom F20) holds (h * (F20 /. i)) = ((F20 /. i) * h)

        proof

          let i be Nat;

          assume

           A37: i in ( dom F20);

          then

           A40: (F20 /. i) = (F2 /. i) by PARTFUN1: 80;

          ( dom F20) = ( Seg k) by A12, FINSEQ_1: 17;

          then

           A41: 1 <= i & i <= k by A37, FINSEQ_1: 1;

          (k + 0 ) < (k + 1) by XREAL_1: 8;

          hence thesis by A5, A6, A15, A16, A18, A19, A37, A40, A41;

        end;

        

         A43: g = (F . (k + 1)) by A7, PARTFUN1:def 6

        .= (h * i) by A5, A7;

        

         A44: ( Product F1) = ( Product (F10 ^ <*h*>)) by A5, A9, FINSEQ_3: 55

        .= (( Product F10) * h) by GROUP_4: 6;

        

         A45: ( Product F2) = ( Product (F20 ^ <*i*>)) by A5, A10, FINSEQ_3: 55

        .= (( Product F20) * i) by GROUP_4: 6;

        

        thus ( Product F) = ( Product (F0 ^ <*g*>)) by A5, A8, FINSEQ_3: 55

        .= (( Product F0) * g) by GROUP_4: 6

        .= ((( Product F10) * ( Product F20)) * (h * i)) by A4, A13, A22, A29, A43

        .= (((( Product F10) * ( Product F20)) * h) * i) by GROUP_1:def 3

        .= ((( Product F10) * (( Product F20) * h)) * i) by GROUP_1:def 3

        .= ((( Product F10) * (h * ( Product F20))) * i) by A36, Th46

        .= (((( Product F10) * h) * ( Product F20)) * i) by GROUP_1:def 3

        .= (( Product F1) * ( Product F2)) by A44, A45, GROUP_1:def 3;

      end;

      for i be Nat holds P[i] from NAT_1:sch 2( A1, A3);

      hence thesis;

    end;

    theorem :: GROUP_19:48

    

     Th48: for G be Group, a be FinSequence of G st for i be object st i in ( dom a) holds (a . i) = ( 1_ G) holds ( Product a) = ( 1_ G)

    proof

      let G be Group, a be FinSequence of G;

      assume

       A1: for i be object st i in ( dom a) holds (a . i) = ( 1_ G);

      set n = ( len a);

      a = (n |-> ( 1_ G))

      proof

        (n |-> ( 1_ G)) = (( Seg n) --> ( 1_ G)) by FINSEQ_2:def 2;

        then

         A2: ( dom (n |-> ( 1_ G))) = ( Seg n) by FUNCOP_1: 13;

        

         A3: ( dom a) = ( Seg n) by FINSEQ_1:def 3;

        for i be object st i in ( dom a) holds (a . i) = ((n |-> ( 1_ G)) . i)

        proof

          let i be object;

          assume

           A4: i in ( dom a);

          then i in ( Seg n) by FINSEQ_1:def 3;

          then ((n |-> ( 1_ G)) . i) = ( 1_ G) by FINSEQ_2: 57;

          hence thesis by A1, A4;

        end;

        hence thesis by A2, A3, FUNCT_1: 2;

      end;

      

      then ( Product a) = (( 1_ G) |^ n) by GROUP_4: 12

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

      hence thesis;

    end;

    theorem :: GROUP_19:49

    

     Th49: for I be finite set, G be Group, a be the carrier of G -valued totalI -defined Function st for i be object st i in I holds (a . i) = ( 1_ G) holds ( Product a) = ( 1_ G)

    proof

      let I be finite set, G be Group, a be the carrier of G -valued totalI -defined Function;

      assume

       A1: for i be object st i in I holds (a . i) = ( 1_ G);

      set cs = ( canFS I);

      set acs = (a * cs);

      

       A2: ( rng acs) c= the carrier of G;

      

       A3: I = ( dom a) & ( rng cs) = I by FUNCT_2:def 3, PARTFUN1:def 2;

      then ( dom acs) = ( dom cs) by RELAT_1: 27;

      then ( dom acs) = ( Seg ( len cs)) by FINSEQ_1:def 3;

      then acs is FinSequence by FINSEQ_1:def 2;

      then

      reconsider acs as FinSequence of G by A2, FINSEQ_1:def 4;

      

       A4: ( Product a) = ( Product acs) by GROUP_17:def 1;

      for i be object st i in ( dom acs) holds (acs . i) = ( 1_ G)

      proof

        let i be object;

        assume

         A5: i in ( dom acs);

        then i in ( dom cs) by A3, RELAT_1: 27;

        then (cs . i) in ( rng cs) by FUNCT_1: 3;

        then (a . (cs . i)) = ( 1_ G) by A1;

        hence thesis by A5, FUNCT_1: 12;

      end;

      hence thesis by A4, Th48;

    end;

    theorem :: GROUP_19:50

    

     Th50: for A be finite set, B be non empty set, f be B -valued totalA -defined Function holds (f * ( canFS A)) is FinSequence of B

    proof

      let A be finite set, B be non empty set, f be B -valued totalA -defined Function;

      

       A1: ( rng (f * ( canFS A))) c= B;

      A = ( dom f) & ( rng ( canFS A)) = A by FUNCT_2:def 3, PARTFUN1:def 2;

      then ( dom (f * ( canFS A))) = ( dom ( canFS A)) by RELAT_1: 27;

      then ( dom (f * ( canFS A))) = ( Seg ( len ( canFS A))) by FINSEQ_1:def 3;

      then (f * ( canFS A)) is FinSequence by FINSEQ_1:def 2;

      hence thesis by A1, FINSEQ_1:def 4;

    end;

    theorem :: GROUP_19:51

    

     Th51: for I be non empty set, G be Group, a be finite-support Function of I, G, W be finite Subset of I st ( support a) c= W & for i,j be Element of I holds ((a . i) * (a . j)) = ((a . j) * (a . i)) holds ( Product a) = ( Product (a | W))

    proof

      let I be non empty set, G be Group, a be finite-support Function of I, G, W be finite Subset of I;

      assume that

       A1: ( support a) c= W and

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

      reconsider ra = ( rng a) as non empty Subset of G;

      for x,y be Element of G st x in ra & y in ra holds (x * y) = (y * x)

      proof

        let x,y be Element of G;

        assume

         A3: x in ra & y in ra;

        then

        consider i be Element of I such that

         A4: x = (a . i) by FUNCT_2: 113;

        consider j be Element of I such that

         A5: y = (a . j) by A3, FUNCT_2: 113;

        thus thesis by A2, A4, A5;

      end;

      then

      reconsider H = ( gr ra) as non empty commutative Subgroup of G by Th44;

      reconsider A = ( support a) as finite Subset of W by A1;

      reconsider B = (W \ ( support a)) as finite Subset of W by XBOOLE_1: 36;

      per cases ;

        suppose

         A6: A = {} ;

        then ((a | A) * ( canFS A)) = {} ;

        

        then

         A7: ( Product a) = ( Product ( <*> the carrier of G)) by GROUP_17:def 1

        .= ( 1_ G) by GROUP_4: 8;

        for i be object st i in W holds ((a | W) . i) = ( 1_ G)

        proof

          let i be object;

          assume

           A8: i in W;

          then (a . i) = ( 1_ G) by A6, Def2;

          hence ((a | W) . i) = ( 1_ G) by A8, FUNCT_1: 49;

        end;

        hence ( Product a) = ( Product (a | W)) by A7, Th49;

      end;

        suppose

         A11: A <> {} ;

        per cases ;

          suppose B = {} ;

          then W c= A by XBOOLE_1: 37;

          then A = W by XBOOLE_0:def 10;

          hence ( Product a) = ( Product (a | W));

        end;

          suppose

           A12: B <> {} ;

          ( rng a) c= ( [#] H) by GROUP_4:def 4;

          then

           A14: a is Function of I, H by FUNCT_2: 6;

          then

          reconsider fa = (a | ( support a)) as the carrier of H -valued totalA -defined Function;

          reconsider B0 = B as finite Subset of I;

          reconsider fb = (a | B0) as the carrier of H -valued totalB0 -defined Function by A14;

          

           A15: (A \/ B) = W by XBOOLE_1: 45;

          then

          reconsider fab = (a | W) as the carrier of H -valued total(A \/ B) -defined Function by A14;

          

           A16: A misses B by XBOOLE_1: 79;

          

           A17: ( dom fab) = (A \/ B) by A15, FUNCT_2:def 1

          .= (( dom fa) \/ B) by FUNCT_2:def 1

          .= (( dom fa) \/ ( dom fb)) by FUNCT_2:def 1;

          

           A18: for x be object st x in ( dom fab) holds (fab . x) = ((fa +* fb) . x)

          proof

            let x be object;

            assume

             A19: x in ( dom fab);

            per cases by A17, XBOOLE_0:def 3;

              suppose

               A22: x in ( dom fa);

              

               A24: not x in ( dom fb)

              proof

                assume x in ( dom fb);

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

                hence contradiction by XBOOLE_0:def 7, XBOOLE_1: 79;

              end;

              

              thus (fab . x) = (a . x) by A19, FUNCT_1: 47

              .= (fa . x) by A22, FUNCT_1: 47

              .= ((fa +* fb) . x) by A24, FUNCT_4: 11;

            end;

              suppose

               A25: x in ( dom fb);

              

              thus (fab . x) = (a . x) by A19, FUNCT_1: 47

              .= (fb . x) by A25, FUNCT_1: 47

              .= ((fa +* fb) . x) by A25, FUNCT_4: 13;

            end;

          end;

          

           A27: ( dom (fa +* fb)) = (( dom fa) \/ ( dom fb)) by FUNCT_4:def 1;

          reconsider fca = (fa * ( canFS A)) as FinSequence of H by Th50;

          reconsider fcsa = (fa * ( canFS ( support a))) as FinSequence of G by Th50;

          reconsider fcab = (fab * ( canFS (A \/ B))) as FinSequence of H by Th50;

          reconsider fcw = ((a | W) * ( canFS W)) as FinSequence of G by Th50;

          

           A31: ( Product fa) = ( Product fca) by GROUP_17:def 1

          .= ( Product fcsa) by Th45

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

          

           A35: fcab = fcw by XBOOLE_1: 45;

          

           A36: ( Product fab) = ( Product fcab) by GROUP_17:def 1

          .= ( Product fcw) by A35, Th45

          .= ( Product (a | W)) by GROUP_17:def 1;

          for i be object st i in B0 holds (fb . i) = ( 1_ H)

          proof

            let i be object;

            assume

             A38: i in B0;

            then

             A39: i in W & not i in ( support a) by XBOOLE_0:def 5;

            i in ( dom fb) by A38, FUNCT_2:def 1;

            

            hence (fb . i) = (a . i) by FUNCT_1: 47

            .= ( 1_ G) by A39, Def2

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

          end;

          

          then

           A41: ( Product fb) = ( 1_ H) by Th49

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

          

          thus ( Product (a | W)) = (( Product fa) * ( Product fb)) by A11, A12, A16, A17, A18, A27, A36, FUNCT_1: 2, GROUP_17: 8

          .= (( Product a) * ( 1_ G)) by A31, A41, GROUP_2: 43

          .= ( Product a) by GROUP_1:def 4;

        end;

      end;

    end;

    theorem :: GROUP_19:52

    for I be non empty set, G be Group, a be finite-support Function of I, G, W be finite Subset of I st ( support a) c= W holds ex aW be finite-support Function of W, G st aW = (a | W) & ( support a) = ( support aW) & ( Product a) = ( Product aW)

    proof

      let I be non empty set, G be Group, a be finite-support Function of I, G, W be finite Subset of I;

      assume

       A1: ( support a) c= W;

      

       A2: for i be object holds i in ( support a) iff i in ( support (a | W))

      proof

        let i be object;

        hereby

          assume

           A3: i in ( support a);

          then

           A4: (a . i) <> ( 1_ G) & i in I by Def2;

          ((a | W) . i) = (a . i) by A1, A3, FUNCT_1: 49;

          hence i in ( support (a | W)) by A1, A3, A4, Def2;

        end;

        assume

         A6: i in ( support (a | W));

        then

         A7: ((a | W) . i) <> ( 1_ G) & i in W by Def2;

        ((a | W) . i) = (a . i) by A6, FUNCT_1: 49;

        hence i in ( support a) by A7, Def2;

      end;

      ( support (a | W)) is finite;

      then

      reconsider aW = (a | W) as finite-support Function of W, G by Def3;

      take aW;

      (aW | ( support aW)) = ((a | W) | ( support a)) by A2, TARSKI: 2

      .= (a | ( support a)) by A1, RELAT_1: 74;

      hence thesis by A2, TARSKI: 2;

    end;

    theorem :: GROUP_19:53

    

     Th53: for I be non empty set, G be Group, F be Group-Family of I, sx,sy be Element of ( sum F), x,y,xy be finite-support Function of I, G st (for i be Element of I holds (F . i) is Subgroup of G) & (for i,j be Element of I, gi,gj be Element of G st i <> j & gi in (F . i) & gj in (F . j) holds (gi * gj) = (gj * gi)) & sx = x & sy = y & (sx * sy) = xy holds ( Product xy) = (( Product x) * ( Product y))

    proof

      let I be non empty set, G be Group, F be Group-Family of I, sx,sy be Element of ( sum F), x,y,xy be finite-support Function of I, G;

      assume that

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

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

       A3: sx = x & sy = y & (sx * sy) = xy;

      reconsider W = (( support x) \/ ( support y)) as finite Subset of I;

      

       A9: sx in ( sum F);

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

      then

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

      

       A10: sy in ( sum F);

      then y in ( product F) by A3, GROUP_2: 40;

      then

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

      

       A11: (sx * sy) in ( sum F);

      then xy in ( product F) by A3, GROUP_2: 40;

      then

      reconsider pxy = xy as Element of ( product F);

      for i be object st i in ( support xy) holds i in W

      proof

        let i be object;

        assume

         A12: i in ( support xy);

        i in W

        proof

          assume

           A13: not i in W;

          reconsider i as Element of I by A12;

          

           A14: not i in ( support x) & not i in ( support y) by A13, XBOOLE_0:def 3;

          then

           A15: (x . i) = ( 1_ G) by Def2;

          

           A16: (y . i) = ( 1_ G) by A14, Def2;

          

           A17: (F . i) is Subgroup of G by A1;

          (x . i) in (F . i) by A3, A9, Th5, GROUP_2: 40;

          then

          reconsider fxi = (x . i) as Element of (F . i);

          (y . i) in (F . i) by A3, A10, Th5, GROUP_2: 40;

          then

          reconsider fyi = (y . i) as Element of (F . i);

          (xy . i) = ((px * py) . i) by A3, GROUP_2: 43

          .= (fxi * fyi) by GROUP_7: 1

          .= ((x . i) * (y . i)) by A17, GROUP_2: 43

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

          hence contradiction by A12, Def2;

        end;

        hence i in W;

      end;

      then

       A22: ( support xy) c= W;

      

       A23: for a be Function of I, G, i,j be Element of I st a in ( product F) holds ((a . i) * (a . j)) = ((a . j) * (a . i))

      proof

        let a be Function of I, G;

        let i,j be Element of I;

        assume

         A24: a in ( product F);

        then

         A25: (a . i) in (F . i) by Th5;

        

         A26: (a . j) in (F . j) by A24, Th5;

        per cases ;

          suppose i = j;

          hence thesis;

        end;

          suppose i <> j;

          hence thesis by A2, A25, A26;

        end;

      end;

      for i,j be Element of I holds ((x . i) * (x . j)) = ((x . j) * (x . i)) by A3, A9, A23, GROUP_2: 40;

      then

       A28: ( Product x) = ( Product (x | W)) by Th51, XBOOLE_1: 7;

      for i,j be Element of I holds ((y . i) * (y . j)) = ((y . j) * (y . i)) by A3, A10, A23, GROUP_2: 40;

      then

       A34: ( Product y) = ( Product (y | W)) by Th51, XBOOLE_1: 7;

      for i,j be Element of I holds ((xy . i) * (xy . j)) = ((xy . j) * (xy . i)) by A3, A11, A23, GROUP_2: 40;

      then

       A40: ( Product xy) = ( Product (xy | W)) by A22, Th51;

      set cs = ( canFS W);

      reconsider wx = ((x | W) * cs) as FinSequence of G by Th50;

      reconsider wy = ((y | W) * cs) as FinSequence of G by Th50;

      reconsider wxy = ((xy | W) * cs) as FinSequence of G by Th50;

      

       A41: ( rng cs) = W by FUNCT_2:def 3;

      W = ( dom (x | W)) & W = ( dom (y | W)) & W = ( dom (xy | W)) by PARTFUN1:def 2;

      then

       A43: ( dom cs) = ( dom wx) & ( dom cs) = ( dom wy) & ( dom cs) = ( dom wxy) by A41, RELAT_1: 27;

      then ( dom cs) = ( Seg ( len wx)) & ( dom cs) = ( Seg ( len wy)) & ( dom cs) = ( Seg ( len wxy)) by FINSEQ_1:def 3;

      then

       A45: ( len wxy) = ( len wx) & ( len wxy) = ( len wy) by FINSEQ_1: 6;

      

       A50: ( Product (x | W)) = ( Product wx) by GROUP_17:def 1;

      

       A51: ( Product (y | W)) = ( Product wy) by GROUP_17:def 1;

      

       A55: for i,j be Nat st i in ( dom wxy) & j in ( dom wxy) & i <> j holds ((wx /. i) * (wy /. j)) = ((wy /. j) * (wx /. i))

      proof

        let i,j be Nat;

        assume

         A56: i in ( dom wxy) & j in ( dom wxy) & i <> j;

        then

         A57: (cs . i) in ( rng cs) & (cs . j) in ( rng cs) by A43, FUNCT_1: 3;

        then

         A59: (cs . i) in W & (cs . j) in W;

        

         A60: (wx /. i) = (wx . i) by A43, A56, PARTFUN1:def 6

        .= ((x | W) . (cs . i)) by A43, A56, FUNCT_1: 12

        .= (x . (cs . i)) by A57, FUNCT_1: 49;

        

         A61: (wy /. j) = (wy . j) by A43, A56, PARTFUN1:def 6

        .= ((y | W) . (cs . j)) by A43, A56, FUNCT_1: 12

        .= (y . (cs . j)) by A57, FUNCT_1: 49;

        reconsider i0 = (cs . i) as Element of I by A59;

        reconsider j0 = (cs . j) as Element of I by A59;

        

         A64: (x . i0) in (F . i0) by A3, A9, Th5, GROUP_2: 40;

        reconsider gi = (x . i0) as Element of G;

        

         A65: (y . j0) in (F . j0) by A3, A10, Th5, GROUP_2: 40;

        reconsider gj = (y . j0) as Element of G;

        thus thesis by A2, A43, A56, A60, A61, A64, A65, FUNCT_1:def 4;

      end;

      

       A67: for i be Nat st i in ( dom wxy) holds (wxy . i) = ((wx /. i) * (wy /. i))

      proof

        let i be Nat;

        assume

         A68: i in ( dom wxy);

        

         A70: (cs . i) in ( rng cs) by A43, A68, FUNCT_1: 3;

        then

         A71: (cs . i) in W;

        

         A72: (wx /. i) = (wx . i) by A43, A68, PARTFUN1:def 6

        .= ((x | W) . (cs . i)) by A43, A68, FUNCT_1: 12

        .= (x . (cs . i)) by A70, FUNCT_1: 49;

        

         A73: (wy /. i) = (wy . i) by A43, A68, PARTFUN1:def 6

        .= ((y | W) . (cs . i)) by A43, A68, FUNCT_1: 12

        .= (y . (cs . i)) by A70, FUNCT_1: 49;

        

         A74: (wxy /. i) = (wxy . i) by A68, PARTFUN1:def 6

        .= ((xy | W) . (cs . i)) by A68, FUNCT_1: 12

        .= (xy . (cs . i)) by A70, FUNCT_1: 49;

        reconsider i0 = (cs . i) as Element of I by A71;

        

         A75: (F . i0) is Subgroup of G by A1;

        (x . i0) in (F . i0) by A3, A9, Th5, GROUP_2: 40;

        then

        reconsider fxi = (x . i0) as Element of (F . i0);

        (y . i0) in (F . i0) by A3, A10, Th5, GROUP_2: 40;

        then

        reconsider fyi = (y . i0) as Element of (F . i0);

        

        thus (wxy . i) = (xy . i0) by A68, A74, PARTFUN1:def 6

        .= ((px * py) . i0) by A3, GROUP_2: 43

        .= (fxi * fyi) by GROUP_7: 1

        .= ((wx /. i) * (wy /. i)) by A72, A73, A75, GROUP_2: 43;

      end;

      ( Product wxy) = (( Product wx) * ( Product wy)) by A45, A55, A67, Th47;

      hence thesis by A28, A34, A40, A50, A51, GROUP_17:def 1;

    end;

    theorem :: GROUP_19:54

    for I be non empty set, G be Group, F be Group-Family of I holds F is internal DirectSumComponents of G, I iff (for i be Element of I holds (F . i) is Subgroup of G) & (for i,j be Element of I, gi,gj be Element of G st i <> j & gi in (F . i) & gj in (F . j) holds (gi * gj) = (gj * gi)) & (for y be Element of G holds ex x be finite-support Function of I, G st x in ( sum F) & y = ( Product x)) & (for x1,x2 be finite-support Function of I, G st x1 in ( sum F) & x2 in ( sum F) & ( Product x1) = ( Product x2) holds x1 = x2)

    proof

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

      hereby

        assume

         A0: F is internal DirectSumComponents of G, I;

        then

         A1: (for i be Element of I holds (F . i) is Subgroup of G) & ex h be Homomorphism of ( sum F), G st h is bijective & for a be finite-support Function of I, G st a in ( sum F) holds (h . a) = ( Product a) by Def9;

        

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

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

         A3: h is bijective & for a be finite-support Function of I, G st a in ( sum F) holds (h . a) = ( Product a) by A0, Def9;

        

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

        proof

          let y be Element of G;

          ( rng h) = the carrier of G by A3, FUNCT_2:def 3;

          then

          consider x be Element of ( sum F) such that

           A5: y = (h . x) by FUNCT_2: 113;

          x in ( sum F);

          then

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

          take x;

          thus x in ( sum F);

          hence y = ( Product x) by A3, A5;

        end;

        

         A6: for x1,x2 be finite-support Function of I, G st x1 in ( sum F) & x2 in ( sum F) & ( Product x1) = ( Product x2) holds x1 = x2

        proof

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

          assume

           A7: x1 in ( sum F) & x2 in ( sum F) & ( Product x1) = ( Product x2);

          reconsider sx1 = x1, sx2 = x2 as Element of ( sum F) by A7;

          (h . sx1) = ( Product x1) by A3, A7

          .= (h . sx2) by A3, A7;

          hence x1 = x2 by A3, FUNCT_2: 19;

        end;

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

        proof

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

          assume that

           A10: i <> j and

           A11: gi in (F . i) and

           A12: gj in (F . j);

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

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

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

          then

           A13: ( 1_ ( product F)) in ( sum F);

          then

           A14: xi in ( sum F) by A11, Th25;

          

           A15: xj in ( sum F) by A12, A13, Th25;

          reconsider xi as finite-support Function of I, G by A2, A11, A13, Th10, Th25;

          reconsider xj as finite-support Function of I, G by A2, A12, A13, Th10, Th25;

          reconsider sxi = xi as Element of ( sum F) by A14;

          reconsider sxj = xj as Element of ( sum F) by A15;

          reconsider pxi = sxi as Element of ( product F) by GROUP_2: 42;

          reconsider pxj = sxj as Element of ( product F) by GROUP_2: 42;

          xi = ((I --> ( 1_ G)) +* (i,gi)) by A1, Th13;

          then

           A17: ( Product xi) = gi by Th21;

          xj = ((I --> ( 1_ G)) +* (j,gj)) by A1, Th13;

          then

           A18: ( Product xj) = gj by Th21;

          

           A19: ( support (pxi,F)) misses ( support (pxj,F))

          proof

            

             A20: ( support (pxi,F)) c= {i} by A11, Th17;

            ( support (pxj,F)) c= {j} by A12, Th17;

            hence thesis by A10, A20, ZFMISC_1: 11, XBOOLE_1: 64;

          end;

          (gi * gj) = ((h . sxi) * gj) by A3, A11, A13, A17, Th25

          .= ((h . sxi) * (h . sxj)) by A3, A12, A13, A18, Th25

          .= (h . (sxi * sxj)) by GROUP_6:def 6

          .= (h . (pxi * pxj)) by GROUP_2: 43

          .= (h . (pxj * pxi)) by A19, Th32

          .= (h . (sxj * sxi)) by GROUP_2: 43

          .= ((h . sxj) * (h . sxi)) by GROUP_6:def 6

          .= (gj * (h . sxi)) by A3, A12, A13, A18, Th25

          .= (gj * gi) by A3, A11, A13, A17, Th25;

          hence thesis;

        end;

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

      end;

      assume

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

      

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

      defpred P[ object, object] means ex x be finite-support Function of I, G st $1 = x & $2 = ( Product x);

      

       A34: for x be Element of ( sum F) holds ex y be Element of G st P[x, y]

      proof

        let x be Element of ( sum F);

        x in ( sum F);

        then

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

        ( Product x) is Element of G;

        hence thesis;

      end;

      consider h be Function of ( sum F), G such that

       A35: for x be Element of ( sum F) holds P[x, (h . x)] from FUNCT_2:sch 3( A34);

      for y be object st y in ( [#] G) holds ex x be object st x in ( [#] ( sum F)) & y = (h . x)

      proof

        let y be object;

        assume y in ( [#] G);

        then

        reconsider y as Element of G;

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

         A36: x in ( sum F) & y = ( Product x) by A32;

        ex x0 be finite-support Function of I, G st x = x0 & (h . x) = ( Product x0) by A35, A36;

        hence thesis by A36;

      end;

      then ( rng h) = ( [#] G) by FUNCT_2: 10;

      then

       A38: h is onto by FUNCT_2:def 3;

      for x1,x2 be object st x1 in ( [#] ( sum F)) & x2 in ( [#] ( sum F)) & (h . x1) = (h . x2) holds x1 = x2

      proof

        let x1,x2 be object;

        assume

         A39: x1 in ( [#] ( sum F)) & x2 in ( [#] ( sum F)) & (h . x1) = (h . x2);

        then

        reconsider sx1 = x1, sx2 = x2 as Element of ( sum F);

        x1 in ( sum F) by A39;

        then

        reconsider x1 as finite-support Function of I, G by A33, Th10;

        x2 in ( sum F) by A39;

        then

        reconsider x2 as finite-support Function of I, G by A33, Th10;

        

         A40: ex x be finite-support Function of I, G st x1 = x & (h . x1) = ( Product x) by A35, A39;

        

         A42: ex x be finite-support Function of I, G st x2 = x & (h . x2) = ( Product x) by A35, A39;

        x1 in ( sum F) & x2 in ( sum F) by A39;

        hence thesis by A32, A39, A40, A42;

      end;

      then

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

      

       A44: for a be finite-support Function of I, G st a in ( sum F) holds (h . a) = ( Product a)

      proof

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

        assume a in ( sum F);

        then

        reconsider sa = a as Element of ( sum F);

        ex x be finite-support Function of I, G st sa = x & (h . sa) = ( Product x) by A35;

        hence (h . a) = ( Product a);

      end;

      for x,y be Element of ( sum F) holds (h . (x * y)) = ((h . x) * (h . y))

      proof

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

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

         A45: x = x0 & (h . x) = ( Product x0) by A35;

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

         A46: y = y0 & (h . y) = ( Product y0) by A35;

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

         A47: (x * y) = xy0 & (h . (x * y)) = ( Product xy0) by A35;

        thus (h . (x * y)) = ((h . x) * (h . y)) by A32, A45, A46, A47, Th53;

      end;

      then

      reconsider h as Homomorphism of ( sum F), G by GROUP_6:def 6;

      h is bijective by A38, A43;

      hence F is internal DirectSumComponents of G, I by A32, A44, Def8, Def9;

    end;