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,((- 1) |^ (len f)) * (Product fr) are_congruent_mod m

defpred S1[ 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,((- 1) |^ (len f)) * (Product fr) are_congruent_mod m;
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; :: thesis: S1[n + 1]
S1[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,((- 1) |^ (len 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,((- 1) |^ (len 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 ;
f <> {} by A3;
then A7: n + 1 in dom f by ;
consider f1 being FinSequence of INT , a being Element of INT such that
A8: f = f1 ^ <*a*> by ;
A9: n + 1 = (len fr1) + 1 by ;
then A10: fr . (n + 1) = b by ;
A11: n + 1 = (len f1) + 1 by ;
then A12: dom f1 = dom fr1 by ;
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 ;
fr . d = fr1 . d by ;
hence f1 . d, - (fr1 . d) are_congruent_mod m by ; :: thesis: verum
end;
then A15: Product f1,((- 1) |^ (len f1)) * (Product fr1) are_congruent_mod m by A2, A11, A9;
f . (n + 1) = a by ;
then a, - b are_congruent_mod m by A5, A7, A10;
then (Product f1) * a,(((- 1) |^ (len f1)) * (Product fr1)) * (- b) are_congruent_mod m by ;
then Product f,(((- 1) |^ (len f1)) * (- 1)) * ((Product fr1) * b) are_congruent_mod m by ;
then Product f,((- 1) |^ ((len f1) + 1)) * ((Product fr1) * b) are_congruent_mod m by NEWTON:6;
hence Product f,((- 1) |^ (len f)) * (Product fr) are_congruent_mod m by ; :: thesis: verum
end;
hence S1[n + 1] ; :: thesis: verum
end;
A16: S1[ 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,((- 1) |^ (len 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,((- 1) |^ (len f)) * (Product fr) are_congruent_mod m )

A19: f = <*> INT by A17;
A20: (- 1) |^ (len f) = 1 by ;
fr = <*> INT by ;
hence ( ex d being Nat st
( d in dom f & not f . d, - (fr . d) are_congruent_mod m ) or Product f,((- 1) |^ (len f)) * (Product fr) are_congruent_mod m ) by ; :: thesis: verum
end;
for n being Nat holds S1[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,((- 1) |^ (len f)) * (Product fr) are_congruent_mod m ; :: thesis: verum