group_14.miz



    begin

    registration

      let G be Abelian add-associative right_zeroed right_complementable non empty addLoopStr;

      cluster <*G*> -> non empty AbGroup-yielding;

      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, FINSEQ_1: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;

      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, FINSEQ_1: 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 :: GROUP_14:1

    

     Th1: for X be AbGroup holds ex I be 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, FINSEQ_1: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, FINSEQ_1: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 :: GROUP_14:2

    

     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, FINSEQ_1:def 3;

      ( len <*X, Y*>) = 2 by FINSEQ_1: 44;

      then

       A4: ( dom <*X, Y*>) = {1, 2} by FINSEQ_1: 2, FINSEQ_1: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 :: GROUP_14:3

    

     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 :: GROUP_14:4

    

     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 :: GROUP_14:5

    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 :: GROUP_14:6

    

     Th6: for G,H,I be AddGroup, h be Homomorphism of G, H holds for h1 be 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;

      :: original: *

      redefine

      func h1 * h -> Homomorphism of G, I ;

      coherence by Th6;

    end

    theorem :: GROUP_14:7

    

     Th7: for G,H be AddGroup, h be 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 :: GROUP_14:8

    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;

         <*x, y*> is Element of ( product <*PX, PY*>) by Th4;

        then (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 :: GROUP_14:9

    

     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 holds 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 :: GROUP_14:10

    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 holds 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 :: GROUP_14:11

    

     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 be 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 be Element of S holds x is right_complementable

      proof

        let v be Element of S;

        reconsider v1 = v as Element of R;

        consider w1 be 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 be 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 be 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;

      :: GROUP_14:def1

      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 :: GROUP_14:12

    

     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 be 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 :: GROUP_14:13

    

     Th13: for m be CR_Sequence, j be 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 be 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 :: GROUP_14:14

    

     Th14: for m be 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 be 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)) holds 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 be 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 be 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 :: GROUP_14:15

    

     Th15: for X,Y be non empty set holds 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 holds 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 :: GROUP_14:16

    

     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 :: GROUP_14:17

    

     Th17: for X be non-empty non empty FinSequence, Y be non empty set holds 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 holds 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 holds 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 :: GROUP_14:18

    

     Th18: for m be FinSequence of NAT , X be 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 be 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)) holds 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 :: GROUP_14:19

    

     Th19: for m be 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 :: GROUP_14:20

    

     Th20: for m be 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 be 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 be 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 be 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 :: GROUP_14:21

    for m be 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 be 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;