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 ()),() st
for x being Integer st x in the carrier of (Z/Z ()) 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 ()),() st
for x being Integer st x in the carrier of (Z/Z ()) 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 ()),() st
for x being Integer st x in the carrier of (Z/Z ()) holds
I . x = mod (x,m)

set ZZ = Z/Z ();
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 S1[ 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 ()) holds
ex y being object st
( y in the carrier of () & S1[x,y] )
proof
let x be object ; :: thesis: ( x in the carrier of (Z/Z ()) implies ex y being object st
( y in the carrier of () & S1[x,y] ) )

assume x in the carrier of (Z/Z ()) ; :: thesis: ex y being object st
( y in the carrier of () & S1[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
.= 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 ;
then (mod (x1,m)) . i in the carrier of (X . i0) by ;
hence (mod (x1,m)) . i in (carr X) . i by ; :: thesis: verum
end;
hence ex y being object st
( y in the carrier of () & S1[x,y] ) by ; :: thesis: verum
end;
consider I being Function of the carrier of (Z/Z ()), the carrier of () such that
A7: for x being object st x in the carrier of (Z/Z ()) holds
S1[x,I . x] from A8: for x being Integer st x in the carrier of (Z/Z ()) holds
I . x = mod (x,m)
proof
let x be Integer; :: thesis: ( x in the carrier of (Z/Z ()) implies I . x = mod (x,m) )
assume x in the carrier of (Z/Z ()) ; :: 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 ()) holds I . (v + w) = (I . v) + (I . w)
proof
let v, w be Point of (Z/Z ()); :: 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 () ;
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 () ;
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 () ;
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
.= dom X by FINSEQ_1:def 3 ;
A17: ( v1 mod (m . j0) in Segm mj & w1 mod (m . j0) in Segm mj ) by ;
A18: Iw . j0 = w1 mod (m . j0) by ;
A19: Ivw . j0 = vw1 mod (m . j0) by ;
thus Ivw . j = ((v1 + w1) mod ()) mod (m . j0) by
.= (v1 + w1) mod (m . j0) by
.= ((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
.= the addF of (X . j) . ((Iv . j),(Iw . j)) by ; :: 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 ()),() by VECTSP_1:def 20;
take I ; :: thesis: for x being Integer st x in the carrier of (Z/Z ()) holds
I . x = mod (x,m)

thus for x being Integer st x in the carrier of (Z/Z ()) holds
I . x = mod (x,m) by A8; :: thesis: verum