:: Isomorphisms of Direct Products of Finite Cyclic Groups
::  by Kenichi Arai , Hiroyuki Okazaki and Yasunari Shidama

environ

 vocabularies FINSEQ_1, FUNCT_1, RELAT_1, CARD_3, TARSKI, BINOP_2, FINSET_1,
      XXREAL_0, GROUP_2, CARD_1, NUMBERS, ALGSTR_0, FUNCT_2, SUBSET_1,
      XBOOLE_0, STRUCT_0, NAT_1, ORDINAL4, PRE_TOPC, ARYTM_1, ARYTM_3,
      RLVECT_1, SUPINF_2, PRVECT_1, INT_3, XCMPLX_0, INT_1, INT_6, ZFMISC_1,
      VECTSP_1, FUNCSDOM, GROUP_6, GROUP_14, ORDINAL1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
      RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FINSET_1, CARD_1,
      XTUPLE_0, NUMBERS, XCMPLX_0, XXREAL_0, INT_1, CARD_3, FINSEQ_1, RVSUM_1,
      STRUCT_0, ALGSTR_0, PRE_TOPC, RLVECT_1, VECTSP_1, GR_CY_1, PRVECT_1,
      INT_3, INT_6, PRVECT_3, WSIERP_1, MOD_4;
 constructors REALSET1, MONOID_0, PRALG_1, GROUP_4, GROUP_7, FUNCT_7, RELSET_1,
      REAL_1, SQUARE_1, RUSUB_4, ALGSTR_1, CARD_2, PRVECT_2, NAT_D, LOPBAN_1,
      XTUPLE_0, BINOP_2, FINSEQ_4, FINSEQOP, PRVECT_3, SETWISEO, BINOM, INT_3,
      INT_6, POLYNOM1, WELLORD2, WSIERP_1;
 registrations XBOOLE_0, XREAL_0, STRUCT_0, ORDINAL1, NAT_1, FUNCT_2, CARD_1,
      CARD_3, XXREAL_0, RELSET_1, FINSEQ_1, MEMBERED, FUNCT_1, VALUED_0,
      ALGSTR_0, PRVECT_1, INT_1, INT_6, RLVECT_1, PRVECT_3, RELAT_1, SUBSET_1;
 requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
 definitions PRVECT_1;
 equalities FINSEQ_1, BINOP_1, ALGSTR_0, STRUCT_0, PRVECT_1, PRVECT_3, INT_3,
      ORDINAL1;
 expansions ALGSTR_0;
 theorems FUNCT_1, CARD_3, FUNCT_2, TARSKI, FINSEQ_2, XREAL_1, ORDINAL1,
      FINSEQ_1, FINSEQ_3, NAT_1, XBOOLE_0, RELAT_1, XXREAL_0, RLVECT_1,
      RVSUM_1, RELSET_1, ALGSTR_0, PRVECT_1, PRVECT_3, ZFMISC_1, SUBSET_1,
      CARD_1, INT_1, INT_3, INT_6, GR_CY_1, FINSEQ_5, NAT_D, PARTFUN3, CARD_2,
      FINSEQ_4, WELLORD2, TOPGEN_5, MOD_4, VECTSP_1, XTUPLE_0, NDIFF_5;
 schemes NAT_1, BINOP_1, FUNCT_2;

begin

registration
  let G be Abelian add-associative right_zeroed right_complementable
  non empty addLoopStr;
  cluster <* G *> -> non empty AbGroup-yielding for FinSequence;
  correctness
  proof
    now let S be set;
      assume S in rng <*G*>;
      then consider i be object such that
A1:   i in dom <*G*> & <*G*>.i = S by FUNCT_1:def 3;
      reconsider i as Element of NAT by A1;
      dom <*G*> = {1} by FINSEQ_1:2,def 8;
      then i = 1 by A1,TARSKI:def 1;
      hence S is AbGroup by A1,FINSEQ_1:40;
    end;
    hence thesis by PRVECT_1:def 10;
  end;
end;

registration
  let G,F be Abelian add-associative right_zeroed right_complementable
  non empty addLoopStr;
  cluster <* G,F *> -> non empty AbGroup-yielding for FinSequence;
  correctness
  proof
    now let S be set;
      assume S in rng <*G,F*>;
      then consider i be object such that
A1:   i in dom <*G,F*> & <*G,F*>.i = S by FUNCT_1:def 3;
      dom <*G,F*> = {1,2} by FINSEQ_1:2,89;
      then i=1 or i=2 by A1,TARSKI:def 2;
      hence S is AbGroup by A1,FINSEQ_1:44;
    end;
    hence thesis by PRVECT_1:def 10;
  end;
end;

theorem Th1:
  for X be AbGroup holds
  ex I being Homomorphism of X,product <*X*>
  st I is bijective & (for x be Element of X holds I.x = <*x*>)
proof
  let X be AbGroup;
  set CarrX = the carrier of X;
  consider I be Function of CarrX,product <*CarrX*> such that
A1: I is one-to-one & I is onto & (for x be object st x in CarrX holds
  I.x = <*x*>) by PRVECT_3:4;
  len carr <*X*> = len <*X*> by PRVECT_1:def 11;
  then
A2: len carr <*X*> = 1 by FINSEQ_1:40;
A3: dom <*X*> = {1} by FINSEQ_1:2,def 8;
A4: <*X*>.1 = X by FINSEQ_1:def 8;
  1 in {1} by TARSKI:def 1;
  then (carr <*X*>).1 = the carrier of X by A3,A4,PRVECT_1:def 11;
  then
A5: carr <*X*> = <* CarrX *> by A2,FINSEQ_1:40;
  then reconsider I as Function of X,product <*X*>;
  for v,w be Element of X holds I.(v+w) = I.v + I.w
  proof
    let v,w be Element of X;
A6: I.v = <*v*> & I.w = <*w*> & I.(v+w) = <*v+w*> by A1;
A7: <*v*>.1 = v & <*w*>.1 = w by FINSEQ_1:40;
    reconsider Iv = I.v, Iw = I.w as Element of product carr <*X*>;
    1 in {1} by TARSKI:def 1;
    then reconsider j1 = 1 as Element of dom carr <*X*> by A2,FINSEQ_1:2,def 3;
A8: (addop <*X*>).j1 = the addF of (<*X*>.j1) by PRVECT_1:def 12;
A9: ([:addop <*X*>:].(Iv,Iw)).j1 = ((addop <*X*>).j1).(Iv.j1,Iw.j1)
    by PRVECT_1:def 8
      .= v+w by A8,A6,A7,FINSEQ_1:40;
    consider Ivw be Function such that
A10: I.v + I.w = Ivw & dom Ivw = dom carr <*X*> & (for i be object st
    i in dom carr <*X*> holds Ivw.i in carr (<*X*>).i) by CARD_3:def 5;
A11: dom Ivw = Seg 1 by A2,A10,FINSEQ_1:def 3;
    then reconsider Ivw as FinSequence by FINSEQ_1:def 2;
    len Ivw = 1 by A11,FINSEQ_1:def 3;
    hence thesis by A6,A10,A9,FINSEQ_1:40;
  end;
  then reconsider I as Homomorphism of X,product <*X*> by VECTSP_1:def 20;
  take I;
  thus thesis by A1,A5;
end;

registration
  let G,F be non empty AbGroup-yielding FinSequence;
  cluster G^F -> AbGroup-yielding;
  correctness
  proof
    let S be set;
    assume S in rng (G^F);
    then consider i be object such that
A1: i in dom (G^F) & (G^F).i = S by FUNCT_1:def 3;
    reconsider i as Element of NAT by A1;
    per cases by A1,FINSEQ_1:25;
    suppose
A2:   i in dom G;
      then
A3:   (G^F).i = G.i by FINSEQ_1:def 7;
      G.i in rng G by A2,FUNCT_1:3;
      hence S is AbGroup by A3,A1,PRVECT_1:def 10;
    end;
    suppose ex n be Nat st n in dom F & i=len G + n;
      then consider n be Nat such that
A4:   n in dom F & i=len G + n;
A5:   (G^F).i = F.n by A4,FINSEQ_1:def 7;
      F.n in rng F by A4,FUNCT_1:3;
      hence S is AbGroup by A5,A1,PRVECT_1:def 10;
    end;
  end;
end;

theorem Th2:
  for X,Y be AbGroup holds
  ex I be Homomorphism of [:X,Y:],product <*X,Y*> st I is bijective &
  (for x be Element of X, y be Element of Y holds I.(x,y) = <*x,y*>)
proof
  let X,Y be AbGroup;
  set CarrX = the carrier of X;
  set CarrY = the carrier of Y;
  consider I be Function of [:CarrX,CarrY:],product <*CarrX,CarrY*> such that
A1: I is one-to-one & I is onto &
for x,y be object st x in CarrX & y in CarrY
  holds I.(x,y) = <*x,y*> by PRVECT_3:5;
  len carr <*X,Y*> = len <*X,Y*> by PRVECT_1:def 11;
  then
A2: len carr <*X,Y*> = 2 by FINSEQ_1:44;
  then
A3: dom carr <*X,Y*> = {1,2} by FINSEQ_1:2,def 3;
  len <*X,Y*> = 2 by FINSEQ_1:44;
  then
A4: dom <*X,Y*> = {1,2} by FINSEQ_1:2,def 3;
A5: <*X,Y*>.1 = X & <*X,Y*>.2 = Y by FINSEQ_1:44;
  1 in {1,2} & 2 in {1,2} by TARSKI:def 2;
  then (carr <*X,Y*>).1 = CarrX & (carr <*X,Y*>).2 = CarrY
  by A4,A5,PRVECT_1:def 11;
  then
A6: carr <*X,Y*> = <* CarrX,CarrY *> by A2,FINSEQ_1:44;
  then reconsider I as Function of [:X,Y:],product <*X,Y*>;
  for v,w be Element of [:X,Y:] holds I.(v+w) = I.v + I.w
  proof
    let v,w be Element of [:X,Y:];
    consider x1 be Element of X, y1 be Element of Y such that
A7: v = [x1,y1] by SUBSET_1:43;
    consider x2 be Element of X, y2 be Element of Y such that
A8: w = [x2,y2] by SUBSET_1:43;
    I.v = I.(x1,y1) & I.w = I.(x2,y2) by A7,A8;
    then
A9: I.v = <*x1,y1*> & I.w = <*x2,y2*> by A1;
A10: I.(v+w) =I.(x1+x2,y1+y2) by A7,A8,PRVECT_3:def 1
      .= <* x1+x2,y1+y2 *> by A1;
A11: <*x1,y1*>.1 = x1 & <*x2,y2*>.1 = x2 & <*x1,y1*>.2 = y1 & <*x2,y2*>.2 = y2
    by FINSEQ_1:44;
    reconsider Iv = I.v, Iw = I.w as Element of product carr <*X,Y*>;
    reconsider j1=1, j2=2 as Element of dom (carr <*X,Y*>) by A3,TARSKI:def 2;
A12: (addop <*X,Y*>).j1 = the addF of (<*X,Y*>.j1) by PRVECT_1:def 12;
A13: ([:addop <*X,Y*>:].(Iv,Iw)).j1 = ((addop <*X,Y*>).j1).(Iv.j1,Iw.j1)
    by PRVECT_1:def 8
      .= x1+x2 by A12,A9,A11,FINSEQ_1:44;
A14: (addop <*X,Y*>).j2 = the addF of (<*X,Y*>.j2) by PRVECT_1:def 12;
A15: ([:addop <*X,Y*>:].(Iv,Iw)).j2 = ((addop <*X,Y*>).j2).(Iv.j2,Iw.j2)
    by PRVECT_1:def 8
      .= y1+y2 by A14,A9,A11,FINSEQ_1:44;
    consider Ivw be Function such that
A16: I.v + I.w = Ivw & dom Ivw = dom carr <*X,Y*> & (for i be object st
    i in dom carr <*X,Y*> holds Ivw.i in carr (<*X,Y*>).i) by CARD_3:def 5;
A17: dom Ivw = Seg 2 by A2,A16,FINSEQ_1:def 3;
    then reconsider Ivw as FinSequence by FINSEQ_1:def 2;
    len Ivw = 2 by A17,FINSEQ_1:def 3;
    hence thesis by A10,A16,A13,A15,FINSEQ_1:44;
  end;
  then reconsider I as Homomorphism of [:X,Y:],product <*X,Y*>
  by VECTSP_1:def 20;
  take I;
  thus thesis by A1,A6;
end;

theorem Th3:
  for X,Y be Group-Sequence holds
  ex I be Homomorphism of [:product X,product Y:],product (X^Y)
  st I is bijective &
  (for x be Element of product X, y be Element of product Y holds
  ex x1,y1 be FinSequence st x = x1 & y = y1 & I.(x,y) = x1^y1)
proof
  let X,Y be Group-Sequence;
  reconsider CX = carr X, CY = carr Y as non-empty FinSequence;
A1: len CX = len X & len CY = len Y & len carr (X^Y) = len (X^Y)
  by PRVECT_1:def 11;
  consider I be Function of [:product CX,product CY:],product (CX^CY)
  such that
A2: I is one-to-one & I is onto & (for x,y be FinSequence st x in product CX &
  y in product CY holds I.(x,y) = x^y) by PRVECT_3:6;
  set PX = product X;
  set PY = product Y;
  len carr (X^Y) = len X + len Y & len (CX^CY) =len X + len Y
  by A1,FINSEQ_1:22;
  then
A3: dom carr (X^Y) = dom (CX^CY) by FINSEQ_3:29;
A4: for k be Nat st k in dom carr (X^Y) holds carr (X^Y).k = (CX^CY).k
  proof
    let k be Nat;
    assume
A5: k in dom carr (X^Y);
    then reconsider k1 = k as Element of dom (X^Y) by A1,FINSEQ_3:29;
A6: carr (X^Y).k = the carrier of ((X^Y).k1) by PRVECT_1:def 11;
A7: k in dom (X^Y) by A1,A5,FINSEQ_3:29;
    per cases by A7,FINSEQ_1:25;
    suppose
A8:   k in dom X;
      then
A9:   k in dom CX by A1,FINSEQ_3:29;
      reconsider k2 = k1 as Element of dom X by A8;
      thus carr (X^Y).k = the carrier of (X.k2) by A6,FINSEQ_1:def 7
        .= CX.k by PRVECT_1:def 11
        .= (CX^CY).k by A9,FINSEQ_1:def 7;
    end;
    suppose ex n be Nat st n in dom Y & k=len X + n;
      then consider n be Nat such that
A10:  n in dom Y & k = len X + n;
A11:  n in dom CY by A1,A10,FINSEQ_3:29;
      reconsider n1 = n as Element of dom Y by A10;
      thus carr (X^Y).k = the carrier of (Y.n1) by A6,A10,FINSEQ_1:def 7
        .= CY.n by PRVECT_1:def 11
        .= (CX^CY).k by A11,A10,A1,FINSEQ_1:def 7;
    end;
  end;
  then
A12: carr (X^Y) = CX^CY by A3,FINSEQ_1:13;
  reconsider I as Function of [:PX,PY:],product (X^Y) by A3,A4,FINSEQ_1:13;
A13: for x be Element of product X, y be Element of product Y holds ex x1,y1
  be FinSequence st x=x1 & y=y1 & I.(x,y) = x1^y1
  proof
    let x be Element of PX, y be Element of PY;
    reconsider x1=x, y1=y as FinSequence by NDIFF_5:9;
    I.(x,y) = x1^y1 by A2;
    hence thesis;
  end;
  for v,w be Element of [:PX,PY:] holds I.(v+w) = I.v + I.w
  proof
    let v,w be Element of [:PX,PY:];
    consider x1 be Element of PX, y1 be Element of PY such that
A14: v = [x1,y1] by SUBSET_1:43;
    consider x2 be Element of PX, y2 be Element of PY such that
A15: w = [x2,y2] by SUBSET_1:43;
    reconsider xx1=x1, xx2=x2 as FinSequence by NDIFF_5:9;
    reconsider yy1=y1, yy2=y2 as FinSequence by NDIFF_5:9;
    reconsider xx12=x1+x2, yy12=y1+y2 as FinSequence by NDIFF_5:9;
A16: dom xx1 = dom CX & dom xx2 = dom CX & dom xx12 = dom CX & dom yy1 =
    dom CY & dom yy2 = dom CY & dom yy12 = dom CY by CARD_3:9;
    I.v = I.(x1,y1) & I.w = I.(x2,y2) by A14,A15;
    then
A17: I.v = xx1^yy1 & I.w = xx2^yy2 by A2;
    I.(v+w) = I.(x1+x2,y1+y2) by A14,A15,PRVECT_3:def 1;
    then
A18: I.(v+w) = xx12^yy12 by A2;
    then
A19: dom (xx12^yy12) = dom carr (X^Y) by CARD_3:9;
    reconsider Iv = I.v, Iw = I.w as Element of product carr (X^Y);
    reconsider Ivw = I.v + I.w as FinSequence by NDIFF_5:9;
    for j0 be Nat st j0 in dom Ivw holds Ivw.j0 = (xx12^yy12).j0
    proof
      let j0 be Nat;
      assume j0 in dom Ivw;
      then reconsider j=j0 as Element of dom carr (X^Y) by CARD_3:9;
A20:  Ivw.j0 = ((addop (X^Y)).j).(Iv.j,Iw.j) by PRVECT_1:def 8
        .= (the addF of (X^Y).j).(Iv.j,Iw.j) by PRVECT_1:def 12;
      per cases by A20,A3,FINSEQ_1:25;
      suppose
A21:    j0 in dom CX;
        then j0 in dom X by A1,FINSEQ_3:29;
        then
A22:    (X^Y).j = X.j0 by FINSEQ_1:def 7;
A23:    Iv.j = xx1.j & Iw.j = xx2.j by A21,A16,A17,FINSEQ_1:def 7;
A24:    (xx12^yy12).j0 = xx12.j0 by A21,A16,FINSEQ_1:def 7;
        reconsider j1=j0 as Element of dom carr X by A21;
        (the addF of (X^Y).j).(Iv.j,Iw.j) = ((addop X ).j1).(xx1.j1,xx2.j1)
        by A22,A23,PRVECT_1:def 12
          .= (xx12^yy12).j0 by A24,PRVECT_1:def 8;
        hence Ivw.j0 = (xx12^yy12).j0 by A20;
      end;
      suppose ex n be Nat st n in dom CY & j0=len CX + n;
        then consider n be Nat such that
A25:    n in dom CY & j0 = len CX + n;
A26:    len CX = len xx1 & len CX = len xx2 & len CX = len xx12
        by A16,FINSEQ_3:29;
        n in dom Y by A1,A25,FINSEQ_3:29;
        then
A27:    (X^Y).j = Y.n by A25,A1,FINSEQ_1:def 7;
A28:    Iv.j = yy1.n & Iw.j = yy2.n by A16,A17,A25,A26,FINSEQ_1:def 7;
A29:    (xx12^yy12).j0 = yy12.n by A25,A26,A16,FINSEQ_1:def 7;
        reconsider j1=n as Element of dom carr Y by A25;
        (the addF of (X^Y).j).(Iv.j,Iw.j) = ((addop Y).j1).(yy1.j1,yy2.j1)
        by A27,A28,PRVECT_1:def 12
          .= (xx12^yy12).j0 by A29,PRVECT_1:def 8;
        hence Ivw.j0 = (xx12^yy12).j0 by A20;
      end;
    end;
    hence thesis by A18,A19,CARD_3:9,FINSEQ_1:13;
  end;
  then reconsider I as Homomorphism of [:product X,product Y:], product (X^Y)
  by VECTSP_1:def 20;
  take I;
  thus thesis by A13,A2,A12;
end;

theorem Th4:
  for G,F be AbGroup holds
  (for x be set holds x is Element of product <*G,F*> iff
  ex x1 be Element of G, x2 be Element of F st x = <* x1,x2 *>) &
  (for x,y be Element of product <*G,F*>, x1,y1 be Element of G,
  x2,y2 be Element of F st x = <*x1,x2*> & y = <*y1,y2*> holds
  x+y = <*x1+y1,x2+y2*>) & 0.(product <*G,F*>) = <* 0.G,0.F *> &
  (for x be Element of product <*G,F*>, x1 be Element of G, x2 be Element of F
  st x = <* x1,x2 *> holds -x = <* -x1,-x2 *>)
proof
  let G,F be AbGroup;
  consider I be Homomorphism of [:G,F:],product <*G,F*> such that
A1: I is bijective &
  (for x be Element of G, y be Element of F holds I.(x,y) = <*x,y*>) by Th2;
  thus
A2: for x be set holds (x is Element of product <*G,F*> iff ex x1 be Element
  of G, x2 be Element of F st x=<* x1,x2 *>)
  proof
    let y be set;
    hereby assume y is Element of product <*G,F*>;
      then y in the carrier of product <*G,F*>;
      then y in rng I by A1,FUNCT_2:def 3;
      then consider x be Element of the carrier of [:G,F:] such that
A3:   y = I.x by FUNCT_2:113;
      consider x1 be Element of G, x2 be Element of F such that
A4:   x=[x1,x2] by SUBSET_1:43;
      take x1,x2;
      I.(x1,x2) = <*x1,x2*> by A1;
      hence y = <*x1,x2*> by A3,A4;
    end;
    now assume ex x1 be Element of G, x2 be Element of F st y = <*x1,x2*>;
      then consider x1 be Element of G, x2 be Element of F such that
A5:   y = <*x1,x2*>;
A6:   I.[x1,x2] in rng I by FUNCT_2:112;
      I.(x1,x2) = <*x1,x2*> by A1;
      hence y is Element of product <*G,F*> by A5,A6;
    end;
    hence thesis;
  end;
  thus
A7: for x,y be Element of product <*G,F*>, x1,y1 be Element of G, x2,y2 be
  Element of F st x = <*x1,x2*> & y = <*y1,y2*> holds x+y = <*x1+y1,x2+y2*>
  proof
    let x,y be Element of product <*G,F*>;
    let x1,y1 be Element of G, x2,y2 be Element of F;
    assume
A8: x = <*x1,x2*> & y = <*y1,y2*>;
    reconsider z=[x1,x2], w=[y1,y2] as Element of [:G,F:];
A9: z+w = [x1+y1,x2+y2] by PRVECT_3:def 1;
    I.(x1+y1,x2+y2) = <* x1+y1,x2+y2 *> & I.(x1,x2) = <* x1,x2 *> &
    I.(y1,y2) = <* y1,y2 *> by A1;
    hence <* x1+y1,x2+y2 *> =x+y by A9,A8,VECTSP_1:def 20;
  end;
  thus
A10: 0.product <*G,F*> = <* 0.G,0.F *>
  proof
    thus 0.product <*G,F*> = I.(0.[:G,F:]) by MOD_4:40
    .= I.(0.G,0.F)
    .= <* 0.G,0.F *> by A1;
  end;
  thus for x be Element of product <*G,F*>, x1 be Element of G, x2 be Element
  of F st x = <*x1,x2*> holds -x = <* -x1,-x2 *>
  proof
    let x be Element of product <*G,F*>;
    let x1 be Element of G, x2 be Element of F;
    assume
A11: x=<* x1,x2 *>;
    reconsider y = <* -x1,-x2 *> as Element of product <*G,F*> by A2;
    x+y = <* x1+-x1,x2+-x2 *> by A7,A11
      .= <* 0.G,x2+-x2 *> by RLVECT_1:def 10
      .= 0.(product <*G,F*>) by A10,RLVECT_1:def 10;
    hence thesis by RLVECT_1:def 10;
  end;
end;

theorem
  for G,F be AbGroup holds
  (for x be set holds x is Element of [:G,F:] iff ex x1 be Element of G,
  x2 be Element of F st x = [x1,x2]) &
  (for x,y be Element of [:G,F:], x1,y1 be Element of G, x2,y2 be Element of F
  st x = [x1,x2] & y = [y1,y2] holds x+y = [x1+y1,x2+y2]) &
  0.[:G,F:] = [0.G,0.F] &
  (for x be Element of [:G,F:], x1 be Element of G, x2 be Element of F
  st x = [x1,x2] holds -x = [-x1,-x2])
proof
  let G,F be AbGroup;
  thus for x be set holds (x is Element of [:G,F:] iff ex x1 be Element of G,
  x2 be Element of F st x=[x1,x2]) by SUBSET_1:43;
  thus for x,y be Element of [:G,F:], x1,y1 be Element of G,x2,y2 be Element
  of F st x = [x1,x2] & y=[y1,y2] holds x+y = [x1+y1,x2+y2] by PRVECT_3:def 1;
  thus 0.[:G,F:] = [0.G,0.F];
  thus for x be Element of [:G,F:], x1 be Element of G, x2 be Element of F st
  x = [x1,x2] holds -x = [-x1,-x2]
  proof
    let x be Element of [:G,F:];
    let x1 be Element of G, x2 be Element of F;
    assume
A1: x=[x1,x2];
    reconsider y= [-x1,-x2 ] as Element of [:G,F:];
    x+y = [x1+-x1,x2+-x2] by A1,PRVECT_3:def 1
      .= [0.G,x2+-x2] by RLVECT_1:def 10
      .= 0.[:G,F:] by RLVECT_1:def 10;
    hence thesis by RLVECT_1:def 10;
  end;
end;

theorem Th6:
  for G,H,I being AddGroup, h being Homomorphism of G,H
  for h1 being Homomorphism of H,I holds
  h1 * h is Homomorphism of G,I
proof
  let G,H,I be AddGroup;
  let h be Homomorphism of G,H;
  let h1 be Homomorphism of H,I;
  reconsider f = h1 * h as Function of G, I;
  now
    let a,b be Element of G;
    thus f.(a + b) = h1.(h.(a + b)) by FUNCT_2:15
      .= h1.(h.a + h.b) by VECTSP_1:def 20
      .= (h1.(h.a)) + (h1.(h.b)) by VECTSP_1:def 20
      .= f.a + (h1.(h.b)) by FUNCT_2:15
      .= f.a + f.b by FUNCT_2:15;
  end;
  hence thesis by VECTSP_1:def 20;
end;

definition
  let G,H,I be AddGroup;
  let h be Homomorphism of G,H;
  let h1 be Homomorphism of H,I;
  redefine func h1 * h -> Homomorphism of G,I;
  coherence by Th6;
end;

theorem Th7:
  for G,H being AddGroup, h being Homomorphism of G,H st h is bijective holds
  h" is Homomorphism of H,G
proof
  let G,H be AddGroup, h be Homomorphism of G,H;
  assume
A1: h is bijective;
  then
A2: h is one-to-one & rng h = the carrier of H by FUNCT_2:def 3;
  then reconsider h1 = h" as Function of H,G by FUNCT_2:25;
  now
    let a,b be Element of H;
    set a1 = h1.a, b1 = h1.b;
    h.a1 = a & h.b1 = b by A2,FUNCT_1:32;
    hence h1.(a + b) = h1.(h.(a1 + b1)) by VECTSP_1:def 20
      .= h1.a + h1.b by A1,FUNCT_2:26;
  end;
  hence thesis by VECTSP_1:def 20;
end;

theorem
  for X,Y be Group-Sequence holds
  ex I be Homomorphism of product <* product X,product Y *>,product (X^Y)
  st I is bijective &
  (for x be Element of product X, y be Element of product Y holds
  ex x1,y1 be FinSequence st x = x1 & y = y1 & I.<*x,y*> = x1^y1)
proof
  let X,Y be Group-Sequence;
  set PX = product X;
  set PY = product Y;
  set PXY = product(X^Y);
  consider K be Homomorphism of [:PX,PY:],PXY such that
A1: K is bijective & (for x be Element of PX, y be Element of PY
  holds ex x1,y1 be FinSequence st x=x1 & y=y1 & K.(x,y) = x1^y1) by Th3;
  consider J be Homomorphism of [:PX,PY:],product<*PX,PY*> such that
A2: J is bijective & (for x be Element of PX, y be Element of PY
  holds J.(x,y) = <*x,y*>) by Th2;
  reconsider JB = J" as Homomorphism of product <*PX,PY*>,[:PX,PY:] by A2,Th7;
  dom J = the carrier of [:PX,PY:] by FUNCT_2:def 1;
  then rng JB = the carrier of [:PX,PY:] by A2,FUNCT_1:33;
  then
A3: JB is onto by FUNCT_2:def 3;
  reconsider I= K*JB as Homomorphism of product <*PX,PY*>,PXY;
  take I;
  I is onto by A1,A3,FUNCT_2:27;
  hence I is bijective by A1,A2;
  thus for x be Element of PX, y be Element of PY holds ex x1,y1 be FinSequence
  st x = x1 & y = y1 & I.<*x,y*> = x1^y1
  proof
    let x be Element of PX, y be Element of PY;
    consider x1,y1 be FinSequence such that
A4: x=x1 & y=y1 & K.(x,y) = x1^y1 by A1;
A5: J.(x,y) = <*x,y*> by A2;
    [x,y] in the carrier of [:PX,PY:];
    then
A6: [x,y] in dom J by FUNCT_2:def 1;
    I.<*x,y*> = K.(JB.(J.[x,y])) by A5,FUNCT_2:15;
    then I.<*x,y*> = x1^y1 by A4,A6,A2,FUNCT_1:34;
    hence thesis by A4;
  end;
end;

theorem Th9:
  for X,Y be AbGroup holds
  ex I be Homomorphism of [:X,Y:],[:X,product <*Y*>:] st I is bijective &
  (for x be Element of X, y be Element of Y holds I.(x,y) = [x,<*y*>])
proof
  let X,Y be AbGroup;
  consider J be Homomorphism of Y, product <*Y*> such that
A1: J is bijective & (for y be Element of Y holds J.y = <*y*>) by Th1;
  defpred P[object,object,object] means $3 = [$1,<* $2 *>];
A2: for x,y be object st x in the carrier of X & y in the carrier of Y
   ex z be object st z in the carrier of [:X,product <*Y*>:] & P[x,y,z]
  proof
    let x,y be object;
    assume
A3: x in the carrier of X & y in the carrier of Y;
    then reconsider y0=y as Element of Y;
    reconsider z=[x,<*y0*>] as set by TARSKI:1;
    take z;
    J.y0 = <*y0*> by A1;
    hence thesis by A3,ZFMISC_1:87;
  end;
  consider I be Function of [:the carrier of X,the carrier of Y:],
  the carrier of [:X,product <*Y*>:] such that
A4: for x,y be object st x in the carrier of X & y in the carrier of Y holds
  P[x,y,I.(x,y)] from BINOP_1:sch 1(A2);
  reconsider I as Function of [:X,Y:],[:X,product <*Y*>:];
  for v,w be Element of [:X,Y:] holds I.(v+w) = I.v + I.w
  proof
    let v,w be Element of [:X,Y:];
    consider x1 be Element of X, x2 be Element of Y such that
A5: v=[x1,x2] by SUBSET_1:43;
    consider y1 be Element of X, y2 be Element of Y such that
A6: w=[y1,y2] by SUBSET_1:43;
A7: I.(v+w) = I.(x1+y1,x2+y2) by A5,A6,PRVECT_3:def 1
      .= [x1+y1,<*x2+y2*>] by A4;
    I.v = I.(x1,x2) & I.w = I.(y1,y2) by A5,A6;
    then
A8: I.v = [x1,<*x2*>] & I.w = [y1,<*y2*>] by A4;
A9: J.x2 = <*x2*> & J.y2 = <*y2*> by A1;
    then reconsider xx2=<*x2*> as Element of product <*Y*>;
    reconsider yy2=<*y2*> as Element of product <*Y*> by A9;
    <*x2+y2*> = J.(x2+y2) by A1
      .= xx2+yy2 by A9,VECTSP_1:def 20;
    hence I.v + I.w = I.(v+w) by A7,A8,PRVECT_3:def 1;
  end;
  then reconsider I as Homomorphism of [:X,Y:],[:X,product <*Y*>:]
  by VECTSP_1:def 20;
  take I;
  now let z1,z2 be object;
    assume
A10: z1 in the carrier of [:X,Y:] & z2 in the carrier of [:X,Y:] & I.z1 = I.z2;
    consider x1,y1 be object such that
A11: x1 in the carrier of X & y1 in the carrier of Y & z1 = [x1,y1]
    by A10,ZFMISC_1:def 2;
    consider x2,y2 be object such that
A12: x2 in the carrier of X & y2 in the carrier of Y & z2 = [x2,y2]
    by A10,ZFMISC_1:def 2;
    [x1,<*y1*>] = I.(x1,y1) by A4,A11
      .= I.(x2,y2) by A10,A11,A12
      .= [x2,<*y2*>] by A4,A12;
    then x1 = x2 & <*y1*> = <*y2*> by XTUPLE_0:1;
    hence z1 = z2 by A11,A12,FINSEQ_1:76;
  end;
  then
A13: I is one-to-one by FUNCT_2:19;
  now let w be object;
    assume w in the carrier of [:X,product <*Y*>:];
    then consider x,y1 be object such that
A14: x in the carrier of X & y1 in the carrier of product <*Y*> &
    w = [x,y1] by ZFMISC_1:def 2;
    y1 in rng J by A1,A14,FUNCT_2:def 3;
    then consider y be object such that
A15: y in the carrier of Y & y1 = J.y by FUNCT_2:11;
    reconsider z = [x,y] as Element of [:the carrier of X,the carrier of Y:]
    by A14,A15,ZFMISC_1:87;
    J.y = <*y*> by A15,A1;
    then w = I.(x,y) by A4,A14,A15;
    then w = I.z;
    hence w in rng I by FUNCT_2:4;
  end;
  then the carrier of [:X,product <*Y*>:] c= rng I by TARSKI:def 3;
  then I is onto by FUNCT_2:def 3,XBOOLE_0:def 10;
  hence I is bijective by A13;
  thus for x be Element of X, y be Element of Y holds I.(x,y) = [x,<*y*>]
  by A4;
end;

theorem
  for X be Group-Sequence, Y be AbGroup holds
  ex I be Homomorphism of [:product X,Y:],product(X^<*Y*>) st I is bijective &
  (for x be Element of product X, y be Element of Y ex x1,y1 be FinSequence
  st x = x1 & <*y*> = y1 & I.(x,y) = x1^y1)
proof
  let X be Group-Sequence;
  let Y be AbGroup;
  consider I be Homomorphism of [:product X,Y:],[:product X,product <*Y*>:]
  such that
A1: I is bijective & (for x be Element of product X, y be Element of Y holds
  I.(x,y) = [x,<*y*>]) by Th9;
  consider J be Homomorphism of [:product X,product <*Y*>:], product (X^<*Y*>)
  such that
A2: J is bijective & (for x be Element of product X,
  y be Element of product <*Y*> holds ex x1,y1 be FinSequence st x=x1 &
  y=y1 & J.(x,y) = x1^y1) by Th3;
  set K = J*I;
  reconsider K as Homomorphism of [:product X,Y:],product (X^<*Y*>);
  take K;
A3: rng J = the carrier of product (X^<*Y*>) by A2,FUNCT_2:def 3;
  rng I = the carrier of [:product X,product <*Y*>:] by A1,FUNCT_2:def 3;
  then rng(J*I) = J.:(the carrier of [:product X,product <*Y*>:])
  by RELAT_1:127
    .= the carrier of product (X^<*Y*>) by A3,RELSET_1:22;
  then K is onto by FUNCT_2:def 3;
  hence K is bijective by A1,A2;
  thus for x be Element of product X, y be Element of Y holds ex x1,y1 be
  FinSequence st x = x1 & <*y*> = y1 & K.(x,y) = x1^y1
  proof
    let x be Element of product X, y be Element of Y;
A4: I.(x,y) = [x,<*y*>] by A1;
    [x,y] in the carrier of [:product X,Y:];
    then [x,<*y*>] in the carrier of [:product X,product <*Y*>:]
    by A4,FUNCT_2:5;
    then reconsider yy=<*y*> as Element of product <*Y*> by ZFMISC_1:87;
    consider x1,y1 be FinSequence such that
A5: x = x1 & yy = y1 & J.(x,yy) = x1^y1 by A2;
    J.(x,yy) = J.(I.([x,y])) by A4
      .= K.(x,y) by FUNCT_2:15;
    hence thesis by A5;
  end;
end;

theorem Th11:
  for n be non zero Nat holds
  the addLoopStr of INT.Ring n is non empty Abelian right_complementable
  add-associative right_zeroed
proof
  let n be non zero Nat;
A1: 1 <= n by NAT_1:14;
  now per cases;
    suppose n=1;
      hence INT.Ring n is Ring by INT_3:10;
    end;
    suppose n<>1;
      then 1 < n by A1,XXREAL_0:1;
      hence INT.Ring n is Ring by INT_3:11;
    end;
  end;
  then reconsider R = INT.Ring n as Ring;
  set S = the addLoopStr of INT.Ring n;
A2: for v,w being Element of S holds v + w = w + v
  proof
    let v,w be Element of S;
    reconsider v1=v,w1=w as Element of R;
    thus v+w = v1+w1
      .= w1+v1
      .= w+v;
  end;
A3: for x being Element of S holds x is right_complementable
  proof
    let v be Element of S;
    reconsider v1=v as Element of R;
    consider w1 being Element of R such that
A4: v1 + w1 = 0.R by ALGSTR_0:def 11;
    reconsider w=w1 as Element of S;
    v+w = 0.S by A4;
    hence thesis;
  end;
A5: for u,v,w being Element of S holds (u + v) + w = u + (v + w)
  proof
    let u,v,w be Element of S;
    reconsider u1=u,v1=v,w1=w as Element of R;
    thus (u + v) + w = (u1 + v1) + w1
      .= u1 + (v1 + w1) by RLVECT_1:def 3
      .= u + (v + w);
  end;
A6: for v being Element of S holds v + (0.S) = v
  proof
    let v be Element of S;
    reconsider v1=v as Element of R;
    thus v + (0.S) = v1 + 0.R
      .= v;
  end;
  thus thesis by A2,A3,A5,A6,RLVECT_1:def 2,RLVECT_1:def 3,
  RLVECT_1:def 4;
end;

definition
  let n be natural Number;
  func Z/Z n -> addLoopStr equals
  the addLoopStr of INT.Ring n;
  coherence;
end;

registration
  let n be non zero natural Number;
  cluster Z/Z n -> non empty strict;
  coherence;
end;

registration
  let n be non zero natural Number;
  cluster Z/Z n -> Abelian right_complementable add-associative right_zeroed;
  coherence by Th11;
end;

theorem Th12:
  for X be Group-Sequence, x,y,z be Element of product X,
  x1,y1,z1 be FinSequence st x = x1 & y = y1 & z = z1 holds
  z = x+y iff for j be Element of dom carr X holds
  z1.j = (the addF of (X.j)).((x1.j),(y1.j))
proof
  let X be Group-Sequence, x,y,z be Element of product X, x1,y1,z1 be
  FinSequence;
  assume
A1: x = x1 & y = y1 & z = z1;
  hereby assume
A2: z = x+y;
    thus for j be Element of dom carr X holds z1.j = (the addF of (X.j)).
    ((x1.j),(y1.j))
    proof
      let j be Element of dom carr X;
      thus z1.j = ((addop X).j).((x1.j),(y1.j)) by A1,A2,PRVECT_1:def 8
        .= (the addF of (X.j)).((x1.j),(y1.j)) by PRVECT_1:def 12;
    end;
  end;
  assume
A3: for j be Element of dom carr X holds z1.j = (the addF of (X.j)).
  ((x1.j),(y1.j));
  reconsider Ixy = x+y as FinSequence by NDIFF_5:9;
A4: dom Ixy = dom carr X by CARD_3:9;
  for j0 being Nat st j0 in dom z1 holds z1.j0 = Ixy.j0
  proof
    let j0 be Nat;
    assume j0 in dom z1;
    then reconsider j = j0 as Element of dom carr X by CARD_3:9,A1;
    Ixy. j0 = ((addop X).j).((x1.j),(y1.j)) by A1,PRVECT_1:def 8
      .= (the addF of (X.j)).((x1.j),(y1.j)) by PRVECT_1:def 12
      .= z1.j by A3;
    hence thesis;
  end;
  hence z = x + y by A1,CARD_3:9,A4,FINSEQ_1:13;
end;

theorem Th13:
  for m being CR_Sequence, j being Nat, x be Integer st j in dom m
  holds (x mod Product(m)) mod m.j = x mod m.j
proof
  let m be CR_Sequence, j be Nat, x be Integer;
  assume
A1: j in dom m;
  consider z being Integer such that
A2: z * m.j = Product(m) by A1,INT_6:10;
  (x mod Product(m)) mod m.j = (x - (x div (z * m.j)) * (z * m.j)) mod m.j
  by A2,INT_1:def 10
    .= ((x mod m.j) - (0 + ((x div (z * m.j)) * z) * m.j mod m.j)) mod m.j
      by INT_6:7
    .= ((x mod m.j) - (0 mod m.j)) mod m.j by NAT_D:61
    .= (x - 0) mod m.j by INT_6:7
    .= x mod m.j;
  hence thesis;
end;

Lm1: for m be non zero Nat, x be Integer holds
(x mod m) in Segm m
proof
  let m be non zero Nat, x be Integer;
  x mod m >= 0 & (x mod m) < m by NAT_D:62;
  then x mod m in NAT by INT_1:3;
  hence thesis by NAT_1:44,NAT_D:62;
end;

theorem Th14:
  for m being CR_Sequence, X be Group-Sequence st len m = len X &
  (for i be Element of NAT st i in dom X holds ex mi be non zero Nat
  st mi = m.i & X.i = Z/Z (mi)) holds
  ex I being Homomorphism of Z/Z (Product(m)),product X
  st (for x be Integer st x in the carrier of Z/Z (Product(m)) holds
  I.x = mod(x,m))
proof
  let m be CR_Sequence, X be Group-Sequence;
  assume
A1: len m = len X & (for i be Element of NAT st i in dom X holds ex mi be
  non zero Nat st mi = m.i & X.i = Z/Z (mi));
  set ZZ = Z/Z (Product(m));
  reconsider CX = carr X as non-empty FinSequence;
  len (carr X) = len X by PRVECT_1:def 11;
  then
A2: dom (carr X) = Seg (len X) by FINSEQ_1:def 3
    .= dom X by FINSEQ_1:def 3;
  defpred P[object,object] means
ex x be Integer st $1 = x & $2 = mod(x,m);
A3: for x be object st x in the carrier of Z/Z (Product(m))
ex y be object st y in
  the carrier of (product X) & P[x,y]
  proof
    let x be object;
    assume x in the carrier of Z/Z (Product(m));
    then reconsider x1 = x as Integer;
A4: dom (mod(x1,m)) = Seg len (mod(x1,m)) by FINSEQ_1:def 3
      .=Seg len m by INT_6:def 3
      .=Seg len (carr X) by A1,PRVECT_1:def 11
      .=dom (carr X) by FINSEQ_1:def 3;
    now let i be object;
      assume
A5:   i in dom carr X;
      then reconsider i0 = i as Element of dom carr X;
      reconsider i1 = i as Nat by A5;
      consider mi be non zero Nat such that
A6:  mi=m.i0 & X.i0 = Z/Z (mi) by A1,A2;
      (mod(x1,m)).i = x1 mod m.i1 by A4,A5,INT_6:def 3;
      then (mod(x1,m)).i in the carrier of (X.i0) by A6,Lm1;
      hence (mod(x1,m)).i in (carr X).i by A2,PRVECT_1:def 11;
    end;
    hence thesis by CARD_3:9,A4;
  end;
  consider I being Function of the carrier of Z/Z (Product(m)),the carrier of
  (product X) such that
A7: for x be object st x in the carrier of Z/Z (Product(m)) holds P[x,I.x]
  from FUNCT_2:sch 1 (A3);
A8: for x be Integer st x in the carrier of Z/Z (Product(m))
  holds I.x = mod(x,m)
  proof
    let x be Integer;
    assume x in the carrier of Z/Z (Product(m));
    then ex x0 be Integer st x = x0 & I.x = mod(x0,m) by A7;
    hence I.x = mod(x,m);
  end;
  for v,w being Point of ZZ holds I.(v + w) = (I.v) + (I.w)
  proof
    let v,w be Point of ZZ;
    reconsider v1 = v, w1 = w, vw1 = v + w as Integer;
    reconsider Iv = I.v, Iw = I.w, Ivw = I.(v + w) as FinSequence
      by NDIFF_5:9;
A9: I.v1 = mod(v1,m) by A8;
A10: I.w1 = mod(w1,m) by A8;
A11: I.(vw1) = mod(vw1,m) by A8;
    I.v in the carrier of (product X);
    then mod(v1,m) in product (carr X) by A8;
    then
A12: dom (mod(v1,m)) = dom (carr X) by CARD_3:9;
    I.w in the carrier of (product X);
    then mod(w1,m) in product (carr X) by A8;
    then
A13: dom (mod(w1,m)) = dom (carr X) by CARD_3:9;
    I.(v+w) in the carrier of (product X);
    then mod(vw1,m) in product (carr X) by A8;
    then
A14: dom (mod(vw1,m)) = dom (carr X) by CARD_3:9;
    now let j be Element of dom (carr X);
      reconsider j0=j as Nat;
      consider mj be non zero Nat such that
A15:   mj = m.j0 & X.j0 = Z/Z (mj) by A2,A1;
A16:   dom m = Seg (len X) by A1,FINSEQ_1:def 3
        .= dom X by FINSEQ_1:def 3;
A17:   (v1 mod m.j0) in Segm mj & (w1 mod m.j0) in Segm mj by Lm1,A15;
A18:  Iw.j0 = w1 mod m.j0 by A13,A10,INT_6:def 3;
A19:  Ivw.j0 = vw1 mod m.j0 by A14,A11,INT_6:def 3;
      thus Ivw.j
        = ((v1+w1) mod Product(m)) mod m.j0 by GR_CY_1:def 4,A19
       .= ((v1+w1)) mod m.j0 by A2,A16,Th13
       .= ((v1 mod m.j0) +(w1 mod m.j0)) mod m.j0 by NAT_D:66
       .= (addint(mj)).((v1 mod m.j0),(w1 mod m.j0)) by A17,A15,GR_CY_1:def 4
       .= (the addF of (X.j)).((Iv.j),(Iw.j)) by A12,A9,INT_6:def 3,A18,A15;
    end;
    hence I.(v + w) = (I.v) + (I.w) by Th12;
  end;
  then reconsider I as Homomorphism of Z/Z (Product(m)),product X
  by VECTSP_1:def 20;
  take I;
  thus thesis by A8;
end;

theorem Th15:
  for X,Y be non empty set ex I be Function of [:X,Y:],[:X,product<*Y*>:]
  st I is one-to-one onto &
  (for x,y be set st x in X & y in Y holds I.(x,y) = [x,<*y*>])
proof
  let X,Y be non empty set;
A1: product <*Y*> <> {}
  proof
    assume product <*Y*> = {};
    then {} in rng <*Y*> by CARD_3:26;
    then {} in { Y } by FINSEQ_1:39;
    hence contradiction by TARSKI:def 1;
  end;
  consider J be Function of Y,product <*Y*> such that
A2: J is one-to-one & J is onto &
(for y be object st y in Y holds J.y = <*y*>)
  by PRVECT_3:4;
  defpred P[object,object,object] means $3 = [$1,<* $2 *>];
A3: for x,y be object st x in X & y in Y
   ex z be object st z in [:X,product <*Y*>:]
  & P[x,y,z]
  proof
    let x,y be object;
    assume
A4: x in X & y in Y;
    reconsider z = [x,<*y*>] as set by TARSKI:1;
    take z;
    J.y = <* y *> by A2,A4;
    then <* y *> in product <*Y*> by A4,A1,FUNCT_2:5;
    hence thesis by A4,ZFMISC_1:87;
  end;
  consider I be Function of [:X,Y:],[:X,product <*Y*>:] such that
A5: for x,y be object st x in X & y in Y holds P[x,y,I.(x,y)]
  from BINOP_1:sch 1(A3);
  reconsider I as Function of [:X,Y:],[:X,product <*Y*>:];
  take I;
  thus I is one-to-one
  proof
    now let z1,z2 be object;
      assume
A6:   z1 in [:X,Y:] & z2 in [:X,Y:] & I.z1 = I.z2;
      then consider x1,y1 be object such that
A7:   x1 in X & y1 in Y & z1 = [x1,y1] by ZFMISC_1:def 2;
      consider x2,y2 be object such that
A8:   x2 in X & y2 in Y & z2 = [x2,y2] by A6,ZFMISC_1:def 2;
A9:   [x1,<*y1*>] = I.(x1,y1) by A5,A7
        .= I.(x2,y2) by A6,A7,A8
        .= [x2,<*y2*>] by A5,A8;
      then <*y1*> = <*y2*> by XTUPLE_0:1;
      then y1 = y2 by FINSEQ_1:76;
      hence z1 = z2 by A7,A8,A9,XTUPLE_0:1;
    end;
    hence thesis by FUNCT_2:19,A1;
  end;
  thus I is onto
  proof
    now let w be object;
      assume w in [:X, product <*Y*>:];
      then consider x,y1 be object such that
A10:   x in X & y1 in product <*Y*> & w = [x,y1] by ZFMISC_1:def 2;
      y1 in rng J by A2,A10,FUNCT_2:def 3;
      then consider y be object such that
A11:  y in Y & y1 = J.y by FUNCT_2:11;
A12:  J.y = <*y*> by A11,A2;
      reconsider z = [x,y] as Element of [:X,Y:] by A10,A11,ZFMISC_1:87;
      w = I.(x,y) by A5,A10,A11,A12
        .= I.z;
      hence w in rng I by FUNCT_2:4,A1;
    end;
    then [:X,product <*Y*>:] c= rng I by TARSKI:def 3;
    hence thesis by FUNCT_2:def 3,XBOOLE_0:def 10;
  end;
  thus for x,y be set st x in X & y in Y holds I.(x,y) = [x,<*y*>] by A5;
end;

theorem Th16:
  for X be non empty set holds card(product <*X*>) = card X
proof
  let X be non empty set;
  consider I be Function of X,product <*X*> such that
A1: I is one-to-one & I is onto &
 for x be object st x in X holds I.x = <*x*>
  by PRVECT_3:4;
  not {} in rng <*X*>
  proof
    assume not not {} in rng <*X*>;
    then {} in { X } by FINSEQ_1:39;
    hence contradiction by TARSKI:def 1;
  end;
  then product (<*X*>) <> {} by CARD_3:26;
  then
A2: dom I = X by FUNCT_2:def 1;
  rng I = product (<*X*>) by A1,FUNCT_2:def 3;
  hence card(X) = card(product(<*X*>)) by CARD_1:5,A1,A2,WELLORD2:def 4;
end;

theorem Th17:
  for X be non-empty non empty FinSequence, Y be non empty set
  ex I be Function of [:product X,Y:],product(X^<*Y*>)
  st I is one-to-one onto &
  (for x,y be set st x in product X & y in Y ex x1,y1 be FinSequence
  st x = x1 & <*y*> = y1 & I.(x,y) = x1^y1)
proof
  let X be non-empty non empty FinSequence, Y be non empty set;
A1: product <*Y*> <> {}
  proof
    assume product <*Y*> = {};
    then {} in rng <*Y*> by CARD_3:26;
    then {} in { Y } by FINSEQ_1:39;
    hence contradiction by TARSKI:def 1;
  end;
  consider I be Function of [:product X,Y:],[:product X,product <*Y*>:]
  such that
A2: I is one-to-one & I is onto & (for x,y be set st x in product X & y in Y
  holds I.(x,y) = [x,<*y*>]) by Th15;
  <*Y*> is non-empty
  proof
    assume not (<*Y*> is non-empty);
    then {} in rng <*Y*> by RELAT_1:def 9;
    then {} in {Y} by FINSEQ_1:39;
    hence contradiction by TARSKI:def 1;
  end;
  then reconsider YY=<*Y*> as non-empty non empty FinSequence;
  consider J be Function of [:product X,product YY:],product(X^YY)
  such that
A3: J is one-to-one & J is onto & (for x,y be FinSequence st x in product X &
  y in product YY holds J.(x,y) = x^y) by PRVECT_3:6;
  set K = J*I;
  reconsider K as Function of [:product X,Y:],product (X^<*Y*>);
  take K;
  thus K is one-to-one by A2,A3;
A4: rng J = product (X^<*Y*>) by A3,FUNCT_2:def 3;
  rng I = [:product X,product<*Y*>:] by A2,FUNCT_2:def 3;
  then rng(J * I) = J.:([:product X,product <*Y*>:]) by RELAT_1:127
    .= product (X^<*Y*>) by A4,RELSET_1:22;
  hence K is onto by FUNCT_2:def 3;
  thus for x,y be set st x in product X & y in Y ex x1,y1 be FinSequence st
  x = x1 & <*y*> =y1 & K.(x,y) = x1^y1
  proof
    let x,y be set;
    assume
A5: x in product X & y in Y;
    then
A6: I.(x,y) = [x,<*y*>] by A2;
A7: [x,y] in [: product X,Y:] by A5,ZFMISC_1:87;
    then [x,<*y*>] in [:product X,product <*Y*>:] by A6,A1,FUNCT_2:5;
    then
A8: <*y*> in product <*Y*> by ZFMISC_1:87;
    reconsider xx=x as Function by A5;
    dom xx = dom X by CARD_3:9,A5
      .=Seg (len X) by FINSEQ_1:def 3;
    then reconsider x1=xx as FinSequence by FINSEQ_1:def 2;
    set y1 = <*y*>;
A9: J.(x,<*y*>) = x1^y1 by A3,A5,A8;
    J.(x,<*y*>) = K.(x,y) by A6,A7,FUNCT_2:15;
    hence thesis by A9;
  end;
end;

theorem Th18:
  for m being FinSequence of NAT, X being non-empty non empty FinSequence
  st len m = len X &
  (for i be Element of NAT st i in dom X holds card(X.i) = m.i) holds
  card(product X) = Product(m)
proof
  defpred P[Nat] means for m being FinSequence of NAT, X be non-empty non empty
  FinSequence st len m = $1 & len m = len X & (for i be Element of NAT st i in
  dom X holds card(X.i) = m.i) holds card(product X) = Product(m);
A1: P[0];
A2: for n be Nat st P[n] holds P[n+1]
  proof
    let n be Nat;
    assume
A3: P[n];
    now let m be FinSequence of NAT, X be non-empty non empty FinSequence;
      assume
A4:  len m = n + 1 & len m = len X & (for i be Element of NAT st i in dom X
      holds card(X.i) = m.i);
      now per cases;
        suppose
A5:       n = 0;
A6:       m = <*m.1*> by A5,FINSEQ_1:40,A4;
A7:       X = <*X.1*> by A5,FINSEQ_1:40,A4;
          n+1 in Seg (n+1) by FINSEQ_1:4;
          then
A8:       1 in dom X by A5,FINSEQ_1:def 3,A4;
          thus card(product X) = card (X.1) by Th16,A7,A8
            .= m.1 by A8,A4
            .= Product(m) by A6,RVSUM_1:95;
        end;
        suppose
A9:       n <> 0;
          set X1 = X | n;
          reconsider m1 = m | n as FinSequence of NAT;
A10:       len m1 = n by NAT_1:11,A4,FINSEQ_1:59;
A11:       len X1 = n by NAT_1:11,A4,FINSEQ_1:59;
A12:       dom X1 = Seg (len X1) by FINSEQ_1:def 3
            .= Seg n by NAT_1:11,A4,FINSEQ_1:59;
A13:       dom m1 = Seg (len m1) by FINSEQ_1:def 3
            .= Seg n by NAT_1:11,A4,FINSEQ_1:59;
          X1 is non-empty
          proof
            assume not X1 is non-empty;
            then
A14:        {} in rng X1 by RELAT_1:def 9;
            rng X1 c= rng X by RELAT_1:70;
            hence contradiction by A14;
          end;
          then reconsider X1 as non-empty non empty FinSequence by A9;
          now let i be Element of NAT;
            assume
A15:        i in dom X1;
            Seg n c= Seg (n+1) by NAT_1:11,FINSEQ_1:5;
            then i in Seg (len X) by A4,A12,A15;
            then
A16:        i in dom X by FINSEQ_1:def 3;
            thus card(X1.i) = card(X.i) by FUNCT_1:47,A15
              .= m.i by A4,A16
              .= m1.i by FUNCT_1:47,A15,A13,A12;
          end;
          then
A17:      card(product X1) = Product m1 by A3,A10,A11;
A18:      n < len X by NAT_1:19,A4;
A19:      X is FinSequence of (rng X) by FINSEQ_1:def 4;
A20:      X = X| (n + 1) by FINSEQ_1:58,A4
            .= X1^(<*X.(len X) *>) by A18,FINSEQ_5:83,A4;
A21:      n < len m by NAT_1:19,A4;
A22:      m = m| (n+1) by FINSEQ_1:58,A4
            .= m1^(<*m.(len m) *>) by A21,FINSEQ_5:83,A4;
          len X in Seg (len X) by A4,FINSEQ_1:4;
          then
A23:      len X in dom X by FINSEQ_1:def 3;
          then
A24:      card(X.(len X)) = m.(len m) by A4;
          consider I be Function of [:product X1,(X.(len X)):],
          product(X1^<*(X.(len X))*>) such that
A25:      I is one-to-one & I is onto & (for x,y be set st x in product X1 &
          y in (X.(len X))
          ex x1,y1 be FinSequence st x = x1 & <*y*> = y1 & I.(x,y) = x1^y1)
          by A23,Th17;
          not {} in rng (X1^<*(X.(len X))*>)
          proof
            assume not not {} in rng (X1^<*(X.(len X))*>);
            then {} in ( rng X1 \/ rng <*(X.(len X))*>) by FINSEQ_1:31;
            then {} in rng X1 or {} in rng <*(X.(len X))*> by XBOOLE_0:def 3;
            then not X1 is non-empty or {} in { X.(len X) }
            by FINSEQ_1:39;
            hence contradiction by TARSKI:def 1,A23;
          end;
          then product(X1^<*(X.(len X))*>) <> {} by CARD_3:26;
          then
A26:      dom I = [:product X1,(X.(len X)):] by FUNCT_2:def 1;
          rng I = product(X1^<*(X.(len X))*>) by A25,FUNCT_2:def 3;
          then
A27:      card([:product X1,(X.(len X)):]) = card(product(X1^<*(X.(len X))*>))
          by CARD_1:5,A25,A26,WELLORD2:def 4;
A28:      card(product X) = card(product <*(product X1),(X.(len X))*>)
          by CARD_1:5,A20,A27,TOPGEN_5:8;
A29:      product X1 is finite set & X.(len X) is finite set by A24,A17;
          card(product <*(product X1),(X.(len X))*>) =
          card([:product X1,(X.(len X)):]) by CARD_1:5,TOPGEN_5:8
            .= (Product m1) * (m.(len m)) by A24,A17,A29,CARD_2:46;
          hence card (product X) = Product(m) by RVSUM_1:96,A22,A28;
        end;
      end;
      hence card (product X) = Product(m);
    end;
    hence P[n+1];
  end;
  for n be Nat holds P[n] from NAT_1:sch 2(A1,A2);
  hence thesis;
end;

theorem Th19:
  for m being CR_Sequence, X be Group-Sequence st len m = len X &
  (for i be Element of NAT st i in dom X holds ex mi be non zero Nat
  st mi = m.i & X.i = Z/Z (mi)) holds
  card(the carrier of product X) = Product(m)
proof
  let m be CR_Sequence, X be Group-Sequence;
  assume
A1: len m = len X & (for i be Element of NAT st i in dom X holds ex mi be
  non zero Nat st mi=m.i & X.i = Z/Z (mi));
A2: dom (carr X) = Seg (len (carr X)) by FINSEQ_1:def 3
    .=Seg (len X) by PRVECT_1:def 11
    .= dom X by FINSEQ_1:def 3;
A3: dom X = Seg (len X) by FINSEQ_1:def 3
    .= dom m by FINSEQ_1:def 3,A1;
A4: for i be Element of NAT st i in dom (carr X) holds card((carr X).i) = m.i
  proof
    let i be Element of NAT;
    assume
A5: i in dom (carr X);
    reconsider i0=i as Element of dom X by A2,A5;
    consider mi be non zero Nat such that
A6: mi = m.i & X.i = Z/Z (mi) by A2,A5,A1;
    thus card((carr X).i) = card(the carrier of (X.i0)) by PRVECT_1:def 11
      .=m.i by A6;
  end;
A7: len carr X = len m by A1,PRVECT_1:def 11;
  now let i be Nat;
    assume i in dom m;
    then ex mi be non zero Nat st mi = m.i & X.i = Z/Z (mi)
    by A3,A1;
    hence m.i in NAT by ORDINAL1:def 12;
  end;
  then m is FinSequence of NAT by FINSEQ_2:12;
  hence thesis by A4,A7,Th18;
end;

theorem Th20:
  for m being CR_Sequence, X be Group-Sequence,
  I be Function of Z/Z (Product(m)),product X st len m = len X &
  (for i be Element of NAT st i in dom X holds ex mi be non zero Nat
  st mi = m.i & X.i = Z/Z (mi)) &
  (for x be Integer st x in the carrier of Z/Z (Product(m)) holds
  I.x = mod(x,m)) holds
  I is one-to-one
proof
  let m be CR_Sequence, X be Group-Sequence, I be Function of
   Z/Z (Product(m)),product X;
  assume
A1: len m = len X & (for i be Element of NAT st i in dom X holds ex mi be
  non zero Nat st mi=m.i & X.i = Z/Z (mi)) & (for x be Integer st
  x in the carrier of Z/Z (Product(m)) holds I.x = mod(x,m));
  for x1,x2 be object
st x1 in the carrier of Z/Z (Product(m)) & x2 in the carrier
  of Z/Z (Product(m)) & I.x1 = I.x2 holds x1 = x2
  proof
    let x1,x2 be object;
    assume
A2: x1 in the carrier of Z/Z (Product(m)) & x2 in the carrier of
    Z/Z (Product(m)) & I.x1 = I.x2;
   then reconsider xx1 = x1,xx2 = x2 as Integer;
A3: 0<=xx1 & xx1 < Product(m) by A2,NAT_1:44;
A4: 0<=xx2 & xx2 < Product(m) by A2,NAT_1:44;
A5: I.x2 = mod(xx2,m) by A1,A2;
   reconsider I0 = 0 as Integer;
   reconsider u = {} as INT-valued FinSequence;
A6: dom (mod(xx1,m)) = Seg len (mod(xx1,m)) by FINSEQ_1:def 3
     .=Seg len m by INT_6:def 3
     .=dom m by FINSEQ_1:def 3;
A7: now let i be Nat;
      assume
A8:  i in dom m;
A9:   i in dom (mod(xx2,m)) by A5,A6,A1,A2,A8;
      m.i in rng m by FUNCT_1:3,A8;
      then
A10:   m.i > 0 by PARTFUN3:def 1;
A11:   xx1 mod (m.i) = (mod(xx1,m)).i by A6,A8,INT_6:def 3
        .= (mod(xx2,m)).i by A1,A2,A5
        .= xx2 mod (m .i) by A9,INT_6:def 3;
      then
A12:  (m.i) divides ((xx1 - xx2) - I0) by INT_1:def 4,NAT_D:64,A10;
A13:  (m . i) divides ((xx2 - xx1) - I0) by INT_1:def 4,NAT_D:64,A10,A11;
      u.i = I0;
      hence (xx1 - xx2),u.i are_congruent_mod (m.i) & (xx2 - xx1),u.i
      are_congruent_mod (m.i) by A12,A13,INT_1:def 4;
    end;
A14: for i being Nat st i in dom m holds I0,u.i
  are_congruent_mod (m.i)
  proof
    let i be Nat;
    assume i in dom m;
A15: u.i = I0;
    I0 - I0 = (I0 - I0) * (m.i);
    hence I0,u.i are_congruent_mod (m.i) by A15,INT_1:def 4,INT_1:def 3;
  end;
A16: xx1 mod Product(m) >=0 & xx1 mod Product(m) < Product(m) by NAT_D:62;
A17: xx2 mod Product(m) >=0 & xx2 mod Product(m) < Product(m) by NAT_D:62;
A18: xx1 mod Product(m) = xx1 by A3,NAT_D:63;
A19: xx2 mod Product(m) = xx2 by A4,NAT_D:63;
  per cases;
    suppose xx2 <= xx1;
      then
A20:  xx1-xx2 in NAT by INT_1:5;
      xx1-xx2 <= xx1 mod Product(m) by A18,XREAL_1:43,A2;
      then xx1-xx2 - Product(m) < xx1 mod Product(m) - (xx1 mod Product(m))
      by A16,XREAL_1:15;
      then
A21:   xx1-xx2 < xx1-xx2 - (xx1-xx2 - Product(m)) by XREAL_1:46;
      for i being Nat st i in dom m holds (xx1 - xx2),u.i
      are_congruent_mod (m.i) by A7;
      then xx1 - xx2 = I0 by INT_6:42,A14,A20,A21;
      hence x1 = x2;
    end;
    suppose not xx2 <= xx1;
      then
A22:  xx2-xx1 in NAT by INT_1:5;
      xx2-xx1 <= xx2 mod Product(m) by A19,XREAL_1:43,A2;
      then xx2-xx1 - Product(m) < xx2 mod Product(m) - (xx2 mod Product(m))
      by A17,XREAL_1:15;
      then
A23:  xx2-xx1 < xx2-xx1 - (xx2-xx1 - Product(m)) by XREAL_1:46;
      for i being Nat st i in dom m holds (xx2 - xx1),u.i
      are_congruent_mod (m.i) by A7;
      then xx2 - xx1 =I0 by INT_6:42,A14,A22,A23;
      hence x1 = x2;
    end;
  end;
  hence I is one-to-one by FUNCT_2:19;
end;

theorem
  for m being CR_Sequence, X be Group-Sequence st len m = len X &
  (for i be Element of NAT st i in dom X holds ex mi be non zero Nat
  st mi = m.i & X.i = Z/Z (mi)) holds
  ex I being Homomorphism of Z/Z (Product(m)),product X st I is bijective &
  (for x be Integer st x in the carrier of Z/Z (Product(m)) holds
  I.x = mod(x,m))
proof
  let m be CR_Sequence, X be Group-Sequence;
  assume
A1: len m = len X & (for i be Element of NAT st i in dom X holds ex mi be
  non zero Nat st mi = m.i & X.i = Z/Z (mi));
  then consider I be Homomorphism of Z/Z (Product(m)),product X such that
A2: (for x be Integer st x in the carrier of Z/Z (Product(m)) holds I.x =
  mod(x,m)) by Th14;
A3: I is one-to-one by A1,Th20,A2;
  Product(m) is Nat by TARSKI:1; then
A4: card(Segm Product(m)) = Product(m);
A5: card(the carrier of product X) = Product(m) by A1,Th19;
  then the carrier of product X is finite;
  then I is onto by A3,A4,A5,FINSEQ_4:63;
  hence thesis by A2,A3;
end;

{"subset_name": "curated", "file": "formal/mizar/group_14.miz"}