group_7.miz



    begin

    reserve i,I for set,

f,g,h for Function,

s for ManySortedSet of I;

    definition

      let R be Relation;

      :: GROUP_7:def1

      attr R is multMagma-yielding means

      : Def1: for y be set st y in ( rng R) holds y is non empty multMagma;

    end

    registration

      cluster multMagma-yielding -> 1-sorted-yielding for Function;

      coherence

      proof

        let f be Function such that

         A1: f is multMagma-yielding;

        let x be object;

        assume x in ( dom f);

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

        hence thesis by A1;

      end;

    end

    registration

      let I be set;

      cluster multMagma-yielding for ManySortedSet of I;

      existence

      proof

        set H = the non empty multMagma;

        set f = (I --> H);

        take f;

        let a be set;

        assume a in ( rng f);

        then ex x be object st x in ( dom f) & a = (f . x) by FUNCT_1:def 3;

        hence thesis by FUNCOP_1: 7;

      end;

    end

    registration

      cluster multMagma-yielding for Function;

      existence

      proof

        set I = the set, f = the multMagma-yielding ManySortedSet of I;

        take f;

        thus thesis;

      end;

    end

    definition

      let I be set;

      mode multMagma-Family of I is multMagma-yielding ManySortedSet of I;

    end

    definition

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

      :: original: .

      redefine

      func F . i -> non empty multMagma ;

      coherence

      proof

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

        then (F . i) in ( rng F) by FUNCT_1:def 3;

        hence thesis by Def1;

      end;

    end

    registration

      let I be set, F be multMagma-Family of I;

      cluster ( Carrier F) -> non-empty;

      coherence

      proof

        let i be object;

        assume

         A1: i in I;

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

        then (F . i) in ( rng F) by A1, FUNCT_1:def 3;

        then

         A2: (F . i) is non empty multMagma by Def1;

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

        hence thesis by A2;

      end;

    end

     Lm1:

    now

      let I be non empty set, i be Element of I, F be multMagma-yielding ManySortedSet of I, f be Element of ( product ( Carrier F));

      

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

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

      hence (f . i) in the carrier of (F . i) by A1, CARD_3: 9;

    end;

    definition

      let I be set, F be multMagma-Family of I;

      :: GROUP_7:def2

      func product F -> strict multMagma means

      : Def2: the carrier of it = ( product ( Carrier F)) & for f,g be Element of ( product ( Carrier F)), i be set st i in I holds ex Fi be non empty multMagma, h be Function st Fi = (F . i) & h = (the multF of it . (f,g)) & (h . i) = (the multF of Fi . ((f . i),(g . i)));

      existence

      proof

        set A = ( product ( Carrier F));

        defpred P[ Element of A, Element of A, set] means for i be set st i in I holds ex Fi be non empty multMagma, h be Function st Fi = (F . i) & h = $3 & (h . i) = (the multF of Fi . (($1 . i),($2 . i)));

        

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

        

         A2: for x,y be Element of A holds ex z be Element of A st P[x, y, z]

        proof

          let x,y be Element of A;

          defpred R[ object, object] means ex Fi be non empty multMagma st Fi = (F . $1) & $2 = (the multF of Fi . ((x . $1),(y . $1)));

          

           A3: for i be object st i in I holds ex w be object st w in ( union ( rng ( Carrier F))) & R[i, w]

          proof

            let i be object;

            assume

             A4: i in I;

            then

            reconsider I1 = I as non empty set;

            reconsider i1 = i as Element of I1 by A4;

            reconsider F1 = F as multMagma-Family of I1;

            take w = (the multF of (F1 . i1) . ((x . i1),(y . i1)));

            

             A5: (( Carrier F) . i1) in ( rng ( Carrier F)) by A1, FUNCT_1:def 3;

            

             A6: ex R be 1-sorted st R = (F . i1) & (( Carrier F1) . i1) = the carrier of R by PRALG_1:def 15;

            then

             A7: (y . i1) in the carrier of (F1 . i1) by A1, CARD_3: 9;

            (x . i1) in the carrier of (F1 . i1) by A1, A6, CARD_3: 9;

            then (the multF of (F1 . i1) . ((x . i1),(y . i1))) in the carrier of (F1 . i1) by A7, BINOP_1: 17;

            hence w in ( union ( rng ( Carrier F))) by A6, A5, TARSKI:def 4;

            thus thesis;

          end;

          consider z be Function such that

           A8: ( dom z) = I & ( rng z) c= ( union ( rng ( Carrier F))) & for x be object st x in I holds R[x, (z . x)] from FUNCT_1:sch 6( A3);

          

           A9: for i be object st i in ( dom ( Carrier F)) holds (z . i) in (( Carrier F) . i)

          proof

            let i be object;

            assume

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

            then

            reconsider I1 = I as non empty set;

            

             A11: ex Fi be non empty multMagma st Fi = (F . i) & (z . i) = (the multF of Fi . ((x . i),(y . i))) by A8, A10;

            reconsider i1 = i as Element of I1 by A10;

            reconsider F1 = F as multMagma-Family of I1;

            

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

            then

             A13: (y . i1) in the carrier of (F1 . i1) by A1, CARD_3: 9;

            (x . i1) in the carrier of (F1 . i1) by A1, A12, CARD_3: 9;

            hence thesis by A11, A12, A13, BINOP_1: 17;

          end;

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

          then

          reconsider z as Element of A by A9, CARD_3: 9;

          take z;

          let i be set;

          assume i in I;

          then

          consider Fi be non empty multMagma such that

           A14: Fi = (F . i) and

           A15: (z . i) = (the multF of Fi . ((x . i),(y . i))) by A8;

          take Fi, z;

          thus Fi = (F . i) & z = z & (z . i) = (the multF of Fi . ((x . i),(y . i))) by A14, A15;

        end;

        consider B be BinOp of A such that

         A16: for a,b be Element of A holds P[a, b, (B . (a,b))] from BINOP_1:sch 3( A2);

        take multMagma (# A, B #);

        thus the carrier of multMagma (# A, B #) = ( product ( Carrier F));

        let f,g be Element of ( product ( Carrier F)), i be set;

        assume i in I;

        hence thesis by A16;

      end;

      uniqueness

      proof

        let A,B be strict multMagma such that

         A17: the carrier of A = ( product ( Carrier F)) and

         A18: for f,g be Element of ( product ( Carrier F)), i be set st i in I holds ex Fi be non empty multMagma, h be Function st Fi = (F . i) & h = (the multF of A . (f,g)) & (h . i) = (the multF of Fi . ((f . i),(g . i))) and

         A19: the carrier of B = ( product ( Carrier F)) and

         A20: for f,g be Element of ( product ( Carrier F)), i be set st i in I holds ex Fi be non empty multMagma, h be Function st Fi = (F . i) & h = (the multF of B . (f,g)) & (h . i) = (the multF of Fi . ((f . i),(g . i)));

        for x,y be set st x in the carrier of A & y in the carrier of A holds (the multF of A . (x,y)) = (the multF of B . (x,y))

        proof

          set P = ( product ( Carrier F));

          let x,y be set such that

           A21: x in the carrier of A and

           A22: y in the carrier of A;

          reconsider x1 = x, y1 = y as Element of P by A17, A21, A22;

           [x1, y1] in [:the carrier of A, the carrier of A:] by A21, A22, ZFMISC_1: 87;

          then

          reconsider f = (the multF of A . [x1, y1]) as Element of P by A17, FUNCT_2: 5;

           [x1, y1] in [:the carrier of B, the carrier of B:] by A19, ZFMISC_1: 87;

          then

          reconsider g = (the multF of B . [x1, y1]) as Element of P by A19, FUNCT_2: 5;

          

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

          then

           A24: ( dom g) = I by CARD_3: 9;

          

           A25: for i be object st i in I holds (f . i) = (g . i)

          proof

            let i be object;

            assume

             A26: i in I;

            then

             A27: ex Gi be non empty multMagma, h2 be Function st Gi = (F . i) & h2 = (the multF of B . (x1,y1)) & (h2 . i) = (the multF of Gi . ((x1 . i),(y1 . i))) by A20;

            ex Fi be non empty multMagma, h1 be Function st Fi = (F . i) & h1 = (the multF of A . (x1,y1)) & (h1 . i) = (the multF of Fi . ((x1 . i),(y1 . i))) by A18, A26;

            hence thesis by A27;

          end;

          ( dom f) = I by A23, CARD_3: 9;

          hence thesis by A24, A25, FUNCT_1: 2;

        end;

        hence thesis by A17, A19, BINOP_1: 1;

      end;

    end

    registration

      let I be set, F be multMagma-Family of I;

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

      coherence

      proof

        

         A1: the carrier of ( product F) = ( product ( Carrier F)) by Def2;

        hence the carrier of ( product F) is non empty;

        thus thesis by A1, MONOID_0: 80;

      end;

    end

    theorem :: GROUP_7:1

    

     Th1: for F be multMagma-Family of I, G be non empty multMagma, p,q be Element of ( product F), x,y be Element of G st i in I & G = (F . i) & f = p & g = q & h = (p * q) & (f . i) = x & (g . i) = y holds (x * y) = (h . i)

    proof

      let F be multMagma-Family of I, G be non empty multMagma, p,q be Element of ( product F), x,y be Element of G such that

       A1: i in I and

       A2: G = (F . i) and

       A3: f = p and

       A4: g = q and

       A5: h = (p * q) and

       A6: (f . i) = x and

       A7: (g . i) = y;

      set GP = ( product F);

      q in the carrier of GP;

      then

       A8: g in ( product ( Carrier F)) by A4, Def2;

      p in the carrier of GP;

      then f in ( product ( Carrier F)) by A3, Def2;

      then ex Fi be non empty multMagma, m be Function st Fi = (F . i) & m = (the multF of GP . (f,g)) & (m . i) = (the multF of Fi . ((f . i),(g . i))) by A1, A8, Def2;

      hence thesis by A2, A3, A4, A5, A6, A7;

    end;

    definition

      let I be set, F be multMagma-Family of I;

      :: GROUP_7:def3

      attr F is Group-like means

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

      :: GROUP_7:def4

      attr F is associative means

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

      :: GROUP_7:def5

      attr F is commutative means

      : Def5: for i be set st i in I holds ex Fi be commutative non empty multMagma st Fi = (F . i);

    end

    definition

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

      :: original: Group-like

      redefine

      :: GROUP_7:def6

      attr F is Group-like means

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

      compatibility

      proof

        hereby

          assume

           A1: F is Group-like;

          let i be Element of I;

          ex Fi be Group-like non empty multMagma st Fi = (F . i) by A1;

          hence (F . i) is Group-like;

        end;

        assume

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

        let i be set;

        assume i in I;

        then

        reconsider i1 = i as Element of I;

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

        take F1;

        thus thesis;

      end;

      :: original: associative

      redefine

      :: GROUP_7:def7

      attr F is associative means

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

      compatibility

      proof

        hereby

          assume

           A3: F is associative;

          let i be Element of I;

          ex Fi be associative non empty multMagma st Fi = (F . i) by A3;

          hence (F . i) is associative;

        end;

        assume

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

        let i be set;

        assume i in I;

        then

        reconsider i1 = i as Element of I;

        reconsider Fi = (F . i1) as associative non empty multMagma by A4;

        take Fi;

        thus thesis;

      end;

      :: original: commutative

      redefine

      :: GROUP_7:def8

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

      compatibility

      proof

        hereby

          assume

           A5: F is commutative;

          let i be Element of I;

          ex Fi be commutative non empty multMagma st Fi = (F . i) by A5;

          hence (F . i) is commutative;

        end;

        assume

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

        let i be set;

        assume i in I;

        then

        reconsider i1 = i as Element of I;

        reconsider Fi = (F . i1) as commutative non empty multMagma by A6;

        take Fi;

        thus thesis;

      end;

    end

    registration

      let I be set;

      cluster Group-like associative commutative for multMagma-Family of I;

      existence

      proof

        set H = the commutative Group;

        set f = (I --> H);

        f is multMagma-yielding

        proof

          let i be set;

          assume i in ( rng f);

          then ex x be object st x in ( dom f) & i = (f . x) by FUNCT_1:def 3;

          hence thesis by FUNCOP_1: 7;

        end;

        then

        reconsider f as multMagma-Family of I;

        take f;

        hereby

          let i be set;

          assume

           A1: i in I;

          then

          reconsider I1 = I as non empty set;

          reconsider i1 = i as Element of I1 by A1;

          reconsider F1 = f as multMagma-Family of I1;

          reconsider Fi = (F1 . i1) as Group-like non empty multMagma;

          take Fi;

          thus Fi = (f . i);

        end;

        hereby

          let i be set;

          assume

           A2: i in I;

          then

          reconsider I1 = I as non empty set;

          reconsider i1 = i as Element of I1 by A2;

          reconsider F1 = f as multMagma-Family of I1;

          reconsider Fi = (F1 . i1) as associative non empty multMagma;

          take Fi;

          thus Fi = (f . i);

        end;

        let i be set;

        assume

         A3: i in I;

        then

        reconsider I1 = I as non empty set;

        reconsider i1 = i as Element of I1 by A3;

        reconsider F1 = f as multMagma-Family of I1;

        reconsider Fi = (F1 . i1) as commutative non empty multMagma;

        take Fi;

        thus thesis;

      end;

    end

    registration

      let I be set, F be Group-like multMagma-Family of I;

      cluster ( product F) -> Group-like;

      coherence

      proof

        defpred P[ object, object] means ex Fi be non empty multMagma, e be Element of Fi st Fi = (F . $1) & $2 = e & for h be Element of Fi holds (h * e) = h & (e * h) = h & ex g be Element of Fi st (h * g) = e & (g * h) = e;

        set G = ( product F);

        

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

        

         A2: for i be object st i in I holds ex y be object st y in ( union ( rng ( Carrier F))) & P[i, y]

        proof

          let i be object;

          assume

           A3: i in I;

          then

          reconsider I1 = I as non empty set;

          reconsider i1 = i as Element of I1 by A3;

          reconsider F1 = F as Group-like multMagma-Family of I1;

          

           A4: ex R be 1-sorted st R = (F . i1) & (( Carrier F1) . i1) = the carrier of R by PRALG_1:def 15;

          (F1 . i1) is Group-like by Def6;

          then

          consider e be Element of (F1 . i1) such that

           A5: for h be Element of (F1 . i1) holds (h * e) = h & (e * h) = h & ex g be Element of (F1 . i1) st (h * g) = e & (g * h) = e;

          take e;

          (( Carrier F) . i1) in ( rng ( Carrier F)) by A1, FUNCT_1:def 3;

          hence e in ( union ( rng ( Carrier F))) by A4, TARSKI:def 4;

          take (F1 . i1), e;

          thus (F1 . i1) = (F . i) & e = e;

          let h be Element of (F1 . i1);

          thus thesis by A5;

        end;

        consider ee be Function such that

         A6: ( dom ee) = I and ( rng ee) c= ( union ( rng ( Carrier F))) and

         A7: for x be object st x in I holds P[x, (ee . x)] from FUNCT_1:sch 6( A2);

        now

          let i be object;

          assume

           A8: i in ( dom ee);

          then

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

          ex Fi be non empty multMagma, e be Element of Fi st Fi = (F . i) & (ee . i) = e & for h be Element of Fi holds (h * e) = h & (e * h) = h & ex g be Element of Fi st (h * g) = e & (g * h) = e by A6, A7, A8;

          hence (ee . i) in (( Carrier F) . i) by A9;

        end;

        then

         A10: ee in ( product ( Carrier F)) by A1, A6, CARD_3: 9;

        then

        reconsider e1 = ee as Element of G by Def2;

        take e1;

        let h be Element of G;

        reconsider h1 = h as Element of ( product ( Carrier F)) by Def2;

        reconsider he = (the multF of G . (h,e1)), eh = (the multF of G . (e1,h)) as Element of ( product ( Carrier F)) by Def2;

        

         A11: ( dom h1) = I by A1, CARD_3: 9;

         A12:

        now

          let i be object;

          assume

           A13: i in I;

          then

          consider Fi be non empty multMagma, e2 be Element of Fi such that

           A14: Fi = (F . i) and

           A15: (ee . i) = e2 and

           A16: for h be Element of Fi holds (h * e2) = h & (e2 * h) = h & ex g be Element of Fi st (h * g) = e2 & (g * h) = e2 by A7;

          reconsider h2 = (h1 . i) as Element of Fi by A13, A14, Lm1;

          

           A17: ex Gi be non empty multMagma, f be Function st Gi = (F . i) & f = (the multF of G . (h1,e1)) & (f . i) = (the multF of Gi . ((h1 . i),(ee . i))) by A10, A13, Def2;

          (h2 * e2) = h2 by A16;

          hence (he . i) = (h1 . i) by A17, A14, A15;

        end;

        ( dom he) = I by A1, CARD_3: 9;

        hence (h * e1) = h by A11, A12;

         A18:

        now

          let i be object;

          assume

           A19: i in I;

          then

          consider Fi be non empty multMagma, e2 be Element of Fi such that

           A20: Fi = (F . i) and

           A21: (ee . i) = e2 and

           A22: for h be Element of Fi holds (h * e2) = h & (e2 * h) = h & ex g be Element of Fi st (h * g) = e2 & (g * h) = e2 by A7;

          reconsider h2 = (h1 . i) as Element of Fi by A19, A20, Lm1;

          

           A23: ex Gi be non empty multMagma, f be Function st Gi = (F . i) & f = (the multF of G . (e1,h1)) & (f . i) = (the multF of Gi . ((ee . i),(h1 . i))) by A10, A19, Def2;

          (e2 * h2) = h2 by A22;

          hence (eh . i) = (h1 . i) by A23, A20, A21;

        end;

        defpred R[ object, object] means ex Fi be non empty multMagma, hi be Element of Fi st Fi = (F . $1) & hi = (h1 . $1) & ex g be Element of Fi st (hi * g) = (ee . $1) & (g * hi) = (ee . $1) & $2 = g;

        

         A24: for i be object st i in I holds ex y be object st y in ( union ( rng ( Carrier F))) & R[i, y]

        proof

          let i be object;

          assume

           A25: i in I;

          then

          consider Fi be non empty multMagma, e be Element of Fi such that

           A26: Fi = (F . i) and

           A27: (ee . i) = e and

           A28: for h be Element of Fi holds (h * e) = h & (e * h) = h & ex g be Element of Fi st (h * g) = e & (g * h) = e by A7;

          

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

          reconsider hi = (h1 . i) as Element of Fi by A25, A26, Lm1;

          consider g be Element of Fi such that

           A30: (hi * g) = e and

           A31: (g * hi) = e by A28;

          take g;

          (( Carrier F) . i) in ( rng ( Carrier F)) by A1, A25, FUNCT_1:def 3;

          hence g in ( union ( rng ( Carrier F))) by A26, A29, TARSKI:def 4;

          take Fi, hi;

          thus Fi = (F . i) & hi = (h1 . i) by A26;

          take g;

          thus thesis by A27, A30, A31;

        end;

        consider gg be Function such that

         A32: ( dom gg) = I and ( rng gg) c= ( union ( rng ( Carrier F))) and

         A33: for x be object st x in I holds R[x, (gg . x)] from FUNCT_1:sch 6( A24);

        now

          let i be object;

          assume

           A34: i in ( dom gg);

          then

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

          ex Fi be non empty multMagma, hi be Element of Fi st Fi = (F . i) & hi = (h1 . i) & ex g be Element of Fi st (hi * g) = (ee . i) & (g * hi) = (ee . i) & (gg . i) = g by A32, A33, A34;

          hence (gg . i) in (( Carrier F) . i) by A35;

        end;

        then

         A36: gg in ( product ( Carrier F)) by A1, A32, CARD_3: 9;

        then

        reconsider g1 = gg as Element of G by Def2;

        ( dom eh) = I by A1, CARD_3: 9;

        hence (e1 * h) = h by A11, A18;

        take g1;

        reconsider he = (the multF of G . (h,g1)), eh = (the multF of G . (g1,h)) as Element of ( product ( Carrier F)) by Def2;

         A37:

        now

          let i be object;

          assume

           A38: i in I;

          then

           A39: ex Fi be non empty multMagma, hi be Element of Fi st Fi = (F . i) & hi = (h1 . i) & ex g be Element of Fi st (hi * g) = (ee . i) & (g * hi) = (ee . i) & (gg . i) = g by A33;

          ex Gi be non empty multMagma, h5 be Function st Gi = (F . i) & h5 = (the multF of G . (h1,gg)) & (h5 . i) = (the multF of Gi . ((h1 . i),(gg . i))) by A36, A38, Def2;

          hence (he . i) = (ee . i) by A39;

        end;

         A40:

        now

          let i be object;

          assume

           A41: i in I;

          then

           A42: ex Fi be non empty multMagma, hi be Element of Fi st Fi = (F . i) & hi = (h1 . i) & ex g be Element of Fi st (hi * g) = (ee . i) & (g * hi) = (ee . i) & (gg . i) = g by A33;

          ex Gi be non empty multMagma, h5 be Function st Gi = (F . i) & h5 = (the multF of G . (gg,h1)) & (h5 . i) = (the multF of Gi . ((gg . i),(h1 . i))) by A36, A41, Def2;

          hence (eh . i) = (ee . i) by A42;

        end;

        ( dom he) = I by A1, CARD_3: 9;

        hence (h * g1) = e1 by A6, A37;

        ( dom eh) = I by A1, CARD_3: 9;

        hence thesis by A6, A40;

      end;

    end

    registration

      let I be set, F be associative multMagma-Family of I;

      cluster ( product F) -> associative;

      coherence

      proof

        set G = ( product F);

        let x,y,z be Element of G;

        reconsider x1 = x, y1 = y, z1 = z as Element of ( product ( Carrier F)) by Def2;

        set xy = (the multF of G . (x,y)), yz = (the multF of G . (y,z)), s = (the multF of G . (xy,z)), t = (the multF of G . (x,yz));

        reconsider xy, yz, s, t as Element of ( product ( Carrier F)) by Def2;

        

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

        then

         A2: ( dom t) = I by CARD_3: 9;

         A3:

        now

          let i be object;

          assume

           A4: i in I;

          then

          consider XY be non empty multMagma, hxy be Function such that

           A5: XY = (F . i) and

           A6: hxy = (the multF of G . (x,y)) and

           A7: (hxy . i) = (the multF of XY . ((x1 . i),(y1 . i))) by Def2;

          

           A8: ex YZ be non empty multMagma, hyz be Function st YZ = (F . i) & hyz = (the multF of G . (y,z)) & (hyz . i) = (the multF of YZ . ((y1 . i),(z1 . i))) by A4, Def2;

          reconsider xi = (x1 . i), yi = (y1 . i) as Element of XY by A4, A5, Lm1;

          consider XYZ1 be non empty multMagma, hxyz1 be Function such that

           A9: XYZ1 = (F . i) and

           A10: hxyz1 = (the multF of G . (xy,z)) and

           A11: (hxyz1 . i) = (the multF of XYZ1 . ((xy . i),(z1 . i))) by A4, Def2;

          reconsider zi = (z1 . i), xiyi = (xi * yi) as Element of XYZ1 by A4, A5, A9, Lm1;

          reconsider xii = xi, yii = yi as Element of XYZ1 by A5, A9;

          

           A12: XYZ1 is associative by A4, A9, Def7;

          

           A13: ex XYZ2 be non empty multMagma, hxyz2 be Function st XYZ2 = (F . i) & hxyz2 = (the multF of G . (x,yz)) & (hxyz2 . i) = (the multF of XYZ2 . ((x1 . i),(yz . i))) by A4, Def2;

          

          thus (s . i) = (xiyi * zi) by A6, A7, A10, A11

          .= (xii * (yii * zi)) by A5, A9, A12

          .= (t . i) by A8, A9, A13;

        end;

        ( dom s) = I by A1, CARD_3: 9;

        hence thesis by A2, A3;

      end;

    end

    registration

      let I be set, F be commutative multMagma-Family of I;

      cluster ( product F) -> commutative;

      coherence

      proof

        set G = ( product F);

        let x,y be Element of G;

        reconsider x1 = x, y1 = y, xy = (the multF of G . (x,y)), yx = (the multF of G . (y,x)) as Element of ( product ( Carrier F)) by Def2;

        

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

        then

         A2: ( dom yx) = I by CARD_3: 9;

         A3:

        now

          let i be object;

          assume

           A4: i in I;

          then

          consider XY be non empty multMagma, hxy be Function such that

           A5: XY = (F . i) and

           A6: hxy = (the multF of G . (x,y)) and

           A7: (hxy . i) = (the multF of XY . ((x1 . i),(y1 . i))) by Def2;

          reconsider xi = (x1 . i), yi = (y1 . i) as Element of XY by A4, A5, Lm1;

          

           A8: ex YX be non empty multMagma, hyx be Function st YX = (F . i) & hyx = (the multF of G . (y,x)) & (hyx . i) = (the multF of YX . ((y1 . i),(x1 . i))) by A4, Def2;

          

           A9: ex Fi be commutative non empty multMagma st (Fi = (F . i)) by A4, Def5;

          

          thus (xy . i) = (xi * yi) by A6, A7

          .= (yi * xi) by A5, A9, GROUP_1:def 12

          .= (yx . i) by A5, A8;

        end;

        ( dom xy) = I by A1, CARD_3: 9;

        hence thesis by A2, A3;

      end;

    end

    theorem :: GROUP_7:2

    for F be multMagma-Family of I, G be non empty multMagma st i in I & G = (F . i) & ( product F) is Group-like holds G is Group-like

    proof

      let F be multMagma-Family of I, G be non empty multMagma such that

       A1: i in I and

       A2: G = (F . i);

      set GP = ( product F);

      given e be Element of GP such that

       A3: for h be Element of GP holds (h * e) = h & (e * h) = h & ex g be Element of GP st (h * g) = e & (g * h) = e;

      reconsider f = e as Element of ( product ( Carrier F)) by Def2;

      reconsider ei = (f . i) as Element of G by A1, A2, Lm1;

      take ei;

      let h be Element of G;

      defpred P[ object, object] means ($1 = i implies $2 = h) & ($1 <> i implies ex H be non empty multMagma, a be Element of H st H = (F . $1) & $2 = a);

      

       A4: for j be object st j in I holds ex k be object st P[j, k]

      proof

        let j be object such that

         A5: j in I;

        per cases ;

          suppose j = i;

          hence thesis;

        end;

          suppose

           A6: j <> i;

          j in ( dom F) by A5, PARTFUN1:def 2;

          then (F . j) in ( rng F) by FUNCT_1:def 3;

          then

          reconsider Fj = (F . j) as non empty multMagma by Def1;

          set a = the Element of Fj;

          take a;

          thus j = i implies a = h by A6;

          thus thesis;

        end;

      end;

      consider g be ManySortedSet of I such that

       A7: for j be object st j in I holds P[j, (g . j)] from PBOOLE:sch 3( A4);

      

       A8: ( dom g) = I by PARTFUN1:def 2;

       A9:

      now

        let j be object;

        assume

         A10: j in ( dom g);

        then

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

        per cases ;

          suppose

           A12: i = j;

          then (g . j) = h by A7, A10;

          hence (g . j) in (( Carrier F) . j) by A2, A11, A12;

        end;

          suppose j <> i;

          then ex H be non empty multMagma, a be Element of H st H = (F . j) & (g . j) = a by A7, A10;

          hence (g . j) in (( Carrier F) . j) by A11;

        end;

      end;

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

      then

      reconsider g as Element of ( product ( Carrier F)) by A8, A9, CARD_3: 9;

      

       A13: (g . i) = h by A1, A7;

      reconsider g1 = g as Element of GP by Def2;

      

       A14: (e * g1) = g1 by A3;

      (g1 * e) = g1 by A3;

      hence (h * ei) = h & (ei * h) = h by A1, A2, A13, A14, Th1;

      consider gg be Element of GP such that

       A15: (g1 * gg) = e and

       A16: (gg * g1) = e by A3;

      reconsider r = gg as Element of ( product ( Carrier F)) by Def2;

      reconsider r1 = (r . i) as Element of G by A1, A2, Lm1;

      take r1;

      thus thesis by A1, A2, A13, A15, A16, Th1;

    end;

    theorem :: GROUP_7:3

    for F be multMagma-Family of I, G be non empty multMagma st i in I & G = (F . i) & ( product F) is associative holds G is associative

    proof

      let F be multMagma-Family of I, G be non empty multMagma such that

       A1: i in I and

       A2: G = (F . i) and

       A3: for x,y,z be Element of ( product F) holds ((x * y) * z) = (x * (y * z));

      let x,y,z be Element of G;

      defpred Y[ object, object] means ($1 = i implies $2 = y) & ($1 <> i implies ex H be non empty multMagma, a be Element of H st H = (F . $1) & $2 = a);

      

       A4: for j be object st j in I holds ex k be object st Y[j, k]

      proof

        let j be object such that

         A5: j in I;

        per cases ;

          suppose j = i;

          hence thesis;

        end;

          suppose

           A6: j <> i;

          j in ( dom F) by A5, PARTFUN1:def 2;

          then (F . j) in ( rng F) by FUNCT_1:def 3;

          then

          reconsider Fj = (F . j) as non empty multMagma by Def1;

          set a = the Element of Fj;

          take a;

          thus j = i implies a = y by A6;

          thus thesis;

        end;

      end;

      consider gy be ManySortedSet of I such that

       A7: for j be object st j in I holds Y[j, (gy . j)] from PBOOLE:sch 3( A4);

      

       A8: ( dom gy) = I by PARTFUN1:def 2;

       A9:

      now

        let j be object;

        assume

         A10: j in ( dom gy);

        then

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

        per cases ;

          suppose

           A12: i = j;

          then (gy . j) = y by A7, A10;

          hence (gy . j) in (( Carrier F) . j) by A2, A11, A12;

        end;

          suppose j <> i;

          then ex H be non empty multMagma, a be Element of H st H = (F . j) & (gy . j) = a by A7, A10;

          hence (gy . j) in (( Carrier F) . j) by A11;

        end;

      end;

      defpred Z[ object, object] means ($1 = i implies $2 = z) & ($1 <> i implies ex H be non empty multMagma, a be Element of H st H = (F . $1) & $2 = a);

      

       A13: for j be object st j in I holds ex k be object st Z[j, k]

      proof

        let j be object such that

         A14: j in I;

        per cases ;

          suppose j = i;

          hence thesis;

        end;

          suppose

           A15: j <> i;

          j in ( dom F) by A14, PARTFUN1:def 2;

          then (F . j) in ( rng F) by FUNCT_1:def 3;

          then

          reconsider Fj = (F . j) as non empty multMagma by Def1;

          set a = the Element of Fj;

          take a;

          thus j = i implies a = z by A15;

          thus thesis;

        end;

      end;

      consider gz be ManySortedSet of I such that

       A16: for j be object st j in I holds Z[j, (gz . j)] from PBOOLE:sch 3( A13);

      set GP = ( product F);

      defpred X[ object, object] means ($1 = i implies $2 = x) & ($1 <> i implies ex H be non empty multMagma, a be Element of H st H = (F . $1) & $2 = a);

      

       A17: for j be object st j in I holds ex k be object st X[j, k]

      proof

        let j be object such that

         A18: j in I;

        per cases ;

          suppose j = i;

          hence thesis;

        end;

          suppose

           A19: j <> i;

          j in ( dom F) by A18, PARTFUN1:def 2;

          then (F . j) in ( rng F) by FUNCT_1:def 3;

          then

          reconsider Fj = (F . j) as non empty multMagma by Def1;

          set a = the Element of Fj;

          take a;

          thus j = i implies a = x by A19;

          thus thesis;

        end;

      end;

      consider gx be ManySortedSet of I such that

       A20: for j be object st j in I holds X[j, (gx . j)] from PBOOLE:sch 3( A17);

      

       A21: ( dom gx) = I by PARTFUN1:def 2;

       A22:

      now

        let j be object;

        assume

         A23: j in ( dom gx);

        then

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

        per cases ;

          suppose

           A25: i = j;

          then (gx . j) = x by A20, A23;

          hence (gx . j) in (( Carrier F) . j) by A2, A24, A25;

        end;

          suppose j <> i;

          then ex H be non empty multMagma, a be Element of H st H = (F . j) & (gx . j) = a by A20, A23;

          hence (gx . j) in (( Carrier F) . j) by A24;

        end;

      end;

      

       A26: ( dom gz) = I by PARTFUN1:def 2;

       A27:

      now

        let j be object;

        assume

         A28: j in ( dom gz);

        then

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

        per cases ;

          suppose

           A30: i = j;

          then (gz . j) = z by A16, A28;

          hence (gz . j) in (( Carrier F) . j) by A2, A29, A30;

        end;

          suppose j <> i;

          then ex H be non empty multMagma, a be Element of H st H = (F . j) & (gz . j) = a by A16, A28;

          hence (gz . j) in (( Carrier F) . j) by A29;

        end;

      end;

      

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

      then

      reconsider gx as Element of ( product ( Carrier F)) by A21, A22, CARD_3: 9;

      reconsider gz as Element of ( product ( Carrier F)) by A26, A31, A27, CARD_3: 9;

      reconsider gy as Element of ( product ( Carrier F)) by A8, A31, A9, CARD_3: 9;

      reconsider x1 = gx, y1 = gy, z1 = gz as Element of GP by Def2;

      reconsider xy = (x1 * y1), xyz3 = ((x1 * y1) * z1), yz = (y1 * z1), xyz5 = (x1 * (y1 * z1)) as Element of ( product ( Carrier F)) by Def2;

      reconsider xyi = (xy . i), yzi = (yz . i) as Element of G by A1, A2, Lm1;

      

       A32: ((x1 * y1) * z1) = (x1 * (y1 * z1)) by A3;

      

       A33: (gx . i) = x by A1, A20;

      then

       A34: (x * yzi) = (xyz5 . i) by A1, A2, Th1;

      

       A35: (gz . i) = z by A1, A16;

      then

       A36: (xyi * z) = (xyz3 . i) by A1, A2, Th1;

      

       A37: (gy . i) = y by A1, A7;

      then (xy . i) = (x * y) by A1, A2, A33, Th1;

      hence thesis by A1, A2, A32, A37, A35, A36, A34, Th1;

    end;

    theorem :: GROUP_7:4

    for F be multMagma-Family of I, G be non empty multMagma st i in I & G = (F . i) & ( product F) is commutative holds G is commutative

    proof

      let F be multMagma-Family of I, G be non empty multMagma such that

       A1: i in I and

       A2: G = (F . i) and

       A3: for x,y be Element of ( product F) holds (x * y) = (y * x);

      let x,y be Element of G;

      defpred Y[ object, object] means ($1 = i implies $2 = y) & ($1 <> i implies ex H be non empty multMagma, a be Element of H st H = (F . $1) & $2 = a);

      

       A4: for j be object st j in I holds ex k be object st Y[j, k]

      proof

        let j be object such that

         A5: j in I;

        per cases ;

          suppose j = i;

          hence thesis;

        end;

          suppose

           A6: j <> i;

          j in ( dom F) by A5, PARTFUN1:def 2;

          then (F . j) in ( rng F) by FUNCT_1:def 3;

          then

          reconsider Fj = (F . j) as non empty multMagma by Def1;

          set a = the Element of Fj;

          take a;

          thus j = i implies a = y by A6;

          thus thesis;

        end;

      end;

      consider gy be ManySortedSet of I such that

       A7: for j be object st j in I holds Y[j, (gy . j)] from PBOOLE:sch 3( A4);

      set GP = ( product F);

      defpred X[ object, object] means ($1 = i implies $2 = x) & ($1 <> i implies ex H be non empty multMagma, a be Element of H st H = (F . $1) & $2 = a);

      

       A8: for j be object st j in I holds ex k be object st X[j, k]

      proof

        let j be object such that

         A9: j in I;

        per cases ;

          suppose j = i;

          hence thesis;

        end;

          suppose

           A10: j <> i;

          j in ( dom F) by A9, PARTFUN1:def 2;

          then (F . j) in ( rng F) by FUNCT_1:def 3;

          then

          reconsider Fj = (F . j) as non empty multMagma by Def1;

          set a = the Element of Fj;

          take a;

          thus j = i implies a = x by A10;

          thus thesis;

        end;

      end;

      consider gx be ManySortedSet of I such that

       A11: for j be object st j in I holds X[j, (gx . j)] from PBOOLE:sch 3( A8);

      

       A12: ( dom gy) = I by PARTFUN1:def 2;

       A13:

      now

        let j be object;

        assume

         A14: j in ( dom gy);

        then

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

        per cases ;

          suppose

           A16: i = j;

          then (gy . j) = y by A7, A14;

          hence (gy . j) in (( Carrier F) . j) by A2, A15, A16;

        end;

          suppose j <> i;

          then ex H be non empty multMagma, a be Element of H st H = (F . j) & (gy . j) = a by A7, A14;

          hence (gy . j) in (( Carrier F) . j) by A15;

        end;

      end;

      

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

      then

      reconsider gy as Element of ( product ( Carrier F)) by A12, A13, CARD_3: 9;

      

       A18: (gy . i) = y by A1, A7;

      

       A19: ( dom gx) = I by PARTFUN1:def 2;

      now

        let j be object;

        assume

         A20: j in ( dom gx);

        then

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

        per cases ;

          suppose

           A22: i = j;

          then (gx . j) = x by A11, A20;

          hence (gx . j) in (( Carrier F) . j) by A2, A21, A22;

        end;

          suppose j <> i;

          then ex H be non empty multMagma, a be Element of H st H = (F . j) & (gx . j) = a by A11, A20;

          hence (gx . j) in (( Carrier F) . j) by A21;

        end;

      end;

      then

      reconsider gx as Element of ( product ( Carrier F)) by A19, A17, CARD_3: 9;

      reconsider x1 = gx, y1 = gy as Element of GP by Def2;

      

       A23: (x1 * y1) = (y1 * x1) by A3;

      reconsider xy = (x1 * y1) as Element of ( product ( Carrier F)) by Def2;

      

       A24: (gx . i) = x by A1, A11;

      then (xy . i) = (x * y) by A1, A2, A18, Th1;

      hence thesis by A1, A2, A23, A24, A18, Th1;

    end;

    theorem :: GROUP_7:5

    

     Th5: for F be Group-like multMagma-Family of I st for i be set st i in I holds ex G be Group-like non empty multMagma st G = (F . i) & (s . i) = ( 1_ G) holds s = ( 1_ ( product F))

    proof

      let F be Group-like multMagma-Family of I such that

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

      set GP = ( product F);

      

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

      

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

      now

        let i be object;

        assume

         A4: i in ( dom s);

        then

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

        ex G be Group-like non empty multMagma st (G = (F . i)) & ((s . i) = ( 1_ G)) by A1, A4;

        hence (s . i) in (( Carrier F) . i) by A5;

      end;

      then

       A6: s in ( product ( Carrier F)) by A3, A2, CARD_3: 9;

      then

      reconsider e = s as Element of GP by Def2;

      now

        let h be Element of GP;

        reconsider h1 = h, he = (h * e), eh = (e * h) as Element of ( product ( Carrier F)) by Def2;

        

         A7: ( dom h1) = I by A2, CARD_3: 9;

         A8:

        now

          let i be object;

          assume

           A9: i in I;

          then

          consider G be Group-like non empty multMagma such that

           A10: G = (F . i) and

           A11: (s . i) = ( 1_ G) by A1;

          reconsider b = (h1 . i), c = (s . i) as Element of G by A9, A10, A11, Lm1;

          

           A12: ex Fi be non empty multMagma, m be Function st Fi = (F . i) & m = (the multF of GP . (h,s)) & (m . i) = (the multF of Fi . ((h1 . i),(s . i))) by A6, A9, Def2;

          (b * c) = b by A11, GROUP_1:def 4;

          hence (he . i) = (h1 . i) by A12, A10;

        end;

        ( dom he) = I by A2, CARD_3: 9;

        hence (h * e) = h by A7, A8;

         A13:

        now

          let i be object;

          assume

           A14: i in I;

          then

          consider G be Group-like non empty multMagma such that

           A15: G = (F . i) and

           A16: (s . i) = ( 1_ G) by A1;

          reconsider b = (h1 . i), c = (s . i) as Element of G by A14, A15, A16, Lm1;

          

           A17: ex Fi be non empty multMagma, m be Function st Fi = (F . i) & m = (the multF of GP . (s,h)) & (m . i) = (the multF of Fi . ((s . i),(h1 . i))) by A6, A14, Def2;

          (c * b) = b by A16, GROUP_1:def 4;

          hence (eh . i) = (h1 . i) by A17, A15;

        end;

        ( dom eh) = I by A2, CARD_3: 9;

        hence (e * h) = h by A7, A13;

      end;

      hence thesis by GROUP_1: 4;

    end;

    theorem :: GROUP_7:6

    

     Th6: for F be Group-like multMagma-Family of I, G be Group-like non empty multMagma st i in I & G = (F . i) & f = ( 1_ ( product F)) holds (f . i) = ( 1_ G)

    proof

      let F be Group-like multMagma-Family of I, G be Group-like non empty multMagma such that

       A1: i in I and

       A2: G = (F . i) and

       A3: f = ( 1_ ( product F));

      set GP = ( product F);

      f in the carrier of GP by A3;

      then

       A4: f in ( product ( Carrier F)) by Def2;

      then

      reconsider e = (f . i) as Element of G by A1, A2, Lm1;

      now

        let h be Element of G;

        defpred P[ object, object] means ($1 = i implies $2 = h) & ($1 <> i implies ex H be Group-like non empty multMagma st H = (F . $1) & $2 = ( 1_ H));

        

         A5: for j be object st j in I holds ex k be object st P[j, k]

        proof

          let j be object such that

           A6: j in I;

          per cases ;

            suppose j = i;

            hence thesis;

          end;

            suppose

             A7: j <> i;

            consider Fj be Group-like non empty multMagma such that

             A8: Fj = (F . j) by A6, Def3;

            take ( 1_ Fj);

            thus j = i implies ( 1_ Fj) = h by A7;

            thus thesis by A8;

          end;

        end;

        consider g be ManySortedSet of I such that

         A9: for j be object st j in I holds P[j, (g . j)] from PBOOLE:sch 3( A5);

        

         A10: ( dom g) = I by PARTFUN1:def 2;

         A11:

        now

          let j be object;

          assume

           A12: j in ( dom g);

          then

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

          per cases ;

            suppose

             A14: i = j;

            then (g . j) = h by A9, A12;

            hence (g . j) in (( Carrier F) . j) by A2, A13, A14;

          end;

            suppose j <> i;

            then ex H be Group-like non empty multMagma st (H = (F . j)) & ((g . j) = ( 1_ H)) by A9, A12;

            hence (g . j) in (( Carrier F) . j) by A13;

          end;

        end;

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

        then

         A15: g in ( product ( Carrier F)) by A10, A11, CARD_3: 9;

        then

        reconsider g1 = g as Element of GP by Def2;

        

         A16: (g1 * ( 1_ ( product F))) = g1 by GROUP_1:def 4;

        

         A17: (g . i) = h by A1, A9;

        

         A18: (g . i) = h by A1, A9;

        ex Fi be non empty multMagma, m be Function st Fi = (F . i) & m = (the multF of GP . (g,f)) & (m . i) = (the multF of Fi . ((g . i),(f . i))) by A1, A4, A15, Def2;

        hence (h * e) = h by A2, A3, A16, A18;

        

         A19: (( 1_ ( product F)) * g1) = g1 by GROUP_1:def 4;

        ex Fi be non empty multMagma, m be Function st Fi = (F . i) & m = (the multF of GP . (f,g)) & (m . i) = (the multF of Fi . ((f . i),(g . i))) by A1, A4, A15, Def2;

        hence (e * h) = h by A2, A3, A19, A17;

      end;

      hence thesis by GROUP_1: 4;

    end;

    theorem :: GROUP_7:7

    

     Th7: for F be associative Group-like multMagma-Family of I, x be Element of ( product F) st x = g & for i be set st i in I holds ex G be Group, y be Element of G st G = (F . i) & (s . i) = (y " ) & y = (g . i) holds s = (x " )

    proof

      let F be associative Group-like multMagma-Family of I, x be Element of ( product F) such that

       A1: x = g and

       A2: for i be set st i in I holds ex G be Group, y be Element of G st G = (F . i) & (s . i) = (y " ) & y = (g . i);

      set GP = ( product F);

      

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

      

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

      now

        let i be object;

        assume

         A5: i in ( dom s);

        then

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

        ex G be Group, y be Element of G st G = (F . i) & (s . i) = (y " ) & y = (g . i) by A2, A5;

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

      end;

      then

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

      then

      reconsider f1 = s as Element of GP by Def2;

      reconsider II = ( 1_ GP), xf = (x * f1), fx = (f1 * x), x1 = x as Element of ( product ( Carrier F)) by Def2;

      

       A8: ( dom II) = I by A3, CARD_3: 9;

       A9:

      now

        let i be object;

        assume

         A10: i in I;

        then

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

         A11: G = (F . i) and

         A12: (s . i) = (y " ) and

         A13: y = (g . i) by A2;

        

         A14: ex Fi be non empty multMagma, m be Function st Fi = (F . i) & m = (the multF of GP . (s,x)) & (m . i) = (the multF of Fi . ((s . i),(x1 . i))) by A7, A10, Def2;

        ((y " ) * y) = ( 1_ G) by GROUP_1:def 5;

        hence (fx . i) = (II . i) by A1, A10, A14, A11, A12, A13, Th6;

      end;

      ( dom fx) = I by A3, CARD_3: 9;

      then

       A15: (f1 * x) = ( 1_ GP) by A8, A9;

       A16:

      now

        let i be object;

        assume

         A17: i in I;

        then

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

         A18: G = (F . i) and

         A19: (s . i) = (y " ) and

         A20: y = (g . i) by A2;

        

         A21: ex Fi be non empty multMagma, m be Function st Fi = (F . i) & m = (the multF of GP . (x,s)) & (m . i) = (the multF of Fi . ((x1 . i),(s . i))) by A7, A17, Def2;

        (y * (y " )) = ( 1_ G) by GROUP_1:def 5;

        hence (xf . i) = (II . i) by A1, A17, A21, A18, A19, A20, Th6;

      end;

      ( dom xf) = I by A3, CARD_3: 9;

      then (x * f1) = ( 1_ GP) by A8, A16;

      hence thesis by A15, GROUP_1:def 5;

    end;

    theorem :: GROUP_7:8

    

     Th8: for F be associative Group-like multMagma-Family of I, x be Element of ( product F), G be Group, y be Element of G st i in I & G = (F . i) & f = x & g = (x " ) & (f . i) = y holds (g . i) = (y " )

    proof

      let F be associative Group-like multMagma-Family of I, x be Element of ( product F), G be Group, y be Element of G such that

       A1: i in I and

       A2: G = (F . i) and

       A3: f = x and

       A4: g = (x " ) and

       A5: (f . i) = y;

      set GP = ( product F);

      

       A6: (the multF of GP . (g,f)) = ((x " ) * x) by A3, A4

      .= ( 1_ GP) by GROUP_1:def 5;

      (x " ) in the carrier of GP;

      then

       A7: g in ( product ( Carrier F)) by A4, Def2;

      then

      reconsider gi = (g . i) as Element of G by A1, A2, Lm1;

      x in the carrier of GP;

      then

       A8: f in ( product ( Carrier F)) by A3, Def2;

      then ex Fi be non empty multMagma, h be Function st Fi = (F . i) & h = (the multF of GP . (g,f)) & (h . i) = (the multF of Fi . ((g . i),(f . i))) by A1, A7, Def2;

      then

       A9: (gi * y) = ( 1_ G) by A1, A2, A5, A6, Th6;

      

       A10: (the multF of GP . (f,g)) = (x * (x " )) by A3, A4

      .= ( 1_ GP) by GROUP_1:def 5;

      ex Fi be non empty multMagma, h be Function st Fi = (F . i) & h = (the multF of GP . (f,g)) & (h . i) = (the multF of Fi . ((f . i),(g . i))) by A1, A8, A7, Def2;

      then (y * gi) = ( 1_ G) by A1, A2, A5, A10, Th6;

      hence thesis by A9, GROUP_1:def 5;

    end;

    definition

      let I be set, F be associative Group-like multMagma-Family of I;

      :: GROUP_7:def9

      func sum F -> strict Subgroup of ( product F) means

      : Def9: for x be object holds x in the carrier of it iff ex g be Element of ( product ( Carrier F)), J be finite Subset of I, f be ManySortedSet of J st g = ( 1_ ( product F)) & x = (g +* f) & for j be set st j in J holds ex G be Group-like non empty multMagma st G = (F . j) & (f . j) in the carrier of G & (f . j) <> ( 1_ G);

      existence

      proof

        set GP = ( product F), CF = ( Carrier F);

        

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

        reconsider g = ( 1_ GP) as Element of ( product CF) by Def2;

        

         A2: ( dom g) = ( dom CF) by CARD_3: 9;

        defpred P[ object] means ex J be finite Subset of I, f be ManySortedSet of J st $1 = (g +* f) & for j be set st j in J holds ex G be Group-like non empty multMagma st G = (F . j) & (f . j) in the carrier of G & (f . j) <> ( 1_ G);

        consider A be set such that

         A3: for x be object holds x in A iff x in ( product CF) & P[x] from XBOOLE_0:sch 1;

        

         A4: A c= the carrier of GP

        proof

          let a be object;

          assume a in A;

          then a in ( product CF) by A3;

          hence thesis by Def2;

        end;

        

         A5: P[g]

        proof

          set J = ( {} I);

          ( dom {} ) = J;

          then

          reconsider f = {} as ManySortedSet of J by PARTFUN1:def 2, RELAT_1:def 18;

          take J, f;

          

          thus g = (g +* {} )

          .= (g +* f);

          thus thesis;

        end;

        then

        reconsider A as non empty set by A3;

        set b = (the multF of GP || A);

        

         A6: for p be Element of ( product CF) holds ( dom p) = I by PARTFUN1:def 2;

        ( dom b) = [:A, A:] & ( rng b) c= A

        proof

          ( dom the multF of GP) = [:the carrier of GP, the carrier of GP:] by FUNCT_2:def 1;

          hence

           A7: ( dom b) = [:A, A:] by A4, RELAT_1: 62, ZFMISC_1: 96;

          let y be object;

          assume y in ( rng b);

          then

          consider x be object such that

           A8: x in ( dom b) and

           A9: (b . x) = y by FUNCT_1:def 3;

          consider x1,x2 be object such that

           A10: x1 in A and

           A11: x2 in A and

           A12: x = [x1, x2] by A7, A8, ZFMISC_1:def 2;

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

           A13: x1 = (g +* f1) and

           A14: for j be set st j in J1 holds ex G be Group-like non empty multMagma st G = (F . j) & (f1 . j) in the carrier of G & (f1 . j) <> ( 1_ G) by A3, A10;

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

           A15: x2 = (g +* f2) and

           A16: for j be set st j in J2 holds ex G be Group-like non empty multMagma st G = (F . j) & (f2 . j) in the carrier of G & (f2 . j) <> ( 1_ G) by A3, A11;

          reconsider x1, x2 as Function by A13, A15;

          

           A17: ( dom f1) = J1 by PARTFUN1:def 2;

           A18:

          now

            let i be object;

            assume

             A19: i in I;

            then

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

            per cases ;

              suppose

               A21: i in J1;

              then ex G be Group-like non empty multMagma st G = (F . i) & (f1 . i) in the carrier of G & (f1 . i) <> ( 1_ G) by A14;

              hence (x1 . i) in (CF . i) by A13, A17, A20, A21, FUNCT_4: 13;

            end;

              suppose

               A22: not i in J1;

              consider G be Group-like non empty multMagma such that

               A23: G = (F . i) by A19, Def3;

              (x1 . i) = (g . i) by A13, A17, A22, FUNCT_4: 11

              .= ( 1_ G) by A19, A23, Th6;

              hence (x1 . i) in (CF . i) by A20, A23;

            end;

          end;

          

           A24: ( dom f2) = J2 by PARTFUN1:def 2;

           A25:

          now

            let i be object;

            assume

             A26: i in I;

            then

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

            per cases ;

              suppose

               A28: i in J2;

              then ex G be Group-like non empty multMagma st G = (F . i) & (f2 . i) in the carrier of G & (f2 . i) <> ( 1_ G) by A16;

              hence (x2 . i) in (CF . i) by A15, A24, A27, A28, FUNCT_4: 13;

            end;

              suppose

               A29: not i in J2;

              consider G be Group-like non empty multMagma such that

               A30: G = (F . i) by A26, Def3;

              (x2 . i) = (g . i) by A15, A24, A29, FUNCT_4: 11

              .= ( 1_ G) by A26, A30, Th6;

              hence (x2 . i) in (CF . i) by A27, A30;

            end;

          end;

          

           A31: ( dom x1) = (( dom g) \/ ( dom f1)) by A13, FUNCT_4:def 1

          .= I by A2, A1, A17, XBOOLE_1: 12;

          ( dom x2) = (( dom g) \/ ( dom f2)) by A15, FUNCT_4:def 1

          .= I by A2, A1, A24, XBOOLE_1: 12;

          then

          reconsider x2 as Element of ( product CF) by A1, A25, CARD_3: 9;

          reconsider x1 as Element of ( product CF) by A1, A31, A18, CARD_3: 9;

          reconsider X1 = x1, X2 = x2 as Element of GP by Def2;

          

           A32: [x1, x2] in [:A, A:] by A10, A11, ZFMISC_1: 87;

          then

           A33: y = (X1 * X2) by A9, A12, FUNCT_1: 49;

          then

          reconsider y1 = y as Element of ( product CF) by Def2;

          defpred S[ object] means ex G be Group-like non empty multMagma, k1,k2 be Element of G st G = (F . $1) & k1 = (x1 . $1) & k2 = (x2 . $1) & (k1 * k2) = ( 1_ G) & (f1 . $1) <> ( 1_ G) & (f2 . $1) <> ( 1_ G);

          consider K be set such that

           A34: for k be object holds k in K iff k in I & S[k] from XBOOLE_0:sch 1;

          

           A35: P[y]

          proof

            defpred R[ object, object] means ex G be Group-like non empty multMagma, k1,k2 be Element of G st G = (F . $1) & k1 = (x1 . $1) & k2 = (x2 . $1) & $2 = (k1 * k2);

            reconsider J = ((J1 \/ J2) \ K) as finite Subset of I;

            take J;

            

             A36: ( dom y1) = I by A6;

            

             A37: for j be object st j in J holds ex t be object st R[j, t]

            proof

              let j be object;

              assume

               A38: j in J;

              then

              consider G be Group-like non empty multMagma such that

               A39: G = (F . j) by Def3;

              reconsider k1 = (x1 . j), k2 = (x2 . j) as Element of G by A38, A39, Lm1;

              take (k1 * k2);

              thus thesis by A39;

            end;

            consider f be ManySortedSet of J such that

             A40: for j be object st j in J holds R[j, (f . j)] from PBOOLE:sch 3( A37);

            take f;

            set gf = (g +* f);

            

             A41: ( dom f) = J by PARTFUN1:def 2;

             A42:

            now

              let i be object;

              assume

               A43: i in I;

              then

              consider Fi be non empty multMagma, h be Function such that

               A44: Fi = (F . i) and

               A45: h = (the multF of GP . (x1,x2)) and

               A46: (h . i) = (the multF of Fi . ((x1 . i),(x2 . i))) by Def2;

              consider FF be Group-like non empty multMagma such that

               A47: FF = (F . i) by A43, Def3;

              reconsider Fi as Group-like non empty multMagma by A44, A47;

              reconsider x1i = (x1 . i), x2i = (x2 . i) as Element of Fi by A43, A44, Lm1;

              

               A48: (y1 . i) = (x1i * x2i) by A9, A12, A32, A45, A46, FUNCT_1: 49;

              per cases ;

                suppose

                 A49: i in J;

                then ex GG be Group-like non empty multMagma, k1a,k2a be Element of GG st GG = (F . i) & k1a = (x1 . i) & k2a = (x2 . i) & (f . i) = (k1a * k2a) by A40;

                hence (y1 . i) = (gf . i) by A33, A41, A44, A45, A46, A49, FUNCT_4: 13;

              end;

                suppose

                 A50: not i in J;

                

                then

                 A51: (gf . i) = (g . i) by A41, FUNCT_4: 11

                .= ( 1_ FF) by A43, A47, Th6;

                now

                  per cases by A50, XBOOLE_0:def 5;

                    case

                     A52: not i in (J1 \/ J2);

                    then not i in J2 by XBOOLE_0:def 3;

                    then (x2 . i) = (g . i) by A15, A24, FUNCT_4: 11;

                    then

                     A53: (x2 . i) = ( 1_ FF) by A43, A47, Th6;

                     not i in J1 by A52, XBOOLE_0:def 3;

                    then (x1 . i) = (g . i) by A13, A17, FUNCT_4: 11;

                    then (x1 . i) = ( 1_ FF) by A43, A47, Th6;

                    hence (y1 . i) = (gf . i) by A44, A47, A48, A51, A53, GROUP_1:def 4;

                  end;

                    case i in K;

                    then ex GG be Group-like non empty multMagma, k1,k2 be Element of GG st GG = (F . i) & k1 = (x1 . i) & k2 = (x2 . i) & (k1 * k2) = ( 1_ GG) & (f1 . i) <> ( 1_ GG) & (f2 . i) <> ( 1_ GG) by A34;

                    hence (y1 . i) = (gf . i) by A33, A43, A47, A51, Th1;

                  end;

                end;

                hence (y1 . i) = (gf . i);

              end;

            end;

            ( dom gf) = (( dom g) \/ ( dom f)) by FUNCT_4:def 1

            .= I by A2, A1, A41, XBOOLE_1: 12;

            hence y = gf by A36, A42, FUNCT_1: 2;

            let j be set;

            assume

             A54: j in J;

            then

            consider G be Group-like non empty multMagma, k1,k2 be Element of G such that

             A55: G = (F . j) and

             A56: k1 = (x1 . j) and

             A57: k2 = (x2 . j) and

             A58: (f . j) = (k1 * k2) by A40;

            take G;

            thus G = (F . j) by A55;

            thus (f . j) in the carrier of G by A58;

            

             A59: j in (J1 \/ J2) by A54, XBOOLE_0:def 5;

            per cases by A59, XBOOLE_0:def 3;

              suppose

               A60: j in J1 & not j in J2;

              then

               A61: (x1 . j) = (f1 . j) by A13, A17, FUNCT_4: 13;

              consider G1 be Group-like non empty multMagma such that

               A62: G1 = (F . j) and (f1 . j) in the carrier of G1 and

               A63: (f1 . j) <> ( 1_ G1) by A14, A60;

              (x2 . j) = (g . j) by A15, A24, A60, FUNCT_4: 11

              .= ( 1_ G1) by A54, A62, Th6;

              hence thesis by A55, A56, A57, A58, A61, A62, A63, GROUP_1:def 4;

            end;

              suppose

               A64: not j in J1 & j in J2;

              then

               A65: (x2 . j) = (f2 . j) by A15, A24, FUNCT_4: 13;

              consider G2 be Group-like non empty multMagma such that

               A66: G2 = (F . j) and (f2 . j) in the carrier of G2 and

               A67: (f2 . j) <> ( 1_ G2) by A16, A64;

              (x1 . j) = (g . j) by A13, A17, A64, FUNCT_4: 11

              .= ( 1_ G2) by A54, A66, Th6;

              hence thesis by A55, A56, A57, A58, A65, A66, A67, GROUP_1:def 4;

            end;

              suppose

               A68: j in J1 & j in J2;

              then

               A69: ex G2 be Group-like non empty multMagma st G2 = (F . j) & (f2 . j) in the carrier of G2 & (f2 . j) <> ( 1_ G2) by A16;

              

               A70: not j in K by A54, XBOOLE_0:def 5;

              ex G1 be Group-like non empty multMagma st G1 = (F . j) & (f1 . j) in the carrier of G1 & (f1 . j) <> ( 1_ G1) by A14, A68;

              hence thesis by A34, A54, A55, A56, A57, A58, A69, A70;

            end;

          end;

          reconsider ff = (X1 * X2) as Element of ( product CF) by Def2;

          now

            reconsider J = {} as finite Subset of I by XBOOLE_1: 2;

            take J;

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

          end;

          hence thesis by A3, A33, A35;

        end;

        then

        reconsider b as BinOp of A by FUNCT_2:def 1, RELSET_1: 4;

        set H = multMagma (# A, b #);

        H is Group-like

        proof

          reconsider e = g as Element of H by A3, A5;

          take e;

          let h be Element of H;

          reconsider h1 = h as Element of GP by A4;

           [h, e] in [:A, A:] by ZFMISC_1: 87;

          

          hence (h * e) = (h1 * ( 1_ GP)) by FUNCT_1: 49

          .= h by GROUP_1:def 4;

           [e, h] in [:A, A:] by ZFMISC_1: 87;

          

          hence (e * h) = (( 1_ GP) * h1) by FUNCT_1: 49

          .= h by GROUP_1:def 4;

          reconsider h2 = h1, hh = (h1 " ) as Element of ( product ( Carrier F)) by Def2;

          

           A71: P[(h1 " )]

          proof

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

             A72: h = (g +* f) and

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

            defpred W[ object, object] means ex G be Group, m be Element of G st G = (F . $1) & m = (f . $1) & $2 = (m " );

            

             A74: for i be object st i in J holds ex j be object st W[i, j]

            proof

              let i be object;

              assume

               A75: i in J;

              then

              consider Gg be Group-like non empty multMagma such that

               A76: Gg = (F . i) by Def3;

              ex Ga be associative non empty multMagma st Ga = (F . i) by A75, Def4;

              then

              reconsider G = Gg as Group by A76;

              ex GG be Group-like non empty multMagma st GG = (F . i) & (f . i) in the carrier of GG & (f . i) <> ( 1_ GG) by A73, A75;

              then

              reconsider m = (f . i) as Element of G by A76;

              take (m " );

              thus thesis by A76;

            end;

            consider f9 be ManySortedSet of J such that

             A77: for j be object st j in J holds W[j, (f9 . j)] from PBOOLE:sch 3( A74);

            set gf9 = (g +* f9);

            

             A78: ( dom f9) = J by PARTFUN1:def 2;

            

             A79: ( dom f) = J by PARTFUN1:def 2;

             A80:

            now

              let i be object;

              assume

               A81: i in I;

              then

              consider G3 be Group-like non empty multMagma such that

               A82: G3 = (F . i) by Def3;

              ex G4 be associative non empty multMagma st G4 = (F . i) by A81, Def4;

              then

              consider G5 be Group such that

               A83: G5 = (F . i) by A82;

              per cases ;

                suppose

                 A84: i in J;

                then

                 A85: (gf9 . i) = (f9 . i) by A78, FUNCT_4: 13;

                

                 A86: ex G be Group, m be Element of G st G = (F . i) & m = (f . i) & (f9 . i) = (m " ) by A77, A84;

                (h2 . i) = (f . i) by A72, A79, A84, FUNCT_4: 13;

                hence (hh . i) = (gf9 . i) by A81, A86, A85, Th8;

              end;

                suppose

                 A87: not i in J;

                

                then

                 A88: (gf9 . i) = (g . i) by A78, FUNCT_4: 11

                .= ( 1_ G3) by A81, A82, Th6;

                

                 A89: ( 1_ G5) = (( 1_ G5) " ) by GROUP_1: 8;

                (h2 . i) = (g . i) by A72, A79, A87, FUNCT_4: 11

                .= ( 1_ G3) by A81, A82, Th6;

                hence (hh . i) = (gf9 . i) by A81, A82, A83, A88, A89, Th8;

              end;

            end;

            take J;

            take f9;

            

             A90: ( dom hh) = I by A6;

            ( dom gf9) = (( dom g) \/ ( dom f9)) by FUNCT_4:def 1

            .= I by A2, A1, A78, XBOOLE_1: 12;

            hence (h1 " ) = (g +* f9) by A90, A80;

            let j be set;

            assume

             A91: j in J;

            then

            consider G be Group, m be Element of G such that

             A92: G = (F . j) and

             A93: m = (f . j) and

             A94: (f9 . j) = (m " ) by A77;

            take G;

            thus G = (F . j) & (f9 . j) in the carrier of G by A92, A94;

            ex G1 be Group-like non empty multMagma st G1 = (F . j) & (f . j) in the carrier of G1 & (f . j) <> ( 1_ G1) by A73, A91;

            hence thesis by A92, A93, A94, GROUP_1: 10;

          end;

          ( product CF) = the carrier of GP by Def2;

          then

          reconsider h9 = (h1 " ) as Element of H by A3, A71;

          take h9;

           [h, h9] in [:A, A:] by ZFMISC_1: 87;

          

          hence (h * h9) = (h1 * (h1 " )) by FUNCT_1: 49

          .= e by GROUP_1:def 5;

           [h9, h] in [:A, A:] by ZFMISC_1: 87;

          

          hence (h9 * h) = ((h1 " ) * h1) by FUNCT_1: 49

          .= e by GROUP_1:def 5;

        end;

        then

        reconsider H as Group-like non empty multMagma;

        reconsider H as strict Subgroup of GP by A4, GROUP_2:def 5;

        take H;

        let x be object;

        hereby

          assume x in the carrier of H;

          then P[x] by A3;

          hence ex g be Element of ( product CF), J be finite Subset of I, f be ManySortedSet of J st g = ( 1_ ( product F)) & x = (g +* f) & for j be set st j in J holds ex G be Group-like non empty multMagma st G = (F . j) & (f . j) in the carrier of G & (f . j) <> ( 1_ G);

        end;

        given g be Element of ( product CF), J be finite Subset of I, f be ManySortedSet of J such that

         A95: g = ( 1_ ( product F)) and

         A96: x = (g +* f) and

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

        

         A98: ( dom g) = I by A6;

        set gf = (g +* f);

        

         A99: ( dom f) = J by PARTFUN1:def 2;

         A100:

        now

          let i be object;

          assume

           A101: i in I;

          then

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

          per cases ;

            suppose

             A103: i in J;

            then ex G be Group-like non empty multMagma st (G = (F . i)) & ((f . i) in the carrier of G) & ((f . i) <> ( 1_ G)) by A97;

            hence (gf . i) in (CF . i) by A99, A102, A103, FUNCT_4: 13;

          end;

            suppose

             A104: not i in J;

            consider G be Group-like non empty multMagma such that

             A105: G = (F . i) by A101, Def3;

            (gf . i) = (g . i) by A99, A104, FUNCT_4: 11

            .= ( 1_ G) by A95, A101, A105, Th6;

            hence (gf . i) in (CF . i) by A102, A105;

          end;

        end;

        ( dom gf) = (( dom g) \/ ( dom f)) by FUNCT_4:def 1

        .= I by A98, A99, XBOOLE_1: 12;

        then x in ( product CF) by A1, A96, A100, CARD_3: 9;

        hence thesis by A3, A95, A96, A97;

      end;

      uniqueness

      proof

        defpred P[ object] means ex g be Element of ( product ( Carrier F)), J be finite Subset of I, f be ManySortedSet of J st g = ( 1_ ( product F)) & $1 = (g +* f) & for j be set st j in J holds ex G be Group-like non empty multMagma st G = (F . j) & (f . j) in the carrier of G & (f . j) <> ( 1_ G);

        let A,B be strict Subgroup of ( product F) such that

         A106: for x be object holds x in the carrier of A iff P[x] and

         A107: for x be object holds x in the carrier of B iff P[x];

        the carrier of A = the carrier of B from XBOOLE_0:sch 2( A106, A107);

        hence thesis by GROUP_2: 59;

      end;

    end

    registration

      let I be set, F be associative Group-like multMagma-Family of I, f,g be Element of ( sum F);

      cluster (the multF of ( sum F) . (f,g)) -> Function-like Relation-like;

      coherence

      proof

        

         A1: (the multF of ( sum F) . (f,g)) in the carrier of ( sum F);

        the carrier of ( sum F) c= the carrier of ( product F) by GROUP_2:def 5;

        then

        reconsider h = (the multF of ( sum F) . (f,g)) as Element of ( product ( Carrier F)) by A1, Def2;

        h is Function;

        hence thesis;

      end;

    end

    theorem :: GROUP_7:9

    for I be finite set, F be associative Group-like multMagma-Family of I holds ( product F) = ( sum F)

    proof

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

      set GP = ( product F), S = ( sum F);

      

       A1: the carrier of S = the carrier of GP

      proof

        reconsider g = ( 1_ GP) as Element of ( product ( Carrier F)) by Def2;

        thus the carrier of S c= the carrier of GP by GROUP_2:def 5;

        let x be object;

        assume x in the carrier of GP;

        then

        reconsider f = x as Element of ( product ( Carrier F)) by Def2;

        

         A2: for p be Element of ( product ( Carrier F)) holds ( dom p) = I by PARTFUN1:def 2;

        then

         A3: ( dom f) = I;

        reconsider f as ManySortedSet of I;

        ex g be Element of ( product ( Carrier F)), J be finite Subset of I, f be ManySortedSet of J st g = ( 1_ GP) & x = (g +* f) & for j be set st j in J holds ex G be Group-like non empty multMagma st G = (F . j) & (f . j) in the carrier of G & (f . j) <> ( 1_ G)

        proof

          deffunc F( object) = (f . $1);

          defpred P[ object] means ex G be Group-like non empty multMagma, m be Element of G st G = (F . $1) & m = (f . $1) & m <> ( 1_ G);

          consider J be set such that

           A4: for j be object holds j in J iff j in I & P[j] from XBOOLE_0:sch 1;

          J c= I by A4;

          then

          reconsider J as Subset of I;

          consider ff be ManySortedSet of J such that

           A5: for j be object st j in J holds (ff . j) = F(j) from PBOOLE:sch 4;

          

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

           A7:

          now

            let i be object such that

             A8: i in I;

            per cases ;

              suppose

               A9: i in J;

              

              hence (f . i) = (ff . i) by A5

              .= ((g +* ff) . i) by A6, A9, FUNCT_4: 13;

            end;

              suppose

               A10: not i in J;

              consider G be Group-like non empty multMagma such that

               A11: G = (F . i) by A8, Def3;

              (f . i) is Element of G by A8, A11, Lm1;

              

              hence (f . i) = ( 1_ G) by A4, A8, A10, A11

              .= (g . i) by A8, A11, Th6

              .= ((g +* ff) . i) by A6, A10, FUNCT_4: 11;

            end;

          end;

          take g, J;

          take ff;

          thus g = ( 1_ GP);

          

           A12: ( dom g) = I by A2;

          ( dom (g +* ff)) = (( dom g) \/ ( dom ff)) by FUNCT_4:def 1

          .= I by A6, A12, XBOOLE_1: 12;

          hence x = (g +* ff) by A3, A7, FUNCT_1: 2;

          let j be set;

          assume

           A13: j in J;

          then

          consider G be Group-like non empty multMagma, m be Element of G such that

           A14: G = (F . j) and

           A15: m = (f . j) and

           A16: m <> ( 1_ G) by A4;

          take G;

          (ff . j) = (f . j) by A5, A13;

          hence thesis by A14, A15, A16;

        end;

        hence thesis by Def9;

      end;

      ( product F) is Subgroup of ( product F) by GROUP_2: 54;

      hence thesis by A1, GROUP_2: 59;

    end;

    begin

    theorem :: GROUP_7:10

    

     Th10: for G1 be non empty multMagma holds <*G1*> is multMagma-Family of {1}

    proof

      let G1 be non empty multMagma;

      ( dom <*G1*>) = {1} by FINSEQ_1: 2, FINSEQ_1:def 8;

      then

      reconsider A = <*G1*> as ManySortedSet of {1} by PARTFUN1:def 2, RELAT_1:def 18;

      A is multMagma-yielding

      proof

        let y be set;

        assume y in ( rng A);

        then

        consider x be object such that

         A1: x in ( dom A) and

         A2: (A . x) = y by FUNCT_1:def 3;

        x = 1 by A1, TARSKI:def 1;

        hence thesis by A2, FINSEQ_1:def 8;

      end;

      hence thesis;

    end;

    registration

      let G1 be non empty multMagma;

      cluster <*G1*> -> {1} -defined;

      coherence by Th10;

    end

    registration

      let G1 be non empty multMagma;

      cluster <*G1*> -> total multMagma-yielding;

      coherence by Th10;

    end

    theorem :: GROUP_7:11

    

     Th11: for G1 be Group-like non empty multMagma holds <*G1*> is Group-like multMagma-Family of {1}

    proof

      let G1 be Group-like non empty multMagma;

      reconsider A = <*G1*> as multMagma-Family of {1};

      A is Group-like

      proof

        let x be Element of {1};

        x = 1 by TARSKI:def 1;

        hence thesis by FINSEQ_1:def 8;

      end;

      hence thesis;

    end;

    registration

      let G1 be Group-like non empty multMagma;

      cluster <*G1*> -> Group-like;

      coherence by Th11;

    end

    theorem :: GROUP_7:12

    

     Th12: for G1 be associative non empty multMagma holds <*G1*> is associative multMagma-Family of {1}

    proof

      let G1 be associative non empty multMagma;

      reconsider A = <*G1*> as multMagma-Family of {1};

      A is associative

      proof

        let x be Element of {1};

        x = 1 by TARSKI:def 1;

        hence thesis by FINSEQ_1:def 8;

      end;

      hence thesis;

    end;

    registration

      let G1 be associative non empty multMagma;

      cluster <*G1*> -> associative;

      coherence by Th12;

    end

    theorem :: GROUP_7:13

    

     Th13: for G1 be commutative non empty multMagma holds <*G1*> is commutative multMagma-Family of {1}

    proof

      let G1 be commutative non empty multMagma;

      reconsider A = <*G1*> as multMagma-Family of {1};

      A is commutative

      proof

        let x be Element of {1};

        x = 1 by TARSKI:def 1;

        hence thesis by FINSEQ_1:def 8;

      end;

      hence thesis;

    end;

    registration

      let G1 be commutative non empty multMagma;

      cluster <*G1*> -> commutative;

      coherence by Th13;

    end

    theorem :: GROUP_7:14

    for G1 be Group holds <*G1*> is Group-like associative multMagma-Family of {1};

    theorem :: GROUP_7:15

    for G1 be commutative Group holds <*G1*> is commutative Group-like associative multMagma-Family of {1};

    registration

      let G1 be non empty multMagma;

      cluster -> FinSequence-like for Element of ( product ( Carrier <*G1*>));

      coherence by FINSEQ_1: 2, PARTFUN1:def 2;

    end

    registration

      let G1 be non empty multMagma;

      cluster -> FinSequence-like for Element of ( product <*G1*>);

      coherence

      proof

        let x be Element of ( product <*G1*>);

        reconsider y = x as Element of ( product ( Carrier <*G1*>)) by Def2;

        y is FinSequence-like;

        hence thesis;

      end;

    end

    definition

      let G1 be non empty multMagma, x be Element of G1;

      :: original: <*

      redefine

      func <*x*> -> Element of ( product <*G1*>) ;

      coherence

      proof

        set xy = <*x*>, G = <*G1*>;

        

         A1: ( dom ( Carrier G)) = {1} by PARTFUN1:def 2;

        

         A2: (G . 1) = G1 by FINSEQ_1:def 8;

        

         A3: (xy . 1) = x by FINSEQ_1:def 8;

        

         A4: for a be object st a in {1} holds (xy . a) in (( Carrier G) . a)

        proof

          let a be object;

          assume

           A5: a in {1};

          then

           A6: a = 1 by TARSKI:def 1;

          then ex R be 1-sorted st R = (G . 1) & (( Carrier G) . 1) = the carrier of R by A5, PRALG_1:def 15;

          hence thesis by A3, A2, A6;

        end;

        ( dom xy) = {1} by FINSEQ_1: 2, FINSEQ_1:def 8;

        then xy in ( product ( Carrier G)) by A1, A4, CARD_3: 9;

        hence thesis by Def2;

      end;

    end

    theorem :: GROUP_7:16

    

     Th16: for G1,G2 be non empty multMagma holds <*G1, G2*> is multMagma-Family of {1, 2}

    proof

      let G1,G2 be non empty multMagma;

      ( dom <*G1, G2*>) = {1, 2} by FINSEQ_1: 2, FINSEQ_1: 89;

      then

      reconsider A = <*G1, G2*> as ManySortedSet of {1, 2} by PARTFUN1:def 2, RELAT_1:def 18;

      A is multMagma-yielding

      proof

        let y be set;

        assume y in ( rng A);

        then

        consider x be object such that

         A1: x in ( dom A) and

         A2: (A . x) = y by FUNCT_1:def 3;

        x = 1 or x = 2 by A1, TARSKI:def 2;

        hence thesis by A2, FINSEQ_1: 44;

      end;

      hence thesis;

    end;

    registration

      let G1,G2 be non empty multMagma;

      cluster <*G1, G2*> -> {1, 2} -defined;

      coherence by Th16;

    end

    registration

      let G1,G2 be non empty multMagma;

      cluster <*G1, G2*> -> total multMagma-yielding;

      coherence by Th16;

    end

    theorem :: GROUP_7:17

    

     Th17: for G1,G2 be Group-like non empty multMagma holds <*G1, G2*> is Group-like multMagma-Family of {1, 2}

    proof

      let G1,G2 be Group-like non empty multMagma;

      reconsider A = <*G1, G2*> as multMagma-Family of {1, 2};

      A is Group-like

      proof

        let x be Element of {1, 2};

        x = 1 or x = 2 by TARSKI:def 2;

        hence thesis by FINSEQ_1: 44;

      end;

      hence thesis;

    end;

    registration

      let G1,G2 be Group-like non empty multMagma;

      cluster <*G1, G2*> -> Group-like;

      coherence by Th17;

    end

    theorem :: GROUP_7:18

    

     Th18: for G1,G2 be associative non empty multMagma holds <*G1, G2*> is associative multMagma-Family of {1, 2}

    proof

      let G1,G2 be associative non empty multMagma;

      reconsider A = <*G1, G2*> as multMagma-Family of {1, 2};

      A is associative

      proof

        let x be Element of {1, 2};

        x = 1 or x = 2 by TARSKI:def 2;

        hence thesis by FINSEQ_1: 44;

      end;

      hence thesis;

    end;

    registration

      let G1,G2 be associative non empty multMagma;

      cluster <*G1, G2*> -> associative;

      coherence by Th18;

    end

    theorem :: GROUP_7:19

    

     Th19: for G1,G2 be commutative non empty multMagma holds <*G1, G2*> is commutative multMagma-Family of {1, 2}

    proof

      let G1,G2 be commutative non empty multMagma;

      reconsider A = <*G1, G2*> as multMagma-Family of {1, 2};

      A is commutative

      proof

        let x be Element of {1, 2};

        x = 1 or x = 2 by TARSKI:def 2;

        hence thesis by FINSEQ_1: 44;

      end;

      hence thesis;

    end;

    registration

      let G1,G2 be commutative non empty multMagma;

      cluster <*G1, G2*> -> commutative;

      coherence by Th19;

    end

    theorem :: GROUP_7:20

    for G1,G2 be Group holds <*G1, G2*> is Group-like associative multMagma-Family of {1, 2};

    theorem :: GROUP_7:21

    for G1,G2 be commutative Group holds <*G1, G2*> is Group-like associative commutative multMagma-Family of {1, 2};

    registration

      let G1,G2 be non empty multMagma;

      cluster -> FinSequence-like for Element of ( product ( Carrier <*G1, G2*>));

      coherence by FINSEQ_1: 2, PARTFUN1:def 2;

    end

    registration

      let G1,G2 be non empty multMagma;

      cluster -> FinSequence-like for Element of ( product <*G1, G2*>);

      coherence

      proof

        let x be Element of ( product <*G1, G2*>);

        reconsider y = x as Element of ( product ( Carrier <*G1, G2*>)) by Def2;

        y is FinSequence-like;

        hence thesis;

      end;

    end

    definition

      let G1,G2 be non empty multMagma, x be Element of G1, y be Element of G2;

      :: original: <*

      redefine

      func <*x,y*> -> Element of ( product <*G1, G2*>) ;

      coherence

      proof

        set xy = <*x, y*>, G = <*G1, G2*>;

        

         A1: ( dom ( Carrier G)) = {1, 2} by PARTFUN1:def 2;

        

         A2: (xy . 2) = y by FINSEQ_1: 44;

        

         A3: (G . 2) = G2 by FINSEQ_1: 44;

        

         A4: (G . 1) = G1 by FINSEQ_1: 44;

        

         A5: (xy . 1) = x by FINSEQ_1: 44;

        

         A6: for a be object st a in {1, 2} holds (xy . a) in (( Carrier G) . a)

        proof

          let a be object;

          assume

           A7: a in {1, 2};

          per cases by A7, TARSKI:def 2;

            suppose

             A8: a = 1;

            then ex R be 1-sorted st R = (G . 1) & (( Carrier G) . 1) = the carrier of R by A7, PRALG_1:def 15;

            hence thesis by A5, A4, A8;

          end;

            suppose

             A9: a = 2;

            then ex R be 1-sorted st R = (G . 2) & (( Carrier G) . 2) = the carrier of R by A7, PRALG_1:def 15;

            hence thesis by A2, A3, A9;

          end;

        end;

        ( dom xy) = {1, 2} by FINSEQ_1: 2, FINSEQ_1: 89;

        then xy in ( product ( Carrier G)) by A1, A6, CARD_3: 9;

        hence thesis by Def2;

      end;

    end

    theorem :: GROUP_7:22

    

     Th22: for G1,G2,G3 be non empty multMagma holds <*G1, G2, G3*> is multMagma-Family of {1, 2, 3}

    proof

      let G1,G2,G3 be non empty multMagma;

      ( dom <*G1, G2, G3*>) = {1, 2, 3} by FINSEQ_1: 89, FINSEQ_3: 1;

      then

      reconsider A = <*G1, G2, G3*> as ManySortedSet of {1, 2, 3} by PARTFUN1:def 2, RELAT_1:def 18;

      A is multMagma-yielding

      proof

        let y be set;

        assume y in ( rng A);

        then

        consider x be object such that

         A1: x in ( dom A) and

         A2: (A . x) = y by FUNCT_1:def 3;

        x = 1 or x = 2 or x = 3 by A1, ENUMSET1:def 1;

        hence thesis by A2, FINSEQ_1: 45;

      end;

      hence thesis;

    end;

    registration

      let G1,G2,G3 be non empty multMagma;

      cluster <*G1, G2, G3*> -> {1, 2, 3} -defined;

      coherence by Th22;

    end

    registration

      let G1,G2,G3 be non empty multMagma;

      cluster <*G1, G2, G3*> -> total multMagma-yielding;

      coherence by Th22;

    end

    theorem :: GROUP_7:23

    

     Th23: for G1,G2,G3 be Group-like non empty multMagma holds <*G1, G2, G3*> is Group-like multMagma-Family of {1, 2, 3}

    proof

      let G1,G2,G3 be Group-like non empty multMagma;

      reconsider A = <*G1, G2, G3*> as multMagma-Family of {1, 2, 3};

      A is Group-like

      proof

        let x be Element of {1, 2, 3};

        x = 1 or x = 2 or x = 3 by ENUMSET1:def 1;

        hence thesis by FINSEQ_1: 45;

      end;

      hence thesis;

    end;

    registration

      let G1,G2,G3 be Group-like non empty multMagma;

      cluster <*G1, G2, G3*> -> Group-like;

      coherence by Th23;

    end

    theorem :: GROUP_7:24

    

     Th24: for G1,G2,G3 be associative non empty multMagma holds <*G1, G2, G3*> is associative multMagma-Family of {1, 2, 3}

    proof

      let G1,G2,G3 be associative non empty multMagma;

      reconsider A = <*G1, G2, G3*> as multMagma-Family of {1, 2, 3};

      A is associative

      proof

        let x be Element of {1, 2, 3};

        x = 1 or x = 2 or x = 3 by ENUMSET1:def 1;

        hence thesis by FINSEQ_1: 45;

      end;

      hence thesis;

    end;

    registration

      let G1,G2,G3 be associative non empty multMagma;

      cluster <*G1, G2, G3*> -> associative;

      coherence by Th24;

    end

    theorem :: GROUP_7:25

    

     Th25: for G1,G2,G3 be commutative non empty multMagma holds <*G1, G2, G3*> is commutative multMagma-Family of {1, 2, 3}

    proof

      let G1,G2,G3 be commutative non empty multMagma;

      reconsider A = <*G1, G2, G3*> as multMagma-Family of {1, 2, 3};

      A is commutative

      proof

        let x be Element of {1, 2, 3};

        x = 1 or x = 2 or x = 3 by ENUMSET1:def 1;

        hence thesis by FINSEQ_1: 45;

      end;

      hence thesis;

    end;

    registration

      let G1,G2,G3 be commutative non empty multMagma;

      cluster <*G1, G2, G3*> -> commutative;

      coherence by Th25;

    end

    theorem :: GROUP_7:26

    for G1,G2,G3 be Group holds <*G1, G2, G3*> is Group-like associative multMagma-Family of {1, 2, 3};

    theorem :: GROUP_7:27

    for G1,G2,G3 be commutative Group holds <*G1, G2, G3*> is Group-like associative commutative multMagma-Family of {1, 2, 3};

    registration

      let G1,G2,G3 be non empty multMagma;

      cluster -> FinSequence-like for Element of ( product ( Carrier <*G1, G2, G3*>));

      coherence by FINSEQ_3: 1, PARTFUN1:def 2;

    end

    registration

      let G1,G2,G3 be non empty multMagma;

      cluster -> FinSequence-like for Element of ( product <*G1, G2, G3*>);

      coherence

      proof

        let x be Element of ( product <*G1, G2, G3*>);

        reconsider y = x as Element of ( product ( Carrier <*G1, G2, G3*>)) by Def2;

        y is FinSequence-like;

        hence thesis;

      end;

    end

    definition

      let G1,G2,G3 be non empty multMagma, x be Element of G1, y be Element of G2, z be Element of G3;

      :: original: <*

      redefine

      func <*x,y,z*> -> Element of ( product <*G1, G2, G3*>) ;

      coherence

      proof

        set xy = <*x, y, z*>, G = <*G1, G2, G3*>;

        

         A1: ( dom ( Carrier G)) = {1, 2, 3} by PARTFUN1:def 2;

        

         A2: (xy . 2) = y by FINSEQ_1: 45;

        

         A3: (G . 1) = G1 by FINSEQ_1: 45;

        

         A4: (xy . 3) = z by FINSEQ_1: 45;

        

         A5: (G . 3) = G3 by FINSEQ_1: 45;

        

         A6: (G . 2) = G2 by FINSEQ_1: 45;

        

         A7: (xy . 1) = x by FINSEQ_1: 45;

        

         A8: for a be object st a in {1, 2, 3} holds (xy . a) in (( Carrier G) . a)

        proof

          let a be object;

          assume

           A9: a in {1, 2, 3};

          per cases by A9, ENUMSET1:def 1;

            suppose

             A10: a = 1;

            then ex R be 1-sorted st R = (G . 1) & (( Carrier G) . 1) = the carrier of R by A9, PRALG_1:def 15;

            hence thesis by A7, A3, A10;

          end;

            suppose

             A11: a = 2;

            then ex R be 1-sorted st R = (G . 2) & (( Carrier G) . 2) = the carrier of R by A9, PRALG_1:def 15;

            hence thesis by A2, A6, A11;

          end;

            suppose

             A12: a = 3;

            then ex R be 1-sorted st R = (G . 3) & (( Carrier G) . 3) = the carrier of R by A9, PRALG_1:def 15;

            hence thesis by A4, A5, A12;

          end;

        end;

        ( dom xy) = {1, 2, 3} by FINSEQ_1: 89, FINSEQ_3: 1;

        then xy in ( product ( Carrier G)) by A1, A8, CARD_3: 9;

        hence thesis by Def2;

      end;

    end

    reserve G1,G2,G3 for non empty multMagma,

x1,x2 for Element of G1,

y1,y2 for Element of G2,

z1,z2 for Element of G3;

    theorem :: GROUP_7:28

    

     Th28: ( <*x1*> * <*x2*>) = <*(x1 * x2)*>

    proof

      set G = <*G1*>;

      

       A1: (G . 1) = G1 by FINSEQ_1:def 8;

      reconsider l = <*x1*>, p = <*x2*>, lpl = ( <*x1*> * <*x2*>), lpp = <*(x1 * x2)*> as Element of ( product ( Carrier G)) by Def2;

      

       A2: (l . 1) = x1 by FINSEQ_1:def 8;

      

       A3: (p . 1) = x2 by FINSEQ_1:def 8;

      

       A4: (lpp . 1) = (x1 * x2) by FINSEQ_1:def 8;

      

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

      

       A6: for k be Nat st 1 <= k & k <= 1 holds (lpl . k) = (lpp . k)

      proof

        let k be Nat;

        assume that

         A7: 1 <= k and

         A8: k <= 1;

        k in ( Seg 1) by A7, A8;

        then k = 1 by FINSEQ_1: 2, TARSKI:def 1;

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

      end;

      ( dom lpl) = ( dom ( Carrier G)) by CARD_3: 9

      .= ( Seg 1) by FINSEQ_1: 2, PARTFUN1:def 2;

      then

       A9: ( len lpl) = 1 by FINSEQ_1:def 3;

      ( len lpp) = 1 by FINSEQ_1: 39;

      hence thesis by A9, A6;

    end;

    theorem :: GROUP_7:29

    ( <*x1, y1*> * <*x2, y2*>) = <*(x1 * x2), (y1 * y2)*>

    proof

      set G = <*G1, G2*>;

      

       A1: (G . 1) = G1 by FINSEQ_1: 44;

      

       A2: (G . 2) = G2 by FINSEQ_1: 44;

      reconsider l = <*x1, y1*>, p = <*x2, y2*>, lpl = ( <*x1, y1*> * <*x2, y2*>), lpp = <*(x1 * x2), (y1 * y2)*> as Element of ( product ( Carrier G)) by Def2;

      

       A3: 2 in {1, 2} by TARSKI:def 2;

      

       A4: (l . 1) = x1 by FINSEQ_1: 44;

      

       A5: (lpp . 1) = (x1 * x2) by FINSEQ_1: 44;

      

       A6: (p . 2) = y2 by FINSEQ_1: 44;

      

       A7: (lpp . 2) = (y1 * y2) by FINSEQ_1: 44;

      

       A8: (p . 1) = x2 by FINSEQ_1: 44;

      

       A9: (l . 2) = y1 by FINSEQ_1: 44;

      

       A10: 1 in {1, 2} by TARSKI:def 2;

      

       A11: for k be Nat st 1 <= k & k <= 2 holds (lpl . k) = (lpp . k)

      proof

        let k be Nat;

        assume that

         A12: 1 <= k and

         A13: k <= 2;

        

         A14: k in ( Seg 2) by A12, A13;

        per cases by A14, FINSEQ_1: 2, TARSKI:def 2;

          suppose k = 1;

          hence thesis by A10, A4, A8, A1, A5, Th1;

        end;

          suppose k = 2;

          hence thesis by A3, A9, A6, A2, A7, Th1;

        end;

      end;

      ( dom lpl) = ( dom ( Carrier G)) by CARD_3: 9

      .= ( Seg 2) by FINSEQ_1: 2, PARTFUN1:def 2;

      then

       A15: ( len lpl) = 2 by FINSEQ_1:def 3;

      ( len lpp) = 2 by FINSEQ_1: 44;

      hence thesis by A15, A11;

    end;

    theorem :: GROUP_7:30

    ( <*x1, y1, z1*> * <*x2, y2, z2*>) = <*(x1 * x2), (y1 * y2), (z1 * z2)*>

    proof

      set G = <*G1, G2, G3*>;

      

       A1: 3 in {1, 2, 3} by ENUMSET1:def 1;

      

       A2: (G . 1) = G1 by FINSEQ_1: 45;

      

       A3: (G . 3) = G3 by FINSEQ_1: 45;

      

       A4: (G . 2) = G2 by FINSEQ_1: 45;

      reconsider l = <*x1, y1, z1*>, p = <*x2, y2, z2*>, lpl = ( <*x1, y1, z1*> * <*x2, y2, z2*>), lpp = <*(x1 * x2), (y1 * y2), (z1 * z2)*> as Element of ( product ( Carrier G)) by Def2;

      

       A5: 2 in {1, 2, 3} by ENUMSET1:def 1;

      

       A6: (l . 1) = x1 by FINSEQ_1: 45;

      

       A7: (l . 3) = z1 by FINSEQ_1: 45;

      

       A8: (l . 2) = y1 by FINSEQ_1: 45;

      

       A9: (lpp . 3) = (z1 * z2) by FINSEQ_1: 45;

      

       A10: (lpp . 2) = (y1 * y2) by FINSEQ_1: 45;

      

       A11: (lpp . 1) = (x1 * x2) by FINSEQ_1: 45;

      

       A12: (p . 3) = z2 by FINSEQ_1: 45;

      

       A13: (p . 2) = y2 by FINSEQ_1: 45;

      

       A14: (p . 1) = x2 by FINSEQ_1: 45;

      

       A15: 1 in {1, 2, 3} by ENUMSET1:def 1;

      

       A16: for k be Nat st 1 <= k & k <= 3 holds (lpl . k) = (lpp . k)

      proof

        let k be Nat;

        assume that

         A17: 1 <= k and

         A18: k <= 3;

        

         A19: k in ( Seg 3) by A17, A18;

        per cases by A19, ENUMSET1:def 1, FINSEQ_3: 1;

          suppose k = 1;

          hence thesis by A15, A6, A14, A2, A11, Th1;

        end;

          suppose k = 2;

          hence thesis by A5, A8, A13, A4, A10, Th1;

        end;

          suppose k = 3;

          hence thesis by A1, A7, A12, A3, A9, Th1;

        end;

      end;

      ( dom lpl) = ( dom ( Carrier G)) by CARD_3: 9

      .= ( Seg 3) by FINSEQ_3: 1, PARTFUN1:def 2;

      then

       A20: ( len lpl) = 3 by FINSEQ_1:def 3;

      ( len lpp) = 3 by FINSEQ_1: 45;

      hence thesis by A20, A16;

    end;

    reserve G1,G2,G3 for Group-like non empty multMagma;

    theorem :: GROUP_7:31

    ( 1_ ( product <*G1*>)) = <*( 1_ G1)*>

    proof

      set s = <*( 1_ G1)*>, f = <*G1*>;

      ( dom s) = {1} by FINSEQ_1: 2, FINSEQ_1:def 8;

      then

      reconsider s as ManySortedSet of {1} by PARTFUN1:def 2, RELAT_1:def 18;

      for i be set st i in {1} holds ex G be Group-like non empty multMagma st G = (f . i) & (s . i) = ( 1_ G)

      proof

        let i be set;

        assume i in {1};

        then

         A1: i = 1 by TARSKI:def 1;

        then

        reconsider G = (f . i) as Group-like non empty multMagma by FINSEQ_1:def 8;

        take G;

        (f . i) = G1 by A1, FINSEQ_1:def 8;

        hence thesis by A1, FINSEQ_1:def 8;

      end;

      hence thesis by Th5;

    end;

    theorem :: GROUP_7:32

    ( 1_ ( product <*G1, G2*>)) = <*( 1_ G1), ( 1_ G2)*>

    proof

      set s = <*( 1_ G1), ( 1_ G2)*>, f = <*G1, G2*>;

      ( dom s) = {1, 2} by FINSEQ_1: 2, FINSEQ_1: 89;

      then

      reconsider s as ManySortedSet of {1, 2} by PARTFUN1:def 2, RELAT_1:def 18;

      for i be set st i in {1, 2} holds ex G be Group-like non empty multMagma st G = (f . i) & (s . i) = ( 1_ G)

      proof

        let i be set such that

         A1: i in {1, 2};

        per cases by A1, TARSKI:def 2;

          suppose

           A2: i = 1;

          then

          reconsider G = (f . i) as Group-like non empty multMagma by FINSEQ_1: 44;

          take G;

          (f . i) = G1 by A2, FINSEQ_1: 44;

          hence thesis by A2, FINSEQ_1: 44;

        end;

          suppose

           A3: i = 2;

          then

          reconsider G = (f . i) as Group-like non empty multMagma by FINSEQ_1: 44;

          take G;

          (f . i) = G2 by A3, FINSEQ_1: 44;

          hence thesis by A3, FINSEQ_1: 44;

        end;

      end;

      hence thesis by Th5;

    end;

    theorem :: GROUP_7:33

    ( 1_ ( product <*G1, G2, G3*>)) = <*( 1_ G1), ( 1_ G2), ( 1_ G3)*>

    proof

      set s = <*( 1_ G1), ( 1_ G2), ( 1_ G3)*>, f = <*G1, G2, G3*>;

      ( dom s) = {1, 2, 3} by FINSEQ_1: 89, FINSEQ_3: 1;

      then

      reconsider s as ManySortedSet of {1, 2, 3} by PARTFUN1:def 2, RELAT_1:def 18;

      for i be set st i in {1, 2, 3} holds ex G be Group-like non empty multMagma st G = (f . i) & (s . i) = ( 1_ G)

      proof

        let i be set such that

         A1: i in {1, 2, 3};

        per cases by A1, ENUMSET1:def 1;

          suppose

           A2: i = 1;

          then

          reconsider G = (f . i) as Group-like non empty multMagma by FINSEQ_1: 45;

          take G;

          (f . i) = G1 by A2, FINSEQ_1: 45;

          hence thesis by A2, FINSEQ_1: 45;

        end;

          suppose

           A3: i = 2;

          then

          reconsider G = (f . i) as Group-like non empty multMagma by FINSEQ_1: 45;

          take G;

          (f . i) = G2 by A3, FINSEQ_1: 45;

          hence thesis by A3, FINSEQ_1: 45;

        end;

          suppose

           A4: i = 3;

          then

          reconsider G = (f . i) as Group-like non empty multMagma by FINSEQ_1: 45;

          take G;

          (f . i) = G3 by A4, FINSEQ_1: 45;

          hence thesis by A4, FINSEQ_1: 45;

        end;

      end;

      hence thesis by Th5;

    end;

    reserve G1,G2,G3 for Group,

x for Element of G1,

y for Element of G2,

z for Element of G3;

    theorem :: GROUP_7:34

    ( <*x*> qua Element of ( product <*G1*>) " ) = <*(x " )*>

    proof

      reconsider G = <*G1*> as associative Group-like multMagma-Family of {1};

      reconsider lF = <*x*>, p = <*(x " )*> as Element of ( product ( Carrier G)) by Def2;

      

       A1: (p . 1) = (x " ) by FINSEQ_1:def 8;

      

       A2: (G . 1) = G1 by FINSEQ_1:def 8;

      for i be set st i in {1} holds ex H be Group, z be Element of H st H = (G . i) & (p . i) = (z " ) & z = (lF . i)

      proof

        reconsider H = (G . 1) as Group by FINSEQ_1:def 8;

        reconsider z = (p . 1) as Element of H by A1, FINSEQ_1:def 8;

        let i be set;

        assume

         A3: i in {1};

        take H, (z " );

        thus H = (G . i) by A3, TARSKI:def 1;

        thus (p . i) = ((z " ) " ) by A3, TARSKI:def 1;

        i = 1 by A3, TARSKI:def 1;

        hence thesis by A1, A2, FINSEQ_1:def 8;

      end;

      hence thesis by Th7;

    end;

    theorem :: GROUP_7:35

    ( <*x, y*> qua Element of ( product <*G1, G2*>) " ) = <*(x " ), (y " )*>

    proof

      set G = <*G1, G2*>;

      

       A1: (G . 2) = G2 by FINSEQ_1: 44;

      reconsider lF = <*x, y*>, p = <*(x " ), (y " )*> as Element of ( product ( Carrier G)) by Def2;

      

       A2: (p . 1) = (x " ) by FINSEQ_1: 44;

      

       A3: (p . 2) = (y " ) by FINSEQ_1: 44;

      

       A4: (G . 1) = G1 by FINSEQ_1: 44;

      for i be set st i in {1, 2} holds ex H be Group, z be Element of H st H = (G . i) & (p . i) = (z " ) & z = (lF . i)

      proof

        let i be set such that

         A5: i in {1, 2};

        per cases by A5, TARSKI:def 2;

          suppose

           A6: i = 1;

          reconsider H = (G . 1) as Group by FINSEQ_1: 44;

          reconsider z = (p . 1) as Element of H by A2, FINSEQ_1: 44;

          take H, (z " );

          thus H = (G . i) by A6;

          thus (p . i) = ((z " ) " ) by A6;

          thus thesis by A2, A4, A6, FINSEQ_1: 44;

        end;

          suppose

           A7: i = 2;

          reconsider H = (G . 2) as Group by FINSEQ_1: 44;

          reconsider z = (p . 2) as Element of H by A3, FINSEQ_1: 44;

          take H, (z " );

          thus H = (G . i) by A7;

          thus (p . i) = ((z " ) " ) by A7;

          thus thesis by A3, A1, A7, FINSEQ_1: 44;

        end;

      end;

      hence thesis by Th7;

    end;

    theorem :: GROUP_7:36

    ( <*x, y, z*> qua Element of ( product <*G1, G2, G3*>) " ) = <*(x " ), (y " ), (z " )*>

    proof

      set G = <*G1, G2, G3*>;

      

       A1: (G . 2) = G2 by FINSEQ_1: 45;

      

       A2: (G . 3) = G3 by FINSEQ_1: 45;

      reconsider lF = <*x, y, z*>, p = <*(x " ), (y " ), (z " )*> as Element of ( product ( Carrier G)) by Def2;

      

       A3: (p . 1) = (x " ) by FINSEQ_1: 45;

      

       A4: (p . 3) = (z " ) by FINSEQ_1: 45;

      

       A5: (p . 2) = (y " ) by FINSEQ_1: 45;

      

       A6: (G . 1) = G1 by FINSEQ_1: 45;

      for i be set st i in {1, 2, 3} holds ex H be Group, z be Element of H st H = (G . i) & (p . i) = (z " ) & z = (lF . i)

      proof

        let i be set such that

         A7: i in {1, 2, 3};

        per cases by A7, ENUMSET1:def 1;

          suppose

           A8: i = 1;

          reconsider H = (G . 1) as Group by FINSEQ_1: 45;

          reconsider z = (p . 1) as Element of H by A3, FINSEQ_1: 45;

          take H, (z " );

          thus H = (G . i) by A8;

          thus (p . i) = ((z " ) " ) by A8;

          thus thesis by A3, A6, A8, FINSEQ_1: 45;

        end;

          suppose

           A9: i = 2;

          reconsider H = (G . 2) as Group by FINSEQ_1: 45;

          reconsider z = (p . 2) as Element of H by A5, FINSEQ_1: 45;

          take H, (z " );

          thus H = (G . i) by A9;

          thus (p . i) = ((z " ) " ) by A9;

          thus thesis by A5, A1, A9, FINSEQ_1: 45;

        end;

          suppose

           A10: i = 3;

          reconsider H = (G . 3) as Group by FINSEQ_1: 45;

          reconsider z = (p . 3) as Element of H by A4, FINSEQ_1: 45;

          take H, (z " );

          thus H = (G . i) by A10;

          thus (p . i) = ((z " ) " ) by A10;

          thus thesis by A4, A2, A10, FINSEQ_1: 45;

        end;

      end;

      hence thesis by Th7;

    end;

    theorem :: GROUP_7:37

    

     Th37: for f be Function of the carrier of G1, the carrier of ( product <*G1*>) st for x be Element of G1 holds (f . x) = <*x*> holds f is Homomorphism of G1, ( product <*G1*>)

    proof

      let f be Function of the carrier of G1, the carrier of ( product <*G1*>) such that

       A1: for x be Element of G1 holds (f . x) = <*x*>;

      now

        let a,b be Element of G1;

        

        thus (f . (a * b)) = <*(a * b)*> by A1

        .= ( <*a*> * <*b*>) by Th28

        .= ( <*a*> * (f . b)) by A1

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

      end;

      hence thesis by GROUP_6:def 6;

    end;

    theorem :: GROUP_7:38

    

     Th38: for f be Homomorphism of G1, ( product <*G1*>) st for x be Element of G1 holds (f . x) = <*x*> holds f is bijective

    proof

      let f be Homomorphism of G1, ( product <*G1*>) such that

       A1: for x be Element of G1 holds (f . x) = <*x*>;

      

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

      

       A3: ( rng f) = the carrier of ( product <*G1*>)

      proof

        thus ( rng f) c= the carrier of ( product <*G1*>);

        let x be object;

        assume x in the carrier of ( product <*G1*>);

        then

        reconsider a = x as Element of ( product <*G1*>);

        

         A4: 1 in {1} by TARSKI:def 1;

        then

         A5: ex R be 1-sorted st R = ( <*G1*> . 1) & (( Carrier <*G1*>) . 1) = the carrier of R by PRALG_1:def 15;

        a in the carrier of ( product <*G1*>);

        then

         A6: a in ( product ( Carrier <*G1*>)) by Def2;

        then

         A7: ( dom a) = ( dom ( Carrier <*G1*>)) by CARD_3: 9;

        then

         A8: ( dom a) = {1} by PARTFUN1:def 2;

        then (a . 1) in (( Carrier <*G1*>) . 1) by A6, A7, A4, CARD_3: 9;

        then

        reconsider b = (a . 1) as Element of G1 by A5, FINSEQ_1:def 8;

        (f . b) = <*b*> by A1

        .= x by A8, FINSEQ_1: 2, FINSEQ_1:def 8;

        hence thesis by A2, FUNCT_1:def 3;

      end;

      f is one-to-one

      proof

        let m,n be object;

        assume that

         A9: m in ( dom f) and

         A10: n in ( dom f) and

         A11: (f . m) = (f . n);

        reconsider m1 = m, n1 = n as Element of G1 by A9, A10;

         <*m1*> = (f . m1) by A1

        .= <*n1*> by A1, A11;

        hence thesis by FINSEQ_1: 76;

      end;

      hence thesis by A3, GROUP_6: 60;

    end;

    theorem :: GROUP_7:39

    (G1,( product <*G1*>)) are_isomorphic

    proof

      deffunc F( Element of G1) = <*$1*>;

      consider f be Function of the carrier of G1, the carrier of ( product <*G1*>) such that

       A1: for x be Element of G1 holds (f . x) = F(x) from FUNCT_2:sch 4;

      reconsider f as Homomorphism of G1, ( product <*G1*>) by A1, Th37;

      take f;

      thus thesis by A1, Th38;

    end;