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: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: 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 that
A3: len f = n + 1 and
A4: len f = len fr and
A5: 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
consider fr1 being FinSequence of INT , b being Element of INT such that
A6: fr = fr1 ^ <*b*> by A3, A4, FINSEQ_2:19;
f <> {} by A3;
then A7: n + 1 in dom f by A3, FINSEQ_5:6;
consider f1 being FinSequence of INT , a being Element of INT such that
A8: f = f1 ^ <*a*> by A3, FINSEQ_2:19;
A9: n + 1 = (len fr1) + 1 by A3, A4, A6, FINSEQ_2:16;
then A10: fr . (n + 1) = b by A6, FINSEQ_1:42;
A11: n + 1 = (len f1) + 1 by A3, A8, FINSEQ_2:16;
then A12: dom f1 = dom fr1 by A9, FINSEQ_3:29;
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 A13: d in dom f1 ; :: thesis: f1 . d,fr1 . d are_congruent_mod m
then A14: f . d = f1 . d by A8, FINSEQ_1:def 7;
fr . d = fr1 . d by A6, A12, A13, FINSEQ_1:def 7;
hence f1 . d,fr1 . d are_congruent_mod m by A5, A8, A13, A14, FINSEQ_2:15; :: thesis: verum

end;

then A15: Product f1, Product fr1 are_congruent_mod m by A2, A11, A9;
f . (n + 1) = a by A8, A11, FINSEQ_1:42;
then a,b are_congruent_mod m by A5, A7, A10;
then (Product f1) * a,(Product fr1) * b are_congruent_mod m by A15, INT_1:18;
then Product f,(Product fr1) * b are_congruent_mod m by A8, RVSUM_1:96;
hence Product f, Product fr are_congruent_mod m by A6, RVSUM_1:96; :: thesis: verum

end;

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

end;

A16: 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 that
A17: len f = 0 and
A18: 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 )
A19: f = <*> INT by A17;
fr = <*> INT by A17, A18;
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 A19, INT_1:11; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A16, A1);
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