let u be Integer; :: thesis: for m being CR_Sequence
for i being natural number st i in dom m holds
u,(mod u,m) . i are_congruent_mod m . i
let m be CR_Sequence; :: thesis: for i being natural number st i in dom m holds
u,(mod u,m) . i are_congruent_mod m . i
let i be natural number ; :: thesis: ( i in dom m implies u,(mod u,m) . i are_congruent_mod m . i )
assume AS: i in dom m ; :: thesis: u,(mod u,m) . i are_congruent_mod m . i
then m . i in rng m by FUNCT_1:12;
then D1: m . i > 0 by PARTFUN3:def 1;
A: ( len (mod u,m) = len m & ( for i being Element of NAT st i in dom (mod u,m) holds
(mod u,m) . i = u mod (m . i) ) ) by Df1;
dom (mod u,m) = Seg (len (mod u,m)) by FINSEQ_1:def 3
.= dom m by A, FINSEQ_1:def 3 ;
then D: (mod u,m) . i = u mod (m . i) by Df1, AS;
u mod (m . i) = u - ((u div (m . i)) * (m . i)) by D1, INT_1:def 8;
then u - (u mod (m . i)) = (u div (m . i)) * (m . i) ;
hence u,(mod u,m) . i are_congruent_mod m . i by D, INT_1:def 3; :: thesis: verum