let u be Integer; :: thesis: for m being CR_Sequence
for i being Nat 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 Nat st i in dom m holds
u,(mod (u,m)) . i are_congruent_mod m . i
let i be Nat; :: thesis: ( i in dom m implies u,(mod (u,m)) . i are_congruent_mod m . i )
A1: len (mod (u,m)) = len m by Def3;
assume A2: i in dom m ; :: thesis: u,(mod (u,m)) . i are_congruent_mod m . i
then m . i in rng m by FUNCT_1:3;
then m . i > 0 by PARTFUN3:def 1;
then u mod (m . i) = u - ((u div (m . i)) * (m . i)) by INT_1:def 10;
then A3: u - (u mod (m . i)) = (u div (m . i)) * (m . i) ;
dom (mod (u,m)) = Seg (len (mod (u,m))) by FINSEQ_1:def 3
.= dom m by A1, FINSEQ_1:def 3 ;
then (mod (u,m)) . i = u mod (m . i) by A2, Def3;
hence u,(mod (u,m)) . i are_congruent_mod m . i by A3, INT_1:def 5; :: thesis: verum