let m be Integer; :: thesis: for f, fr being FinSequence of INT st len f = len fr & ( for d being Nat st d in dom f holds
f . d,fr . d are_congruent_mod m ) holds
Product f, Product fr are_congruent_mod m
defpred S₁[ Nat] means for f, fr being FinSequence of INT st len f = $1 & len f = len fr & ( for d being Nat st d in dom f holds
f . d,fr . d are_congruent_mod m ) holds
Product f, Product fr are_congruent_mod m;
A1: S₁[ 0 ]

proof

let f, fr be FinSequence of INT ; :: thesis: ( len f = 0 & len f = len fr & ( for d being Nat st d in dom f holds
f . d,fr . d are_congruent_mod m ) implies Product f, Product fr are_congruent_mod m )
assume ( len f = 0 & len f = len fr ) ; :: thesis: ( ex d being Nat st
( d in dom f & not f . d,fr . d are_congruent_mod m ) or Product f, Product fr are_congruent_mod m )
then ( f = <*> INT & fr = <*> INT ) ;
hence ( ex d being Nat st
( d in dom f & not f . d,fr . d are_congruent_mod m ) or Product f, Product fr are_congruent_mod m ) by INT_1:32; :: thesis: verum

end;

A2: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
S₁[n + 1]

proof

let f, fr be FinSequence of INT ; :: thesis: ( len f = n + 1 & len f = len fr & ( for d being Nat st d in dom f holds
f . d,fr . d are_congruent_mod m ) implies Product f, Product fr are_congruent_mod m )
assume A4: ( len f = n + 1 & len f = len fr & ( for d being Nat st d in dom f holds
f . d,fr . d are_congruent_mod m ) ) ; :: thesis: Product f, Product fr are_congruent_mod m
then consider f1 being FinSequence of INT , a being Element of INT such that
A5: f = f1 ^ <*a*> by FINSEQ_2:22;
consider fr1 being FinSequence of INT , b being Element of INT such that
A6: fr = fr1 ^ <*b*> by A4, FINSEQ_2:22;
A7: ( n + 1 = (len f1) + 1 & n + 1 = (len fr1) + 1 ) by A4, A5, A6, FINSEQ_2:19;
then A8: dom f1 = dom fr1 by FINSEQ_3:31;
for d being Nat st d in dom f1 holds
f1 . d,fr1 . d are_congruent_mod m

proof

let d be Nat; :: thesis: ( d in dom f1 implies f1 . d,fr1 . d are_congruent_mod m )
assume A9: d in dom f1 ; :: thesis: f1 . d,fr1 . d are_congruent_mod m
then ( f . d = f1 . d & fr . d = fr1 . d ) by A5, A6, A8, FINSEQ_1:def 7;
hence f1 . d,fr1 . d are_congruent_mod m by A4, A5, A9, FINSEQ_2:18; :: thesis: verum

end;

then A10: Product f1, Product fr1 are_congruent_mod m by A3, A7;
f <> {} by A4;
then A11: n + 1 in dom f by A4, FINSEQ_5:6;
( f . (n + 1) = a & fr . (n + 1) = b ) by A5, A6, A7, FINSEQ_1:59;
then a,b are_congruent_mod m by A4, A11;
then (Product f1) * a,(Product fr1) * b are_congruent_mod m by A10, INT_1:39;
then Product f,(Product fr1) * b are_congruent_mod m by A5, RVSUM_1:126;
hence Product f, Product fr are_congruent_mod m by A6, RVSUM_1:126; :: thesis: verum

end;

hence S₁[n + 1] ; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A1, A2);
hence for f, fr being FinSequence of INT st len f = len fr & ( for d being Nat st d in dom f holds
f . d,fr . d are_congruent_mod m ) holds
Product f, Product fr are_congruent_mod m ; :: thesis: verum