let n be Nat; :: thesis: for i being Integer holds <*i*> mod n = <*(i mod n)*>
let i be Integer; :: thesis: <*i*> mod n = <*(i mod n)*>
set f = <*i*>;
set p = <*i*> mod n;
dom (<*i*> mod n) = dom <*i*> by EULER_2:def 1;
then len (<*i*> mod n) = len <*i*> by FINSEQ_3:29;
then A1: len (<*i*> mod n) = 1 by FINSEQ_1:40;
A2: dom <*i*> = {1} by FINSEQ_1:2, FINSEQ_1:def 8;
1 in {1} by TARSKI:def 1;
then (<*i*> mod n) . 1 = (<*i*> . 1) mod n by A2, EULER_2:def 1
.= i mod n ;
hence <*i*> mod n = <*(i mod n)*> by A1, FINSEQ_1:40; :: thesis: verum