let m be CR_Sequence; :: thesis: for X being Group-Sequence st len m = len X & ( for i being Element of NAT st i in dom X holds

ex mi being 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 being Integer st x in the carrier of (Z/Z (Product m)) holds

I . x = mod (x,m)

let X be Group-Sequence; :: thesis: ( len m = len X & ( for i being Element of NAT st i in dom X holds

ex mi being non zero Nat st

( mi = m . i & X . i = Z/Z mi ) ) implies ex I being Homomorphism of (Z/Z (Product m)),(product X) st

for x being Integer st x in the carrier of (Z/Z (Product m)) holds

I . x = mod (x,m) )

assume A1: ( len m = len X & ( for i being Element of NAT st i in dom X holds

ex mi being non zero Nat st

( mi = m . i & X . i = Z/Z mi ) ) ) ; :: thesis: ex I being Homomorphism of (Z/Z (Product m)),(product X) st

for x being Integer st x in the carrier of (Z/Z (Product m)) holds

I . x = mod (x,m)

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 S_{1}[ object , object ] means ex x being Integer st

( $1 = x & $2 = mod (x,m) );

A3: for x being object st x in the carrier of (Z/Z (Product m)) holds

ex y being object st

( y in the carrier of (product X) & S_{1}[x,y] )

A7: for x being object st x in the carrier of (Z/Z (Product m)) holds

S_{1}[x,I . x]
from FUNCT_2:sch 1(A3);

A8: for x being Integer st x in the carrier of (Z/Z (Product m)) holds

I . x = mod (x,m)

take I ; :: thesis: for x being Integer st x in the carrier of (Z/Z (Product m)) holds

I . x = mod (x,m)

thus for x being Integer st x in the carrier of (Z/Z (Product m)) holds

I . x = mod (x,m) by A8; :: thesis: verum

ex mi being 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 being Integer st x in the carrier of (Z/Z (Product m)) holds

I . x = mod (x,m)

let X be Group-Sequence; :: thesis: ( len m = len X & ( for i being Element of NAT st i in dom X holds

ex mi being non zero Nat st

( mi = m . i & X . i = Z/Z mi ) ) implies ex I being Homomorphism of (Z/Z (Product m)),(product X) st

for x being Integer st x in the carrier of (Z/Z (Product m)) holds

I . x = mod (x,m) )

assume A1: ( len m = len X & ( for i being Element of NAT st i in dom X holds

ex mi being non zero Nat st

( mi = m . i & X . i = Z/Z mi ) ) ) ; :: thesis: ex I being Homomorphism of (Z/Z (Product m)),(product X) st

for x being Integer st x in the carrier of (Z/Z (Product m)) holds

I . x = mod (x,m)

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 S

( $1 = x & $2 = mod (x,m) );

A3: for x being object st x in the carrier of (Z/Z (Product m)) holds

ex y being object st

( y in the carrier of (product X) & S

proof

consider I being Function of the carrier of (Z/Z (Product m)), the carrier of (product X) such that
let x be object ; :: thesis: ( x in the carrier of (Z/Z (Product m)) implies ex y being object st

( y in the carrier of (product X) & S_{1}[x,y] ) )

assume x in the carrier of (Z/Z (Product m)) ; :: thesis: ex y being object st

( y in the carrier of (product X) & S_{1}[x,y] )

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 ;

( y in the carrier of (product X) & S_{1}[x,y] )
by CARD_3:9, A4; :: thesis: verum

end;( y in the carrier of (product X) & S

assume x in the carrier of (Z/Z (Product m)) ; :: thesis: ex y being object st

( y in the carrier of (product X) & S

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 :: thesis: for i being object st i in dom (carr X) holds

(mod (x1,m)) . i in (carr X) . i

hence
ex y being object st (mod (x1,m)) . i in (carr X) . i

let i be object ; :: thesis: ( i in dom (carr X) implies (mod (x1,m)) . i in (carr X) . i )

assume A5: i in dom (carr X) ; :: thesis: (mod (x1,m)) . i in (carr X) . i

then reconsider i0 = i as Element of dom (carr X) ;

reconsider i1 = i as Nat by A5;

consider mi being 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; :: thesis: verum

end;assume A5: i in dom (carr X) ; :: thesis: (mod (x1,m)) . i in (carr X) . i

then reconsider i0 = i as Element of dom (carr X) ;

reconsider i1 = i as Nat by A5;

consider mi being 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; :: thesis: verum

( y in the carrier of (product X) & S

A7: for x being object st x in the carrier of (Z/Z (Product m)) holds

S

A8: for x being Integer st x in the carrier of (Z/Z (Product m)) holds

I . x = mod (x,m)

proof

for v, w being Point of (Z/Z (Product m)) holds I . (v + w) = (I . v) + (I . w)
let x be Integer; :: thesis: ( x in the carrier of (Z/Z (Product m)) implies I . x = mod (x,m) )

assume x in the carrier of (Z/Z (Product m)) ; :: thesis: I . x = mod (x,m)

then ex x0 being Integer st

( x = x0 & I . x = mod (x0,m) ) by A7;

hence I . x = mod (x,m) ; :: thesis: verum

end;assume x in the carrier of (Z/Z (Product m)) ; :: thesis: I . x = mod (x,m)

then ex x0 being Integer st

( x = x0 & I . x = mod (x0,m) ) by A7;

hence I . x = mod (x,m) ; :: thesis: verum

proof

then reconsider I = I as Homomorphism of (Z/Z (Product m)),(product X) by VECTSP_1:def 20;
let v, w be Point of (Z/Z (Product m)); :: thesis: I . (v + w) = (I . v) + (I . w)

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;

end;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 :: thesis: for j being Element of dom (carr X) holds Ivw . j = the addF of (X . j) . ((Iv . j),(Iw . j))

hence
I . (v + w) = (I . v) + (I . w)
by Th12; :: thesis: verumlet j be Element of dom (carr X); :: thesis: Ivw . j = the addF of (X . j) . ((Iv . j),(Iw . j))

reconsider j0 = j as Nat ;

consider mj being 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 ; :: thesis: verum

end;reconsider j0 = j as Nat ;

consider mj being 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 ; :: thesis: verum

take I ; :: thesis: for x being Integer st x in the carrier of (Z/Z (Product m)) holds

I . x = mod (x,m)

thus for x being Integer st x in the carrier of (Z/Z (Product m)) holds

I . x = mod (x,m) by A8; :: thesis: verum