let n be Nat; :: thesis: ( n <> 0 implies for f being integer-valued FinSequence holds Sum f, Sum (f mod n) are_congruent_mod n )
assume A1: n <> 0 ; :: thesis: for f being integer-valued FinSequence holds Sum f, Sum (f mod n) are_congruent_mod n
let f be integer-valued FinSequence; :: thesis: Sum f, Sum (f mod n) are_congruent_mod n
A2: f is FinSequence of INT by FINSEQ_1:102;
defpred S₁[ FinSequence of INT ] means Sum $1, Sum ($1 mod n) are_congruent_mod n;
A3: S₁[ <*> INT] by INT_1:11;
A4: for p being FinSequence of INT
for x being Element of INT st S₁[p] holds
S₁[p ^ <*x*>]

proof

let p be FinSequence of INT ; :: thesis: for x being Element of INT st S₁[p] holds
S₁[p ^ <*x*>]
let x be Element of INT ; :: thesis: ( S₁[p] implies S₁[p ^ <*x*>] )
assume A5: S₁[p] ; :: thesis: S₁[p ^ <*x*>]
A6: Sum (p ^ <*x*>) = (Sum p) + x by RVSUM_1:74;
A7: <*x*> mod n = <*(x mod n)*> by Th9;
A8: Sum <*(x mod n)*> = x mod n by RVSUM_1:73;
(p ^ <*x*>) mod n = (p mod n) ^ (<*x*> mod n) by EULER_2:15;
then A9: Sum ((p ^ <*x*>) mod n) = (Sum (p mod n)) + (x mod n) by A7, A8, RVSUM_1:75;
x,x mod n are_congruent_mod n by A1, NAT_6:10;
hence S₁[p ^ <*x*>] by A5, A6, A9, INT_1:16; :: thesis: verum

end;

for p being FinSequence of INT holds S₁[p] from FINSEQ_2:sch 2(A3, A4);
hence Sum f, Sum (f mod n) are_congruent_mod n by A2; :: thesis: verum