group_12.miz



    begin

    registration

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

      let i be Element of I;

      cluster (F . i) -> Group-like;

      coherence by GROUP_7:def 6;

    end

    registration

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

      let i be Element of I;

      cluster (F . i) -> associative;

      coherence by GROUP_7:def 7;

    end

    registration

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

      let i be Element of I;

      cluster (F . i) -> commutative;

      coherence by GROUP_7:def 8;

    end

    reserve I for non empty set,

F for associative Group-like multMagma-Family of I,

i,j for Element of I;

    theorem :: GROUP_12:1

    

     Th1: for x be Function, g be Element of (F . i) holds (( dom x) = I & (x . i) = g & for j be Element of I st j <> i holds (x . j) = ( 1_ (F . j))) iff x = (( 1_ ( product F)) +* (i,g))

    proof

      let x be Function, g be Element of (F . i);

       A1:

      now

        assume

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

        

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

        

        thus

         A4: ( dom x) = ( dom ( 1_ ( product F))) by A2, FUNCT_7: 30

        .= I by A3, PARTFUN1:def 2;

        ( dom x) = ( dom ( 1_ ( product F))) by A2, FUNCT_7: 30;

        hence (x . i) = g by A2, A4, FUNCT_7: 31;

        thus for j be Element of I st j <> i holds (x . j) = ( 1_ (F . j))

        proof

          let j be Element of I;

          assume j <> i;

          then (x . j) = (( 1_ ( product F)) . j) by A2, FUNCT_7: 32;

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

        end;

      end;

      now

        assume

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

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

        then

         A6: ( dom ( 1_ ( product F))) = I by PARTFUN1:def 2;

        

         A7: ( dom (( 1_ ( product F)) +* (i,g))) = ( dom x) by A5, A6, FUNCT_7: 30;

        set FG = (( 1_ ( product F)) +* (i,g));

        now

          let j0 be object;

          assume j0 in ( dom x);

          then

          reconsider j = j0 as Element of I by A5;

          per cases ;

            suppose

             A8: j <> i;

            then (x . j) = ( 1_ (F . j)) by A5;

            

            hence (x . j0) = (( 1_ ( product F)) . j) by GROUP_7: 6

            .= (FG . j0) by A8, FUNCT_7: 32;

          end;

            suppose j = i;

            hence (x . j0) = (FG . j0) by A6, A5, FUNCT_7: 31;

          end;

        end;

        hence x = (( 1_ ( product F)) +* (i,g)) by A7, FUNCT_1: 2;

      end;

      hence thesis by A1;

    end;

    definition

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

      :: GROUP_12:def1

      func ProjSet (F,i) -> Subset of ( product F) means

      : Def1: for x be set holds x in it iff ex g be Element of (F . i) st x = (( 1_ ( product F)) +* (i,g));

      existence

      proof

        set CF = the carrier of ( product F);

        defpred P[ set] means ex g be Element of (F . i) st $1 = (( 1_ ( product F)) +* (i,g));

        consider H be Subset of CF such that

         A1: for x be set holds x in H iff x in CF & P[x] from SUBSET_1:sch 1;

        take H;

        set Gi = (F . i);

         A2:

        now

          let x be set;

          assume

           A3: P[x];

          

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

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

          hence x in CF by A3, A4, YELLOW17: 2;

        end;

        let x be set;

        x in H iff x in CF & P[x] by A1;

        hence thesis by A2;

      end;

      uniqueness

      proof

        let F1,F2 be Subset of ( product F);

        defpred P[ set] means ex g be Element of (F . i) st $1 = (( 1_ ( product F)) +* (i,g));

        assume

         A5: for x be set holds x in F1 iff P[x];

        assume

         A6: for x be set holds x in F2 iff P[x];

        thus thesis from XFAMILY:sch 2( A5, A6);

      end;

    end

    registration

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

      cluster ( ProjSet (F,i)) -> non empty;

      coherence

      proof

        set Gi = (F . i);

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

        then

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

        

         A2: ( dom (( 1_ ( product F)) +* (i,( 1_ Gi)))) = ( dom ( 1_ ( product F))) by FUNCT_7: 30;

        set FG = (( 1_ ( product F)) +* (i,( 1_ Gi)));

        reconsider FG as I -defined Function by A2, A1, RELAT_1:def 18;

        now

          let j be Element of I;

          per cases ;

            suppose

             A3: j <> i;

            

            thus (FG . j) = (( 1_ ( product F)) . j) by A3, FUNCT_7: 32

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

          end;

            suppose j = i;

            hence (FG . j) = ( 1_ (F . j)) by A1, FUNCT_7: 31;

          end;

        end;

        hence thesis by Def1;

      end;

    end

    theorem :: GROUP_12:2

    

     Th2: for x0 be set holds x0 in ( ProjSet (F,i)) iff ex x be Function, g be Element of (F . i) st x = x0 & ( dom x) = I & (x . i) = g & for j be Element of I st j <> i holds (x . j) = ( 1_ (F . j))

    proof

      let x0 be set;

      defpred P[ set] means ex g be Element of (F . i) st $1 = (( 1_ ( product F)) +* (i,g));

       A1:

      now

        assume x0 in ( ProjSet (F,i));

        then

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

         A2: x0 = (( 1_ ( product F)) +* (i,g)) by Def1;

        reconsider x = x0 as Function by A2;

        take x, g;

        thus x = x0;

        thus ( dom x) = I & (x . i) = g & for j be Element of I st j <> i holds (x . j) = ( 1_ (F . j)) by A2, Th1;

      end;

      now

        assume

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

        thus x0 in ( ProjSet (F,i))

        proof

          consider x be Function, g be Element of (F . i) such that

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

          x = (( 1_ ( product F)) +* (i,g)) by Th1, A4;

          hence x0 in ( ProjSet (F,i)) by Def1, A4;

        end;

      end;

      hence thesis by A1;

    end;

    theorem :: GROUP_12:3

    

     Th3: for g1,g2 be Element of ( product F), z1,z2 be Element of (F . i) st g1 = (( 1_ ( product F)) +* (i,z1)) & g2 = (( 1_ ( product F)) +* (i,z2)) holds (g1 * g2) = (( 1_ ( product F)) +* (i,(z1 * z2)))

    proof

      let g1,g2 be Element of ( product F), z1,z2 be Element of (F . i);

      assume

       A1: g1 = (( 1_ ( product F)) +* (i,z1)) & g2 = (( 1_ ( product F)) +* (i,z2));

      set x1 = g1, x2 = g2;

      

       A2: x1 = g1 & ( dom x1) = I & (x1 . i) = z1 & for j be Element of I st j <> i holds (x1 . j) = ( 1_ (F . j)) by Th1, A1;

      

       A3: x2 = g2 & ( dom x2) = I & (x2 . i) = z2 & for j be Element of I st j <> i holds (x2 . j) = ( 1_ (F . j)) by Th1, A1;

      set x12 = (g1 * g2);

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

      then

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

      

       A5: (x12 . i) = (z1 * z2) by A2, A3, GROUP_7: 1;

      for j be Element of I st i <> j holds (x12 . j) = ( 1_ (F . j))

      proof

        let j be Element of I;

        assume

         A6: i <> j;

        then

         A7: (x1 . j) = ( 1_ (F . j)) by Th1, A1;

        (x2 . j) = ( 1_ (F . j)) by A6, Th1, A1;

        

        hence (x12 . j) = (( 1_ (F . j)) * ( 1_ (F . j))) by A7, GROUP_7: 1

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

      end;

      hence thesis by A4, A5, Th1;

    end;

    theorem :: GROUP_12:4

    

     Th4: for g1 be Element of ( product F), z1 be Element of (F . i) st g1 = (( 1_ ( product F)) +* (i,z1)) holds (g1 " ) = (( 1_ ( product F)) +* (i,(z1 " )))

    proof

      let g1 be Element of ( product F), z1 be Element of (F . i);

      assume

       A1: g1 = (( 1_ ( product F)) +* (i,z1));

      set x1 = g1;

      

       A2: x1 = g1 & ( dom x1) = I & (x1 . i) = z1 & for j be Element of I st j <> i holds (x1 . j) = ( 1_ (F . j)) by Th1, A1;

      set x12 = (g1 " );

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

      then

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

      

       A4: (x12 . i) = (z1 " ) by A2, GROUP_7: 8;

      

       A5: for j be Element of I st i <> j holds (x12 . j) = ( 1_ (F . j))

      proof

        let j be Element of I;

        assume i <> j;

        then (x1 . j) = ( 1_ (F . j)) by Th1, A1;

        

        hence (x12 . j) = (( 1_ (F . j)) " ) by GROUP_7: 8

        .= ( 1_ (F . j)) by GROUP_1: 8;

      end;

      thus thesis by A3, A4, A5, Th1;

    end;

    theorem :: GROUP_12:5

    

     Th5: for g1,g2 be Element of ( product F) st g1 in ( ProjSet (F,i)) & g2 in ( ProjSet (F,i)) holds (g1 * g2) in ( ProjSet (F,i))

    proof

      let g1,g2 be Element of ( product F);

      assume

       A1: g1 in ( ProjSet (F,i)) & g2 in ( ProjSet (F,i));

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

       A2: g1 = (( 1_ ( product F)) +* (i,z1)) by Def1, A1;

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

       A3: g2 = (( 1_ ( product F)) +* (i,z2)) by Def1, A1;

      (g1 * g2) = (( 1_ ( product F)) +* (i,(z1 * z2))) by Th3, A2, A3;

      hence (g1 * g2) in ( ProjSet (F,i)) by Def1;

    end;

    theorem :: GROUP_12:6

    

     Th6: for g be Element of ( product F) st g in ( ProjSet (F,i)) holds (g " ) in ( ProjSet (F,i))

    proof

      let g be Element of ( product F);

      assume

       A1: g in ( ProjSet (F,i));

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

       A2: g = (( 1_ ( product F)) +* (i,z)) by Def1, A1;

      (g " ) = (( 1_ ( product F)) +* (i,(z " ))) by Th4, A2;

      hence (g " ) in ( ProjSet (F,i)) by Def1;

    end;

    definition

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

      :: GROUP_12:def2

      func ProjGroup (F,i) -> strict Subgroup of ( product F) means

      : Def2: the carrier of it = ( ProjSet (F,i));

      existence

      proof

        (for g1,g2 be Element of ( product F) st g1 in ( ProjSet (F,i)) & g2 in ( ProjSet (F,i)) holds (g1 * g2) in ( ProjSet (F,i))) & (for g be Element of ( product F) st g in ( ProjSet (F,i)) holds (g " ) in ( ProjSet (F,i))) by Th5, Th6;

        hence thesis by GROUP_2: 52;

      end;

      uniqueness by GROUP_2: 59;

    end

    

     Lm1: ex f be Homomorphism of (F . i), ( ProjGroup (F,i)) st f is bijective & for x be Element of (F . i) holds (f . x) = (( 1_ ( product F)) +* (i,x))

    proof

      

       A1: the carrier of ( ProjGroup (F,i)) = ( ProjSet (F,i)) by Def2;

      defpred P[ set, set] means $2 = (( 1_ ( product F)) +* (i,$1));

      

       A2: for x be Element of (F . i) holds ex y be Element of ( ProjGroup (F,i)) st P[x, y]

      proof

        let x be Element of (F . i);

        (( 1_ ( product F)) +* (i,x)) in ( ProjSet (F,i)) by Def1;

        hence thesis by A1;

      end;

      consider f be Function of (F . i), the carrier of ( ProjGroup (F,i)) such that

       A3: for x be Element of the carrier of (F . i) holds P[x, (f . x)] from FUNCT_2:sch 3( A2);

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

      proof

        let a,b be Element of (F . i);

        

         A4: (f . a) = (( 1_ ( product F)) +* (i,a)) by A3;

        

         A5: (f . b) = (( 1_ ( product F)) +* (i,b)) by A3;

        

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

        the carrier of ( ProjGroup (F,i)) = ( ProjSet (F,i)) by Def2;

        then

        reconsider ffa = (f . a), ffb = (f . b) as Element of ( product F) by TARSKI:def 3;

        

        thus ((f . a) * (f . b)) = (ffa * ffb) by GROUP_2: 43

        .= (f . (a * b)) by A6, A4, A5, Th3;

      end;

      then

      reconsider f as Homomorphism of (F . i), ( ProjGroup (F,i)) by GROUP_6:def 6;

      take f;

      now

        let x be object;

        assume x in the carrier of ( ProjGroup (F,i));

        then

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

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

        x = (f . g) by A7, A3;

        hence x in ( rng f) by FUNCT_2: 4;

      end;

      then

       A8: the carrier of ( ProjGroup (F,i)) c= ( rng f) by TARSKI:def 3;

      ( rng f) = the carrier of ( ProjGroup (F,i)) by A8, XBOOLE_0:def 10;

      then

       A9: f is onto by FUNCT_2:def 3;

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

      proof

        let x1,x2 be object;

        assume

         A10: x1 in the carrier of (F . i) & x2 in the carrier of (F . i) & (f . x1) = (f . x2);

        then

        reconsider xx1 = x1, xx2 = x2 as Element of the carrier of (F . i);

        

         A11: (f . xx1) = (( 1_ ( product F)) +* (i,xx1)) by A3;

        

         A12: (( 1_ ( product F)) +* (i,xx1)) = (( 1_ ( product F)) +* (i,xx2)) by A10, A11, A3;

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

        then

         A13: ( dom ( 1_ ( product F))) = I by PARTFUN1:def 2;

        

        thus x1 = ((( 1_ ( product F)) +* (i .--> xx1)) . i) by FUNCT_7: 94

        .= ((( 1_ ( product F)) +* (i,xx1)) . i) by A13, FUNCT_7:def 3

        .= ((( 1_ ( product F)) +* (i .--> xx2)) . i) by A13, A12, FUNCT_7:def 3

        .= x2 by FUNCT_7: 94;

      end;

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

      hence f is bijective by A9;

      thus thesis by A3;

    end;

    definition

      let I, F, i;

      :: GROUP_12:def3

      func 1ProdHom (F,i) -> Homomorphism of (F . i), ( ProjGroup (F,i)) means

      : Def3: for x be Element of (F . i) holds (it . x) = (( 1_ ( product F)) +* (i,x));

      existence

      proof

        ex f be Homomorphism of (F . i), ( ProjGroup (F,i)) st f is bijective & for x be Element of (F . i) holds (f . x) = (( 1_ ( product F)) +* (i,x)) by Lm1;

        hence thesis;

      end;

      uniqueness

      proof

        let F1,F2 be Homomorphism of (F . i), ( ProjGroup (F,i)) such that

         A1: for x be Element of (F . i) holds (F1 . x) = (( 1_ ( product F)) +* (i,x)) and

         A2: for x be Element of (F . i) holds (F2 . x) = (( 1_ ( product F)) +* (i,x));

        now

          let x be Element of (F . i);

          

          thus (F1 . x) = (( 1_ ( product F)) +* (i,x)) by A1

          .= (F2 . x) by A2;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    registration

      let I, F, i;

      cluster ( 1ProdHom (F,i)) -> bijective;

      coherence

      proof

        consider f be Homomorphism of (F . i), ( ProjGroup (F,i)) such that

         A1: f is bijective & for x be Element of (F . i) holds (f . x) = (( 1_ ( product F)) +* (i,x)) by Lm1;

        set F2 = ( 1ProdHom (F,i));

        for x be Element of (F . i) holds (f . x) = (F2 . x) by Def3, A1;

        hence thesis by A1, FUNCT_2: 63;

      end;

    end

    registration

      let I, F, i;

      cluster ( ProjGroup (F,i)) -> normal;

      correctness

      proof

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

        set G = ( product F);

        

         A1: for a be Element of G holds ((a * H) * (a " )) c= the carrier of H

        proof

          let a be Element of G;

          now

            let x be object;

            assume x in ((a * H) * (a " ));

            then

            consider h be Element of G such that

             A2: x = (h * (a " )) & h in (a * H) by GROUP_2: 28;

            consider k be Element of G such that

             A3: h = (a * k) & k in H by A2, GROUP_2: 103;

            k in the carrier of H by A3, STRUCT_0:def 5;

            then k in ( ProjSet (F,i)) by Def2;

            then

            consider m be Function, g be Element of (F . i) such that

             A4: m = k & ( dom m) = I & (m . i) = g & for j be Element of I st j <> i holds (m . j) = ( 1_ (F . j)) by Th2;

            set n = ((a * k) * (a " ));

            

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

            

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

            

             A7: ( dom n) = I by A5, PARTFUN1:def 2;

            set Gi = (F . i);

            consider Ri be 1-sorted such that

             A8: Ri = (F . i) & (( Carrier F) . i) = the carrier of Ri by PRALG_1:def 15;

            set ak = (a * k), ad = (a " );

            reconsider xa = (a . i), xk = (k . i) as Element of Gi by A8, A5, A6, CARD_3: 9;

            

             A9: (ak . i) = (xa * xk) by GROUP_7: 1;

            

             A10: (ad . i) = (xa " ) by GROUP_7: 8;

            

             A11: (n . i) = ((xa * xk) * (xa " )) by A9, A10, GROUP_7: 1;

            now

              let j be Element of I;

              assume j <> i;

              then

               A12: (m . j) = ( 1_ (F . j)) by A4;

              set Gj = (F . j);

              consider Rj be 1-sorted such that

               A13: Rj = (F . j) & (( Carrier F) . j) = the carrier of Rj by PRALG_1:def 15;

              reconsider xa = (a . j), xk = (k . j) as Element of Gj by A13, A5, A6, CARD_3: 9;

              

               A14: (ak . j) = (xa * xk) by GROUP_7: 1;

              

               A15: (ad . j) = (xa " ) by GROUP_7: 8;

              

              thus (n . j) = ((xa * xk) * (xa " )) by A14, A15, GROUP_7: 1

              .= (xa * (xa " )) by A12, A4, GROUP_1:def 4

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

            end;

            then n in ( ProjSet (F,i)) by A7, A11, Th2;

            hence x in the carrier of H by Def2, A2, A3;

          end;

          hence ((a * H) * (a " )) c= the carrier of H by TARSKI:def 3;

        end;

        

         A16: for a be Element of G holds (a * H) c= (H * a)

        proof

          let a be Element of G;

          

           A17: ((a * H) * (a " )) c= the carrier of H by A1;

          

           A18: ((a " ) * a) = ( 1_ ( product F)) by GROUP_1:def 5;

          (((a * H) * (a " )) * a) = ((a * (H * (a " ))) * a) by GROUP_2: 106

          .= (a * ((H * (a " )) * a)) by GROUP_2: 33

          .= (a * (H * ((a " ) * a))) by GROUP_2: 107

          .= (a * H) by A18, GROUP_2: 109;

          hence thesis by A17, GROUP_3: 5;

        end;

        

         A19: for a be Element of G holds (H * a) c= (a * H)

        proof

          let a be Element of G;

          

           A20: (((a " ) * H) * ((a " ) " )) c= the carrier of H by A1;

          

           A21: (a * (a " )) = ( 1_ ( product F)) by GROUP_1:def 5;

          (a * (((a " ) * H) * a)) = (a * ((a " ) * (H * a))) by GROUP_2: 106

          .= ((a * (a " )) * (H * a)) by GROUP_2: 32

          .= (((a * (a " )) * H) * a) by GROUP_2: 106

          .= (H * a) by A21, GROUP_2: 109;

          hence thesis by A20, GROUP_3: 5;

        end;

        for a be Element of G holds (a * H) = (H * a)

        proof

          let a be Element of G;

          

           A22: (a * H) c= (H * a) by A16;

          (H * a) c= (a * H) by A19;

          hence thesis by A22, XBOOLE_0:def 10;

        end;

        hence thesis by GROUP_3: 117;

      end;

    end

    theorem :: GROUP_12:7

    for x,y be Element of ( product F) st i <> j & x in ( ProjGroup (F,i)) & y in ( ProjGroup (F,j)) holds (x * y) = (y * x)

    proof

      set G = ( product F);

      let x,y be Element of G;

      assume

       A1: i <> j & x in ( ProjGroup (F,i)) & y in ( ProjGroup (F,j));

      

       A2: the carrier of ( ProjGroup (F,i)) = ( ProjSet (F,i)) & the carrier of ( ProjGroup (F,j)) = ( ProjSet (F,j)) by Def2;

      

       A3: x in ( ProjSet (F,i)) & y in ( ProjSet (F,j)) by A2, A1, STRUCT_0:def 5;

      consider xx be Function, gx be Element of (F . i) such that

       A4: xx = x & ( dom xx) = I & (xx . i) = gx & for k be Element of I st k <> i holds (xx . k) = ( 1_ (F . k)) by A3, Th2;

      consider yy be Function, gy be Element of (F . j) such that

       A5: yy = y & ( dom yy) = I & (yy . j) = gy & for k be Element of I st k <> j holds (yy . k) = ( 1_ (F . k)) by A3, Th2;

      

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

      set xy = (x * y);

      set yx = (y * x);

      

       A7: ( dom xy) = I by A6, PARTFUN1:def 2;

      

       A8: ( dom yx) = I by A6, PARTFUN1:def 2;

      for k be object st k in ( dom xy) holds (xy . k) = (yx . k)

      proof

        let k0 be object;

        assume k0 in ( dom xy);

        then

        reconsider k = k0 as Element of I by A6, PARTFUN1:def 2;

        per cases ;

          suppose

           A9: k0 <> i & k0 <> j;

          then

           A10: (xx . k) = ( 1_ (F . k)) by A4;

          

           A11: (yy . k) = ( 1_ (F . k)) by A9, A5;

          (xy . k) = (( 1_ (F . k)) * ( 1_ (F . k))) by A4, A5, A10, A11, GROUP_7: 1

          .= (yx . k) by A4, A5, A10, A11, GROUP_7: 1;

          hence (xy . k0) = (yx . k0);

        end;

          suppose

           A12: k0 = i or k0 = j;

          per cases by A12;

            suppose

             A13: k0 = i;

            then

             A14: (yy . k) = ( 1_ (F . k)) by A1, A5;

            reconsider gx as Element of (F . k) by A13;

            (xy . k) = (gx * ( 1_ (F . k))) by A4, A5, A14, A13, GROUP_7: 1

            .= gx by GROUP_1:def 4

            .= (( 1_ (F . k)) * gx) by GROUP_1:def 4

            .= (yx . k) by A4, A5, A14, A13, GROUP_7: 1;

            hence (xy . k0) = (yx . k0);

          end;

            suppose

             A15: k0 = j;

            then

             A16: (xx . k) = ( 1_ (F . k)) by A1, A4;

            reconsider gy as Element of (F . k) by A15;

            (xy . k) = (( 1_ (F . k)) * gy) by A4, A5, A16, A15, GROUP_7: 1

            .= gy by GROUP_1:def 4

            .= (gy * ( 1_ (F . k))) by GROUP_1:def 4

            .= (yx . k) by A4, A5, A16, A15, GROUP_7: 1;

            hence (xy . k0) = (yx . k0);

          end;

        end;

      end;

      hence thesis by A7, A8, FUNCT_1: 2;

    end;

    reserve n for non zero Nat;

    theorem :: GROUP_12:8

    

     Th8: for F be associative Group-like multMagma-Family of ( Seg n), J be Nat, GJ be Group st 1 <= J & J <= n & GJ = (F . J) holds for x be Element of ( product F), s be FinSequence of ( product F) st ( len s) < J & (for k be Element of ( Seg n) st k in ( dom s) holds (s . k) in ( ProjGroup (F,k))) & x = ( Product s) holds (x . J) = ( 1_ GJ)

    proof

      let F be associative Group-like multMagma-Family of ( Seg n), J be Nat, GJ be Group;

      assume

       A1: 1 <= J & J <= n & GJ = (F . J);

      defpred P[ Nat] means for x be Element of ( product F), s be FinSequence of ( product F) st ( len s) < J & ( len s) = $1 & (for k be Element of ( Seg n) st k in ( dom s) holds (s . k) in ( ProjGroup (F,k))) & x = ( Product s) holds (x . J) = ( 1_ GJ);

      

       A2: P[ 0 ]

      proof

        let x be Element of ( product F), s be FinSequence of ( product F);

        assume

         A3: ( len s) < J & ( len s) = 0 & (for k be Element of ( Seg n) st k in ( dom s) holds (s . k) in ( ProjGroup (F,k))) & x = ( Product s);

        s = ( <*> the carrier of ( product F)) by A3;

        then

         A4: x = ( 1_ ( product F)) by A3, GROUP_4: 8;

        J in ( Seg n) by A1;

        hence (x . J) = ( 1_ GJ) by A1, A4, GROUP_7: 6;

      end;

      

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

      proof

        let m be Nat;

        assume

         A6: P[m];

        let x be Element of ( product F), s be FinSequence of ( product F);

        assume

         A7: ( len s) < J & ( len s) = (m + 1) & (for k be Element of ( Seg n) st k in ( dom s) holds (s . k) in ( ProjGroup (F,k))) & x = ( Product s);

        

         A8: m < (m + 1) by NAT_1: 13;

        

         A9: 1 <= ( len s) by A7, NAT_1: 11;

        1 <= ( len s) & ( len s) <= n by A7, A1, NAT_1: 11, XXREAL_0: 2;

        then ( len s) in ( Seg n);

        then

        reconsider ls = ( len s) as Element of ( Seg n);

        set t = (s | m);

         A10:

        now

          let k be Element of ( Seg n);

          assume

           A11: k in ( dom t);

          

           A12: (t . k) = (s . k) by A11, FUNCT_1: 47;

          k in ( dom s) by A11, RELAT_1: 57;

          hence (t . k) in ( ProjGroup (F,k)) by A12, A7;

        end;

        set y = ( Product t);

        

         A13: m in NAT by ORDINAL1:def 12;

        ( dom s) = ( Seg (m + 1)) by A7, FINSEQ_1:def 3;

        then ( Seg m) c= ( dom s) by A8, FINSEQ_1: 5;

        then

         A14: ( dom t) = ( Seg m) by RELAT_1: 62;

        then

         A15: ( len t) = m by FINSEQ_1:def 3, A13;

        

         A16: ( len t) = (( len s) - 1) by A14, A7, FINSEQ_1:def 3, A13;

        

         A17: (y . J) = ( 1_ GJ) by A6, A10, A16, A7, XREAL_1: 51;

        ( len s) in ( Seg ( len s)) by A9;

        then

         A18: ( len s) in ( dom s) by FINSEQ_1:def 3;

        then

        reconsider sn = (s . ( len s)) as Element of ( product F) by FINSEQ_2: 11;

        

         A19: (( len t) + 1) = ( len s) by A14, A7, FINSEQ_1:def 3, A13;

        ( len (t ^ <*sn*>)) = ( len s) by A19, FINSEQ_2: 16;

        

        then

         A20: ( dom (t ^ <*sn*>)) = ( Seg ( len s)) by FINSEQ_1:def 3

        .= ( dom s) by FINSEQ_1:def 3;

        

         A21: s = (t ^ <*sn*>)

        proof

          for k be Nat st k in ( dom s) holds (s . k) = ((t ^ <*sn*>) . k)

          proof

            let k be Nat;

            assume k in ( dom s);

            then

             A22: k in ( Seg (( len t) + 1)) by A19, FINSEQ_1:def 3;

            now

              per cases by A22, FINSEQ_2: 7;

                case

                 A23: k in ( Seg ( len t));

                then k in ( dom t) by FINSEQ_1:def 3;

                

                then ((t ^ <*sn*>) . k) = (t . k) by FINSEQ_1:def 7

                .= (s . k) by A23, A15, FUNCT_1: 49;

                hence thesis;

              end;

                case k = (( len t) + 1);

                hence thesis by A19, FINSEQ_1: 42;

              end;

            end;

            hence thesis;

          end;

          hence thesis by A20, FINSEQ_1: 13;

        end;

        

         A24: x = (y * sn) by A21, A7, GROUP_4: 6;

        (s . ( len s)) in ( ProjGroup (F,ls)) by A7, A18;

        then (s . ( len s)) in the carrier of ( ProjGroup (F,ls)) by STRUCT_0:def 5;

        then

         A25: (s . ( len s)) in ( ProjSet (F,ls)) by Def2;

        consider snn be Function, gn be Element of (F . ls) such that

         A26: snn = sn & ( dom snn) = ( Seg n) & (snn . ls) = gn & for k be Element of ( Seg n) st k <> ls holds (snn . k) = ( 1_ (F . k)) by A25, Th2;

        thus (x . J) = ( 1_ GJ)

        proof

          reconsider J0 = J as Element of ( Seg n) by A1, FINSEQ_1: 1;

          

           A27: (snn . J0) = ( 1_ (F . J0)) by A26, A7;

          

          thus (x . J) = (( 1_ (F . J0)) * ( 1_ (F . J0))) by A17, A26, A27, A24, A1, GROUP_7: 1

          .= ( 1_ GJ) by A1, GROUP_1:def 4;

        end;

      end;

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

      hence thesis;

    end;

    theorem :: GROUP_12:9

    

     Th9: for F be associative Group-like multMagma-Family of ( Seg n), x be Element of ( product F), s be FinSequence of ( product F) st ( len s) = n & (for k be Element of ( Seg n) holds (s . k) in ( ProjGroup (F,k))) & x = ( Product s) holds for i be Nat st 1 <= i & i <= n holds ex si be Element of ( product F) st si = (s . i) & (x . i) = (si . i)

    proof

      let F be associative Group-like multMagma-Family of ( Seg n);

      defpred P[ Nat] means for x be Element of ( product F), s be FinSequence of ( product F) st 1 <= ( len s) & ( len s) <= $1 & $1 <= n & (for k be Element of ( Seg n) st k in ( dom s) holds (s . k) in ( ProjGroup (F,k))) & x = ( Product s) holds for i be Nat st 1 <= i & i <= ( len s) holds ex si be Element of ( product F) st si = (s . i) & (x . i) = (si . i);

      

       A1: P[ 0 ];

      

       A2: for m be Nat st P[m] holds P[(m + 1)]

      proof

        let m be Nat;

        assume

         A3: P[m];

        let x be Element of ( product F), s be FinSequence of ( product F);

        assume

         A4: 1 <= ( len s) & ( len s) <= (m + 1) & (m + 1) <= n & (for k be Element of ( Seg n) st k in ( dom s) holds (s . k) in ( ProjGroup (F,k))) & x = ( Product s);

        per cases ;

          suppose m = 0 ;

          then

           A5: ( len s) = 1 by A4, XXREAL_0: 1;

          then

           A6: s = <*(s . 1)*> by FINSEQ_1: 40;

          thus for i be Nat st 1 <= i & i <= ( len s) holds ex si be Element of ( product F) st si = (s . i) & (x . i) = (si . i)

          proof

            let i be Nat;

            assume

             A7: 1 <= i & i <= ( len s);

            1 in ( Seg ( len s)) by A4;

            then 1 in ( dom s) by FINSEQ_1:def 3;

            then

            reconsider si = (s . 1) as Element of ( product F) by FINSEQ_2: 11;

            take si;

            thus thesis by A7, A6, A4, A5, GROUP_4: 9, XXREAL_0: 1;

          end;

        end;

          suppose

           A8: m <> 0 ;

          now

            per cases ;

              suppose

               A9: ( len s) <= m;

              1 <= ( len s) & ( len s) <= m & m <= n

              proof

                ((m + 1) - 1) <= (n - 0 ) by A4, XREAL_1: 13;

                hence thesis by A4, A9;

              end;

              hence for i be Nat st 1 <= i & i <= ( len s) holds ex si be Element of ( product F) st si = (s . i) & (x . i) = (si . i) by A3, A4;

            end;

              suppose

               A10: ( len s) > m;

              

               A11: ( len s) = (m + 1) by A4, A10, NAT_1: 8;

              

               A12: ( len s) <= n by A4, A10, NAT_1: 8;

              then ( len s) in ( Seg n) by A4;

              then

              reconsider ls = ( len s) as Element of ( Seg n);

              set t = (s | m);

              

               A13: m < (m + 1) by NAT_1: 13;

              

               A14: m in NAT by ORDINAL1:def 12;

              ( dom s) = ( Seg (m + 1)) by A11, FINSEQ_1:def 3;

              then ( Seg m) c= ( dom s) by A13, FINSEQ_1: 5;

              then ( dom t) = ( Seg m) by RELAT_1: 62;

              then

               A15: ( len t) = m by FINSEQ_1:def 3, A14;

              

               A16: ( 0 + 1) <= m by A8, NAT_1: 13;

              

               A17: ((m + 1) - 1) <= (n - 0 ) by A4, XREAL_1: 13;

              

               A18: ( dom s) = ( Seg ( len s)) & ( dom t) = ( Seg ( len t)) by FINSEQ_1:def 3;

               A19:

              now

                let k be Element of ( Seg n);

                assume

                 A20: k in ( dom t);

                then

                 A21: (t . k) = (s . k) by FUNCT_1: 47;

                ( Seg ( len t)) c= ( Seg ( len s)) by A15, A10, FINSEQ_1: 5;

                hence (t . k) in ( ProjGroup (F,k)) by A21, A4, A20, A18;

              end;

              set y = ( Product t);

              

               A22: ( len s) in ( Seg ( len s)) by A4;

              then

              reconsider sn = (s . ( len s)) as Element of ( product F) by A18, FINSEQ_2: 11;

              

               A23: s = (t ^ <*sn*>) by A11, FINSEQ_3: 55;

              

               A24: x = (y * sn) by A23, A4, GROUP_4: 6;

              (s . ( len s)) in ( ProjGroup (F,ls)) by A18, A4, A22;

              then (s . ( len s)) in the carrier of ( ProjGroup (F,ls)) by STRUCT_0:def 5;

              then

               A25: (s . ( len s)) in ( ProjSet (F,ls)) by Def2;

              set Gn = (F . ls);

              consider snn be Function, gn be Element of (F . ls) such that

               A26: snn = sn & ( dom snn) = ( Seg n) & (snn . ls) = gn & for k be Element of ( Seg n) st k <> ls holds (snn . k) = ( 1_ (F . k)) by A25, Th2;

              thus for i be Nat st 1 <= i & i <= ( len s) holds ex si be Element of ( product F) st si = (s . i) & (x . i) = (si . i)

              proof

                let i be Nat;

                assume

                 A27: 1 <= i & i <= ( len s);

                per cases ;

                  suppose

                   A28: i <> ( len s);

                  then

                   A29: i < ( len s) by A27, XXREAL_0: 1;

                  ( len s) = (( len t) + ( len <*sn*>)) by A23, FINSEQ_1: 22

                  .= (( len t) + 1) by FINSEQ_1: 40;

                  then

                   A30: 1 <= i & i <= ( len t) by A27, A29, NAT_1: 13;

                  then

                  consider ti be Element of ( product F) such that

                   A31: ti = (t . i) & (y . i) = (ti . i) by A3, A17, A19, A15, A16;

                  

                   A32: (t . i) = (s . i) by A30, A23, FINSEQ_1: 64;

                  1 <= i & i <= n by A30, A17, A15, XXREAL_0: 2;

                  then

                  reconsider ii = i as Element of ( Seg n) by FINSEQ_1: 1;

                  

                   A33: (sn . ii) = ( 1_ (F . ii)) by A26, A28;

                  consider Rii be 1-sorted such that

                   A34: Rii = (F . ii) & (( Carrier F) . ii) = the carrier of Rii by PRALG_1:def 15;

                  

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

                  

                   A36: ( dom ( Carrier F)) = ( Seg n) by PARTFUN1:def 2;

                  reconsider tii = (ti . i) as Element of (F . ii) by A34, A35, A36, CARD_3: 9;

                  (x . i) = (tii * ( 1_ (F . ii))) by A31, A33, A24, GROUP_7: 1

                  .= (ti . i) by GROUP_1:def 4;

                  hence thesis by A31, A32;

                end;

                  suppose

                   A37: i = ( len s);

                  

                   A38: (y . i) = ( 1_ Gn) by A37, Th8, A19, A10, A15, A12, A27;

                  (x . i) = (( 1_ Gn) * gn) by A37, A38, A26, A24, GROUP_7: 1

                  .= (sn . i) by A26, A37, GROUP_1:def 4;

                  hence thesis by A37;

                end;

              end;

            end;

          end;

          hence for i be Nat st 1 <= i & i <= ( len s) holds ex si be Element of ( product F) st si = (s . i) & (x . i) = (si . i);

        end;

      end;

      

       A39: for m be Nat holds P[m] from NAT_1:sch 2( A1, A2);

      thus for x be Element of ( product F), s be FinSequence of ( product F) st ( len s) = n & (for k be Element of ( Seg n) holds (s . k) in ( ProjGroup (F,k))) & x = ( Product s) holds for i be Nat st 1 <= i & i <= n holds ex si be Element of ( product F) st si = (s . i) & (x . i) = (si . i)

      proof

        let x be Element of ( product F), s be FinSequence of ( product F);

        assume

         A40: ( len s) = n & (for k be Element of ( Seg n) holds (s . k) in ( ProjGroup (F,k))) & x = ( Product s);

        

         A41: 1 <= ( len s) & ( len s) <= n by A40, NAT_1: 14;

        for k be Element of ( Seg n) st k in ( dom s) holds (s . k) in ( ProjGroup (F,k)) by A40;

        hence thesis by A40, A41, A39;

      end;

    end;

    theorem :: GROUP_12:10

    

     Th10: for F be associative Group-like multMagma-Family of ( Seg n), x be Element of ( product F), s,t be FinSequence of ( product F) st ( len s) = n & (for k be Element of ( Seg n) holds (s . k) in ( ProjGroup (F,k))) & x = ( Product s) & ( len t) = n & (for k be Element of ( Seg n) holds (t . k) in ( ProjGroup (F,k))) & x = ( Product t) holds s = t

    proof

      let F be associative Group-like multMagma-Family of ( Seg n), x be Element of ( product F), s,t be FinSequence of ( product F);

      set I = ( Seg n);

      assume that

       A1: ( len s) = n and

       A2: (for k be Element of I holds (s . k) in ( ProjGroup (F,k))) and

       A3: x = ( Product s) and

       A4: ( len t) = n and

       A5: (for k be Element of I holds (t . k) in ( ProjGroup (F,k))) and

       A6: x = ( Product t);

      now

        let i be Nat;

        assume

         A7: 1 <= i & i <= n;

        then

        reconsider i0 = i as Element of I by FINSEQ_1: 1;

        consider si be Element of ( product F) such that

         A8: si = (s . i) & (x . i) = (si . i) by A1, A2, A3, A7, Th9;

        consider ti be Element of ( product F) such that

         A9: ti = (t . i) & (x . i) = (ti . i) by A4, A5, A6, A7, Th9;

        (s . i0) in ( ProjGroup (F,i0)) by A2;

        then (s . i0) in the carrier of ( ProjGroup (F,i0)) by STRUCT_0:def 5;

        then

         A10: (s . i0) in ( ProjSet (F,i0)) by Def2;

        consider sn be Function, gn be Element of (F . i0) such that

         A11: sn = si & ( dom sn) = I & (sn . i0) = gn & for k be Element of I st k <> i0 holds (sn . k) = ( 1_ (F . k)) by A8, A10, Th2;

        (t . i0) in ( ProjGroup (F,i0)) by A5;

        then (t . i0) in the carrier of ( ProjGroup (F,i0)) by STRUCT_0:def 5;

        then

         A12: (t . i0) in ( ProjSet (F,i0)) by Def2;

        consider tn be Function, fn be Element of (F . i0) such that

         A13: tn = ti & ( dom tn) = I & (tn . i0) = fn & for k be Element of I st k <> i0 holds (tn . k) = ( 1_ (F . k)) by A9, A12, Th2;

        now

          let x be object;

          assume x in ( dom sn);

          then

          reconsider j = x as Element of I by A11;

          per cases ;

            suppose j = i;

            hence (sn . x) = (tn . x) by A8, A9, A11, A13;

          end;

            suppose

             A14: j <> i;

            then (sn . j) = ( 1_ (F . j)) by A11;

            hence (sn . x) = (tn . x) by A14, A13;

          end;

        end;

        hence (s . i) = (t . i) by A8, A9, A11, A13, FUNCT_1: 2;

      end;

      hence thesis by A1, A4;

    end;

    theorem :: GROUP_12:11

    

     Th11: for F be associative Group-like multMagma-Family of ( Seg n), x be Element of ( product F) holds ex s be FinSequence of ( product F) st ( len s) = n & (for k be Element of ( Seg n) holds (s . k) in ( ProjGroup (F,k))) & x = ( Product s)

    proof

      let F be associative Group-like multMagma-Family of ( Seg n), x be Element of ( product F);

      set I = ( Seg n);

      defpred P[ Nat, set] means ex k be Element of I, g be Element of (F . k) st k = $1 & (x . k) = g & $2 = (( 1_ ( product F)) +* (k,g));

      

       A1: for k be Nat st k in ( Seg n) holds ex z be Element of ( product F) st P[k, z]

      proof

        let k be Nat;

        assume k in ( Seg n);

        then

        reconsider k0 = k as Element of I;

        

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

        

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

        consider Rj be 1-sorted such that

         A4: Rj = (F . k0) & (( Carrier F) . k0) = the carrier of Rj by PRALG_1:def 15;

        reconsider g = (x . k0) as Element of (F . k0) by A4, A3, A2, CARD_3: 9;

        (( 1_ ( product F)) +* (k0,g)) in ( ProjSet (F,k0)) by Def1;

        then

        reconsider z = (( 1_ ( product F)) +* (k0,g)) as Element of ( product F);

        take z;

        thus P[k, z];

      end;

      consider s be FinSequence of ( product F) such that

       A5: ( dom s) = ( Seg n) & for k be Nat st k in ( Seg n) holds P[k, (s . k)] from FINSEQ_1:sch 5( A1);

      take s;

      n in NAT by ORDINAL1:def 12;

      hence

       A6: ( len s) = n by A5, FINSEQ_1:def 3;

      thus

       A7: for k be Element of I holds (s . k) in ( ProjGroup (F,k))

      proof

        let k be Element of ( Seg n);

        ex k0 be Element of I, g be Element of (F . k0) st k0 = k & (x . k0) = g & (s . k) = (( 1_ ( product F)) +* (k0,g)) by A5;

        then

         A8: (s . k) in ( ProjSet (F,k)) by Def1;

        the carrier of ( ProjGroup (F,k)) = ( ProjSet (F,k)) by Def2;

        hence thesis by A8, STRUCT_0:def 5;

      end;

      set y = ( Product s);

      

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

      

       A10: ( dom x) = ( Seg n) by A9, PARTFUN1:def 2;

      

       A11: ( dom y) = ( Seg n) by A9, PARTFUN1:def 2;

      

       A12: ( dom ( 1_ ( product F))) = I by A9, PARTFUN1:def 2;

      now

        let t be object;

        assume t in ( dom x);

        then

         A13: t in ( Seg n) by A9, PARTFUN1:def 2;

        then

        reconsider i = t as Nat;

        1 <= i & i <= n by A13, FINSEQ_1: 1;

        then

         A14: ex si be Element of ( product F) st si = (s . i) & (y . i) = (si . i) by Th9, A6, A7;

        ex i1 be Element of I, g be Element of (F . i1) st i1 = i & (x . i1) = g & (s . i) = (( 1_ ( product F)) +* (i1,g)) by A13, A5;

        hence (x . t) = (y . t) by A12, A14, FUNCT_7: 31;

      end;

      hence thesis by A10, A11, FUNCT_1: 2;

    end;

    theorem :: GROUP_12:12

    

     Th12: for G be commutative Group, F be associative Group-like multMagma-Family of ( Seg n) st (for i be Element of ( Seg n) holds (F . i) is Subgroup of G) & (for x be Element of G holds ex s be FinSequence of G st ( len s) = n & (for k be Element of ( Seg n) holds (s . k) in (F . k)) & x = ( Product s)) & (for s,t be FinSequence of G st ( len s) = n & (for k be Element of ( Seg n) holds (s . k) in (F . k)) & ( len t) = n & (for k be Element of ( Seg n) holds (t . k) in (F . k)) & ( Product s) = ( Product t) holds s = t) holds ex f be Homomorphism of ( product F), G st f is bijective & for x be Element of ( product F) holds ex s be FinSequence of G st ( len s) = n & (for k be Element of ( Seg n) holds (s . k) in (F . k)) & s = x & (f . x) = ( Product s)

    proof

      let G be commutative Group, F be associative Group-like multMagma-Family of ( Seg n);

      set I = ( Seg n);

      assume that

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

       A2: for x be Element of G holds ex s be FinSequence of G st ( len s) = n & (for k be Element of I holds (s . k) in (F . k)) & x = ( Product s) and

       A3: for s,t be FinSequence of G st ( len s) = n & (for k be Element of I holds (s . k) in (F . k)) & ( len t) = n & (for k be Element of I holds (t . k) in (F . k)) & ( Product s) = ( Product t) holds s = t;

      

       A4: for x be Element of ( product F) holds x is FinSequence of G & ( dom x) = I & ( dom x) = ( dom ( Carrier F)) & for i be set st i in ( dom ( Carrier F)) holds (x . i) in (( Carrier F) . i)

      proof

        let x be Element of ( product F);

        

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

        

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

        ( dom x) = ( Seg n) by A5, PARTFUN1:def 2;

        then

        reconsider s = x as FinSequence by FINSEQ_1:def 2;

        

         A7: for i be Element of I holds (x . i) in the carrier of (F . i)

        proof

          let i be Element of I;

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

          hence (x . i) in the carrier of (F . i) by A6, A5, CARD_3: 9;

        end;

        for i be Nat st i in ( dom s) holds (s . i) in the carrier of G

        proof

          let i be Nat;

          assume i in ( dom s);

          then

          reconsider j = i as Element of I by A5, PARTFUN1:def 2;

          

           A8: (s . j) in the carrier of (F . j) by A7;

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

          then the carrier of (F . j) c= the carrier of G by GROUP_2:def 5;

          hence (s . i) in the carrier of G by A8;

        end;

        hence thesis by A5, CARD_3: 9, FINSEQ_2: 12, PARTFUN1:def 2;

      end;

      defpred P[ set, set] means ex s be FinSequence of G st ( len s) = n & (for k be Element of I holds (s . k) in (F . k)) & s = $1 & $2 = ( Product s);

      

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

      proof

        let x be Element of ( product F);

        

         A10: x is FinSequence of G & ( dom x) = I & ( dom x) = ( dom ( Carrier F)) & for i be set st i in ( dom ( Carrier F)) holds (x . i) in (( Carrier F) . i) by A4;

        reconsider s = x as FinSequence of G by A4;

        

         A11: ( dom x) = ( Seg n) by A4;

        

         A12: for i be Element of I holds (x . i) in the carrier of (F . i)

        proof

          let i be Element of I;

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

          hence (x . i) in the carrier of (F . i) by A10;

        end;

        n in NAT by ORDINAL1:def 12;

        then

         A13: ( len s) = n by A11, FINSEQ_1:def 3;

         A14:

        now

          let k be Element of I;

          (s . k) in the carrier of (F . k) by A12;

          hence (s . k) in (F . k) by STRUCT_0:def 5;

        end;

        take ( Product s);

        thus P[x, ( Product s)] by A13, A14;

      end;

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

       A15: for x be Element of the carrier of ( product F) holds P[x, (f . x)] from FUNCT_2:sch 3( A9);

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

      proof

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

        

         A16: a is FinSequence of G & ( dom a) = I & ( dom a) = ( dom ( Carrier F)) & for i be set st i in ( dom ( Carrier F)) holds (a . i) in (( Carrier F) . i) by A4;

        reconsider a1 = a as FinSequence of G by A4;

        

         A17: b is FinSequence of G & ( dom b) = I & ( dom b) = ( dom ( Carrier F)) & for i be set st i in ( dom ( Carrier F)) holds (b . i) in (( Carrier F) . i) by A4;

        reconsider b1 = b as FinSequence of G by A4;

        reconsider ab1 = (a * b) as FinSequence of G by A4;

         A18:

        now

          let k be Nat;

          assume k in ( dom ab1);

          then

          reconsider k0 = k as Element of I by A4;

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

          then

          reconsider aa = (a . k0) as Element of (F . k0) by A16;

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

          then

          reconsider bb = (b . k0) as Element of (F . k0) by A17;

          

           A19: aa = (a1 /. k0) by A16, PARTFUN1:def 6;

          

           A20: bb = (b1 /. k0) by A17, PARTFUN1:def 6;

          

           A21: (F . k0) is Subgroup of G by A1;

          

          thus (ab1 . k) = (aa * bb) by GROUP_7: 1

          .= ((a1 /. k) * (b1 /. k)) by A19, A20, A21, GROUP_2: 43;

        end;

        

         A22: ex sa be FinSequence of G st ( len sa) = n & (for k be Element of I holds (sa . k) in (F . k)) & sa = a & (f . a) = ( Product sa) by A15;

        

         A23: ex sb be FinSequence of G st ( len sb) = n & (for k be Element of I holds (sb . k) in (F . k)) & sb = b & (f . b) = ( Product sb) by A15;

        ex sab be FinSequence of G st ( len sab) = n & (for k be Element of I holds (sab . k) in (F . k)) & sab = (a * b) & (f . (a * b)) = ( Product sab) by A15;

        hence thesis by A18, A22, A23, GROUP_4: 17;

      end;

      then

      reconsider f as Homomorphism of ( product F), G by GROUP_6:def 6;

      take f;

      now

        let y be object;

        assume y in the carrier of G;

        then

        consider s be FinSequence of G such that

         A24: ( len s) = n & (for k be Element of I holds (s . k) in (F . k)) & y = ( Product s) by A2;

        

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

        

         A26: ( dom s) = I by A24, FINSEQ_1:def 3;

        

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

        

         A28: for x be object st x in ( dom ( Carrier F)) holds (s . x) in (( Carrier F) . x)

        proof

          let x be object;

          assume x in ( dom ( Carrier F));

          then

          reconsider i = x as Element of I;

          

           A29: (s . i) in (F . i) by A24;

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

          hence (s . x) in (( Carrier F) . x) by A29, STRUCT_0:def 5;

        end;

        reconsider x = s as Element of ( product F) by A25, A26, A27, A28, CARD_3: 9;

        ex t be FinSequence of G st ( len t) = n & (for k be Element of I holds (t . k) in (F . k)) & t = x & (f . x) = ( Product t) by A15;

        hence y in ( rng f) by A24, FUNCT_2: 4;

      end;

      then

       A30: the carrier of G c= ( rng f) by TARSKI:def 3;

      ( rng f) = the carrier of G by A30, XBOOLE_0:def 10;

      then

       A31: f is onto by FUNCT_2:def 3;

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

      proof

        let x1,x2 be object;

        assume

         A32: x1 in the carrier of ( product F) & x2 in the carrier of ( product F) & (f . x1) = (f . x2);

        consider s be FinSequence of G such that

         A33: ( len s) = n & (for k be Element of I holds (s . k) in (F . k)) & s = x1 & (f . x1) = ( Product s) by A15, A32;

        consider t be FinSequence of G such that

         A34: ( len t) = n & (for k be Element of I holds (t . k) in (F . k)) & t = x2 & (f . x2) = ( Product t) by A15, A32;

        thus x1 = x2 by A3, A33, A32, A34;

      end;

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

      hence thesis by A15, A31;

    end;

    theorem :: GROUP_12:13

    for G,F be associative commutative Group-like multMagma-Family of ( Seg n) st for k be Element of ( Seg n) holds (F . k) = ( ProjGroup (G,k)) holds ex f be Homomorphism of ( product F), ( product G) st f is bijective & for x be Element of ( product F) holds ex s be FinSequence of ( product G) st ( len s) = n & (for k be Element of ( Seg n) holds (s . k) in (F . k)) & s = x & (f . x) = ( Product s)

    proof

      let G,F be associative commutative Group-like multMagma-Family of ( Seg n);

      assume

       A1: for k be Element of ( Seg n) holds (F . k) = ( ProjGroup (G,k));

      

       A2: for i be Element of ( Seg n) holds (F . i) is Subgroup of ( product G)

      proof

        let i be Element of ( Seg n);

        (F . i) = ( ProjGroup (G,i)) by A1;

        hence thesis;

      end;

      

       A3: for x be Element of ( product G) holds ex s be FinSequence of ( product G) st ( len s) = n & (for k be Element of ( Seg n) holds (s . k) in (F . k)) & x = ( Product s)

      proof

        let x be Element of ( product G);

        consider s be FinSequence of ( product G) such that

         A4: ( len s) = n & (for k be Element of ( Seg n) holds (s . k) in ( ProjGroup (G,k))) & x = ( Product s) by Th11;

        take s;

        for k be Element of ( Seg n) holds (s . k) in (F . k)

        proof

          let k be Element of ( Seg n);

          (s . k) in ( ProjGroup (G,k)) by A4;

          hence thesis by A1;

        end;

        hence thesis by A4;

      end;

      for s,t be FinSequence of ( product G) st ( len s) = n & (for k be Element of ( Seg n) holds (s . k) in (F . k)) & ( len t) = n & (for k be Element of ( Seg n) holds (t . k) in (F . k)) & ( Product s) = ( Product t) holds s = t

      proof

        let s,t be FinSequence of ( product G);

        assume

         A5: ( len s) = n & (for k be Element of ( Seg n) holds (s . k) in (F . k)) & ( len t) = n & (for k be Element of ( Seg n) holds (t . k) in (F . k)) & ( Product s) = ( Product t);

        for k be Element of ( Seg n) holds (t . k) in ( ProjGroup (G,k)) & (s . k) in ( ProjGroup (G,k))

        proof

          let k be Element of ( Seg n);

          (s . k) in (F . k) & (t . k) in (F . k) by A5;

          hence thesis by A1;

        end;

        hence thesis by A5, Th10;

      end;

      hence thesis by A2, A3, Th12;

    end;