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

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