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_{1}[ 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_{1}[n] holds

S_{1}[n + 1]
_{1}[ 0 ]
_{1}[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

f . d,fr . d are_congruent_mod m ) holds

Product f, Product fr are_congruent_mod m

defpred S

f . d,fr . d are_congruent_mod m ) holds

Product f, Product fr are_congruent_mod m;

A1: for n being Nat st S

S

proof

A16:
S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A2: S_{1}[n]
; :: thesis: S_{1}[n + 1]

S_{1}[n + 1]
_{1}[n + 1]
; :: thesis: verum

end;assume A2: S

S

proof

hence
S
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

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;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

then A15:
Product f1, Product fr1 are_congruent_mod m
by A2, A11, A9;
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;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

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

proof

for n being Nat holds S
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;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

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