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₁[ 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₁[x,y] )

proof

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₁[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₁[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 ;

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

hence ex y being object st
( y in the carrier of (product X) & S₁[x,y] ) by CARD_3:9, A4; :: thesis: verum

end;

consider I being Function of the carrier of (Z/Z (Product m)), the carrier of (product X) such that
A7: for x being object st x in the carrier of (Z/Z (Product m)) holds
S₁[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)

proof

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;

for v, w being Point of (Z/Z (Product m)) holds I . (v + w) = (I . v) + (I . w)

proof

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;

now :: thesis: for j being Element of dom (carr X) holds Ivw . j = the addF of (X . j) . ((Iv . j),(Iw . j))

let 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;

hence I . (v + w) = (I . v) + (I . w) by Th12; :: thesis: verum

end;

then reconsider I = I as Homomorphism of (Z/Z (Product m)),(product X) by VECTSP_1:def 20;
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