:: Normal Subgroup of Product of Groups
::  by Hiroyuki Okazaki , Kenichi Arai and Yasunari Shidama
::
:: Received July 2, 2010
:: Copyright (c) 2010-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies FINSEQ_1, FUNCT_1, RELAT_1, RLVECT_2, CARD_3, TARSKI, BINOP_1,
      GROUP_1, XXREAL_0, GROUP_2, CARD_1, NUMBERS, FUNCT_4, GROUP_6, GROUP_7,
      FUNCOP_1, ALGSTR_0, GROUP_12, PARTFUN1, FUNCT_2, SUBSET_1, XBOOLE_0,
      STRUCT_0, NAT_1, ORDINAL4, PRE_TOPC, ARYTM_1, ARYTM_3;
 notations TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, RELAT_1, FUNCT_1, RELSET_1,
      PARTFUN1, FUNCT_2, FUNCT_4, FUNCOP_1, CARD_3, ORDINAL1, NUMBERS,
      FINSEQ_1, XXREAL_0, STRUCT_0, ALGSTR_0, GROUP_1, GROUP_2, GROUP_3,
      GROUP_4, GROUP_6, PRALG_1, GROUP_7, FUNCT_7;
 constructors BINOP_1, REALSET1, FUNCT_4, GROUP_6, MONOID_0, PRALG_1, GROUP_4,
      GROUP_7, FUNCT_7, RELSET_1;
 registrations XBOOLE_0, XREAL_0, STRUCT_0, GROUP_2, MONOID_0, ORDINAL1, NAT_1,
      FUNCT_2, FUNCOP_1, CARD_1, CARD_3, GROUP_7, XXREAL_0, RELSET_1, FINSEQ_1;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
 definitions GROUP_2, FINSEQ_1;
 theorems PRALG_1, FUNCT_1, CARD_3, FUNCT_2, TARSKI, GROUP_1, GROUP_2, GROUP_3,
      GROUP_4, GROUP_6, FINSEQ_2, XREAL_1, ORDINAL1, FINSEQ_1, FINSEQ_3, NAT_1,
      XBOOLE_0, RELAT_1, XXREAL_0, GROUP_7, FUNCT_7, YELLOW17, STRUCT_0,
      PARTFUN1;
 schemes NAT_1, SUBSET_1, FUNCT_2, XBOOLE_0, FINSEQ_1;

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 for multMagma;
  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 for multMagma;
  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 for multMagma;
  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 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 set;
      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;
  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 being 1-sorted st Ri = F.i & (Carrier F).i = the carrier of Ri
    by PRALG_1:def 13;
    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 being set holds x in F1 iff P[x];
  assume
  A6: for x being set holds x in F2 iff P[x];
  thus thesis from XBOOLE_0: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 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 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 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 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 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;
  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 being 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 being Element of F.i
    ex y being 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 being 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 set;
      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 set 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 set;
      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;
  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 being 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 being 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 set;
        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 being 1-sorted such that
    A8: Ri = F.i & (Carrier F).i = the carrier of Ri by PRALG_1:def 13;
        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 being 1-sorted such that
      A13: Rj = F.j & (Carrier F).j = the carrier of Rj by PRALG_1:def 13;
          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
  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 set st k in dom xy holds xy.k = yx.k
    proof
      let k0 be set;
      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 empty Nat;

theorem Th8:
  for F being 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,FINSEQ_1:1;
      hence x.J = 1_GJ by A1,A4,GROUP_7:6;
    end;
    A5: for m be Element of NAT st P[m] holds P[m+1]
    proof
      let m be Element of 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;
    dom s= Seg (m+1) by A7,FINSEQ_1:def 3;
    then Seg m c= dom s by A8,FINSEQ_1:5;
    then A13:dom t = Seg m by RELAT_1:62;
    then A14:len t =m by FINSEQ_1:def 3;
    A15: len t = (len s) -1 by A13,A7,FINSEQ_1:def 3;
    A16: y.J = 1_GJ by A6,A10,A15,A7,XREAL_1:51;
    len s in Seg len s by A9; then
    A17: 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;
    A18:len t +1 =len s by A13,A7,FINSEQ_1:def 3;
    len (t^<* sn *>) = len s by A18,FINSEQ_2:16;
    then A19: dom (t^<* sn *>)=Seg len s by FINSEQ_1:def 3
    .=dom s by FINSEQ_1:def 3;
    A20: 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 A21: k in Seg (len t +1) by A18,FINSEQ_1:def 3;
        now per cases by A21,FINSEQ_2:7;
          case A22: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 A22,A14,FUNCT_1:49;
            hence thesis;
          end;
          case k= len t +1;
            hence thesis by A18,FINSEQ_1:42;
          end;
        end;
        hence thesis;
      end;
      hence thesis by A19,FINSEQ_1:13;
    end;
A23: x = y*sn by A20,A7,GROUP_4:6;
    s.len s in ProjGroup(F,ls) by A7,A17; then
    s.len s in the carrier of ProjGroup(F,ls) by STRUCT_0:def 5; then
    A24:s.len s in ProjSet(F,ls) by Def2;
    consider snn be Function,gn be Element of (F.ls) such that
    A25: 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 A24,Th2;
    thus x.J = 1_GJ
    proof
      reconsider J0=J as Element of Seg n by A1,FINSEQ_1:1;
      A26: snn.J0 = 1_F.J0 by A25,A7;
      thus x.J =(1_F.J0)*(1_F.J0) by A16,A25,A26,A23,A1,GROUP_7:1
      .=1_GJ by A1,GROUP_1:def 4;
    end;
  end;
  for m be Element of NAT holds P[m] from NAT_1:sch 1(A2,A5);
  hence thesis;
end;

theorem 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 Element of NAT st P[m] holds P[m+1]
    proof
      let m be Element of 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;
            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 A14:len t =m by FINSEQ_1:def 3;
A15:      0+1 <= m by A8,NAT_1:13;
A16:       (m+1)-1 <= n -0 by A4,XREAL_1:13;
A17:         dom s = Seg len s & dom t = Seg len t by FINSEQ_1:def 3;
A18:       now let k be Element of Seg n;
            assume A19: k in dom t; then
A20:       t.k = s.k by FUNCT_1:47;
            Seg len t c= Seg len s by A14,A10,FINSEQ_1:5;
            hence t.k in ProjGroup(F,k) by A20,A4,A19,A17;
          end;
          set y=Product t;
A21:     len s in Seg len s by A4; then
          reconsider sn=s.len s as Element of product F by A17,FINSEQ_2:11;
A22:     s=t^<* sn *> by A11,FINSEQ_3:55;
A23:     x = y*sn by A22,A4,GROUP_4:6;
          s.len s in ProjGroup(F,ls) by A17,A4,A21; then
          s.len s in the carrier of ProjGroup(F,ls) by STRUCT_0:def 5; then
A24:     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
A25:     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 A24,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 A26:1<= i & i<=len s;
            per cases;
            suppose A27: i <> len s; then
              A28: i < len s by A26,XXREAL_0:1;
              len s = len t + len (<* sn *>) by A22,FINSEQ_1:22
              .= len t + 1 by FINSEQ_1:40; then
              A29: 1<= i & i<=len t by A26,A28,NAT_1:13;
              then consider ti be Element of product F such that
              A30: ti=t.i & y.i = ti.i by A3,A16,A18,A14,A15;
              A31:t.i =s.i by A29,A22,FINSEQ_1:64;
              1<=i & i <= n by A29,A16,A14,XXREAL_0:2; then
              reconsider ii=i as Element of Seg n by FINSEQ_1:1;
A32:         sn.ii = 1_F.ii by A25,A27;
              consider Rii being 1-sorted such that
              A33: Rii = F.ii & (Carrier F).ii = the carrier of Rii
              by PRALG_1:def 13;
              A34:the carrier of product F = product Carrier F
                by GROUP_7:def 2;
              A35: dom (Carrier F) = Seg n by PARTFUN1:def 2;
              reconsider tii=ti.i as Element of F.ii by A33,A34,A35,CARD_3:9;
              x.i =tii*(1_F.ii) by A30,A32,A23,GROUP_7:1
              .=ti.i by GROUP_1:def 4;
              hence thesis by A30,A31;
            end;
            suppose A36: i = len s;
              A37: y.i = 1_Gn by A36,Th8,A18,A10,A14,A12,A26;
              x.i =(1_Gn)*gn by A36,A37,A25,A23,GROUP_7:1
              .=sn.i by A25,A36,GROUP_1:def 4;
              hence thesis by A36;
            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;
  A38: for m be Element of NAT holds P[m] from NAT_1:sch 1(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 A39: len s = n
    & (for k be Element of Seg n holds s.k
    in ProjGroup(F,k)) & x=Product s;
A40: 1<=len s & len s <= n by A39,NAT_1:14;
    for k be Element of Seg n st k in dom s holds s.k in ProjGroup(F,k) by A39;
    hence thesis by A39,A40,A38;
  end;
end;

theorem 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 set;
        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,FINSEQ_1:14;
  end;

theorem Th11:
  for F be associative Group-like multMagma-Family of Seg n,
  x be Element of product F
  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
    ex z being 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 being 1-sorted such that
      A4: Rj = F.k0 & (Carrier F).k0 = the carrier of Rj by PRALG_1:def 13;
      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 set;
      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 Th12:
  for G being commutative Group,
  F being 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
  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 being Homomorphism of product F,G
  st f is bijective &
  for x be Element of product F
  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 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 being 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 being 1-sorted st R = F.i &
        (Carrier F).i = the carrier of R by PRALG_1:def 13;
        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 being Element of
    product F ex y being 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 being 1-sorted st R = F.i &
        (Carrier F).i = the carrier of R by PRALG_1:def 13;
        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 being Element of (the carrier of product F)
  holds P[x,f.x] from FUNCT_2:sch 3(A9);
  for a,b being 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 Element of NAT;
    assume k in dom(ab1);
    then reconsider k0= k as Element of I by A4;
    ex R being 1-sorted st R = F.k0 &
    (Carrier F).k0 = the carrier of R by PRALG_1:def 13; then
    reconsider aa=a.k0 as Element of (F.k0) by A16;
    ex R being 1-sorted st R = F.k0 &
    (Carrier F).k0 = the carrier of R by PRALG_1:def 13; 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 set;
  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 set st x in dom Carrier F holds s.x in (Carrier F).x
  proof
    let x be set;
    assume x in dom Carrier F;
    then reconsider i=x as Element of I;
    A29: s.i in F.i by A24;
    ex R being 1-sorted st R = F.i &
    (Carrier F).i = the carrier of R by PRALG_1:def 13;
    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 set 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 set;
  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
  for G,F being 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 being Homomorphism of product F,product G
  st f is bijective &
  for x be Element of product F
  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
    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;