let m be Nat; :: thesis: for f being integer-valued FinSequence st m <> 0 holds
(Product (f mod m)) mod m = (Product f) mod m
defpred S₁[ Nat] means for f being integer-valued FinSequence st m <> 0 & len f = $1 holds
(Product (f mod m)) mod m = (Product f) mod m;
let f be integer-valued FinSequence; :: thesis: ( m <> 0 implies (Product (f mod m)) mod m = (Product f) mod m )
assume A1: m <> 0 ; :: thesis: (Product (f mod m)) mod m = (Product f) mod m
A2: len f is Element of NAT ;
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
let f be integer-valued FinSequence; :: thesis: ( m <> 0 & len f = n + 1 implies (Product (f mod m)) mod m = (Product f) mod m )
assume that
A5: m <> 0 and
A6: len f = n + 1 ; :: thesis: (Product (f mod m)) mod m = (Product f) mod m
reconsider fn = f | n as integer-valued FinSequence ;
A7: len fn = n by A6, FINSEQ_1:59, NAT_1:11;
A8: len (f mod m) = n + 1 by A6, Def2;
then A9: len ((f mod m) | n) = n by FINSEQ_1:59, NAT_1:11;
A10: n <= len f by A6, NAT_1:11;
A11: for i being Nat st 1 <= i & i <= len ((f mod m) | n) holds
((f mod m) | n) . i = (fn mod m) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len ((f mod m) | n) implies ((f mod m) | n) . i = (fn mod m) . i )
assume that
A12: 1 <= i and
A13: i <= len ((f mod m) | n) ; :: thesis: ((f mod m) | n) . i = (fn mod m) . i
A14: (f | n) . i = (f | (Seg n)) . i by FINSEQ_1:def 16;
A15: i in Seg n by A9, A12, A13, FINSEQ_1:1;
then A16: ((f mod m) | (Seg n)) . i = (f mod m) . i by FUNCT_1:49;
i <= len f by A10, A9, A13, XXREAL_0:2;
then A17: i in dom f by A12, FINSEQ_3:25;
i in dom fn by A7, A9, A12, A13, FINSEQ_3:25;
then (fn mod m) . i = (fn . i) mod m by Def1
.= (f . i) mod m by A15, A14, FUNCT_1:49
.= (f mod m) . i by A17, Def1 ;
hence ((f mod m) | n) . i = (fn mod m) . i by A16, FINSEQ_1:def 16; :: thesis: verum

end;

0 + 1 <= n + 1 by NAT_1:13;
then n + 1 in dom f by A6, FINSEQ_3:25;
then A18: (f mod m) . (n + 1) = (f . (n + 1)) mod m by Def1;
reconsider F = fn mod m as integer-valued FinSequence ;
len ((f mod m) | n) = len (fn mod m) by A7, A9, Def2;
then (f mod m) | n = fn mod m by A11, FINSEQ_1:14;
then f mod m = (fn mod m) ^ <*((f . (n + 1)) mod m)*> by A8, A18, RFINSEQ:7;
then A19: (Product (f mod m)) mod m = ((Product (fn mod m)) * ((f . (n + 1)) mod m)) mod m by RVSUM_1:96
.= (((Product (fn mod m)) mod m) * (((f . (n + 1)) mod m) mod m)) mod m by NAT_D:67
.= (((Product fn) mod m) * (((f . (n + 1)) mod m) mod m)) mod m by A4, A5, A7
.= (((Product fn) mod m) * ((f . (n + 1)) mod m)) mod m by NAT_D:73 ;
(Product f) mod m = (Product (fn ^ <*(f . (n + 1))*>)) mod m by A6, RFINSEQ:7
.= ((Product fn) * (f . (n + 1))) mod m by RVSUM_1:96 ;
hence (Product (f mod m)) mod m = (Product f) mod m by A19, NAT_D:67; :: thesis: verum

end;

A20: S₁[ 0 ]

proof

let f be integer-valued FinSequence; :: thesis: ( m <> 0 & len f = 0 implies (Product (f mod m)) mod m = (Product f) mod m )
assume that
m <> 0 and
A21: len f = 0 ; :: thesis: (Product (f mod m)) mod m = (Product f) mod m
A22: ( f = <*> NAT & len (f mod m) = 0 ) by A21, Def2;
then f mod m = <*> NAT ;
hence (Product (f mod m)) mod m = (Product f) mod m by A22; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A20, A3);
hence (Product (f mod m)) mod m = (Product f) mod m by A1, A2; :: thesis: verum