let n be Nat; :: thesis: for p being Prime

for fp being FinSequence of INT st len fp = n + 1 & p > 2 & not p divides fp . (n + 1) holds

for fr being FinSequence of INT st ( for d being Nat st d in dom fr holds

((Poly-INT fp) . (fr . d)) mod p = 0 ) & ( for d, e being Nat st d in dom fr & e in dom fr & d <> e holds

not fr . d,fr . e are_congruent_mod p ) holds

len fr <= n

let p be Prime; :: thesis: for fp being FinSequence of INT st len fp = n + 1 & p > 2 & not p divides fp . (n + 1) holds

for fr being FinSequence of INT st ( for d being Nat st d in dom fr holds

((Poly-INT fp) . (fr . d)) mod p = 0 ) & ( for d, e being Nat st d in dom fr & e in dom fr & d <> e holds

not fr . d,fr . e are_congruent_mod p ) holds

len fr <= n

defpred S_{1}[ Nat] means for fp being FinSequence of INT st len fp = $1 + 1 & p > 2 & not p divides fp . ($1 + 1) holds

for fr being FinSequence of INT st ( for d being Nat st d in dom fr holds

((Poly-INT fp) . (fr . d)) mod p = 0 ) & ( for d, e being Nat st d in dom fr & e in dom fr & d <> e holds

not fr . d,fr . e are_congruent_mod p ) holds

len fr <= $1;

A1: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[ 0 ]
_{1}[n]
from NAT_1:sch 2(A42, A1);

hence for fp being FinSequence of INT st len fp = n + 1 & p > 2 & not p divides fp . (n + 1) holds

for fr being FinSequence of INT st ( for d being Nat st d in dom fr holds

((Poly-INT fp) . (fr . d)) mod p = 0 ) & ( for d, e being Nat st d in dom fr & e in dom fr & d <> e holds

not fr . d,fr . e are_congruent_mod p ) holds

len fr <= n ; :: thesis: verum

for fp being FinSequence of INT st len fp = n + 1 & p > 2 & not p divides fp . (n + 1) holds

for fr being FinSequence of INT st ( for d being Nat st d in dom fr holds

((Poly-INT fp) . (fr . d)) mod p = 0 ) & ( for d, e being Nat st d in dom fr & e in dom fr & d <> e holds

not fr . d,fr . e are_congruent_mod p ) holds

len fr <= n

let p be Prime; :: thesis: for fp being FinSequence of INT st len fp = n + 1 & p > 2 & not p divides fp . (n + 1) holds

for fr being FinSequence of INT st ( for d being Nat st d in dom fr holds

((Poly-INT fp) . (fr . d)) mod p = 0 ) & ( for d, e being Nat st d in dom fr & e in dom fr & d <> e holds

not fr . d,fr . e are_congruent_mod p ) holds

len fr <= n

defpred S

for fr being FinSequence of INT st ( for d being Nat st d in dom fr holds

((Poly-INT fp) . (fr . d)) mod p = 0 ) & ( for d, e being Nat st d in dom fr & e in dom fr & d <> e holds

not fr . d,fr . e are_congruent_mod p ) holds

len fr <= $1;

A1: for n being Nat st S

S

proof

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

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

let fp be FinSequence of INT ; :: thesis: ( len fp = (n + 1) + 1 & p > 2 & not p divides fp . ((n + 1) + 1) implies for fr being FinSequence of INT st ( for d being Nat st d in dom fr holds

((Poly-INT fp) . (fr . d)) mod p = 0 ) & ( for d, e being Nat st d in dom fr & e in dom fr & d <> e holds

not fr . d,fr . e are_congruent_mod p ) holds

len fr <= n + 1 )

assume that

A3: len fp = (n + 1) + 1 and

A4: p > 2 and

A5: not p divides fp . ((n + 1) + 1) ; :: thesis: for fr being FinSequence of INT st ( for d being Nat st d in dom fr holds

((Poly-INT fp) . (fr . d)) mod p = 0 ) & ( for d, e being Nat st d in dom fr & e in dom fr & d <> e holds

not fr . d,fr . e are_congruent_mod p ) holds

len fr <= n + 1

end;assume A2: S

let fp be FinSequence of INT ; :: thesis: ( len fp = (n + 1) + 1 & p > 2 & not p divides fp . ((n + 1) + 1) implies for fr being FinSequence of INT st ( for d being Nat st d in dom fr holds

((Poly-INT fp) . (fr . d)) mod p = 0 ) & ( for d, e being Nat st d in dom fr & e in dom fr & d <> e holds

not fr . d,fr . e are_congruent_mod p ) holds

len fr <= n + 1 )

assume that

A3: len fp = (n + 1) + 1 and

A4: p > 2 and

A5: not p divides fp . ((n + 1) + 1) ; :: thesis: for fr being FinSequence of INT st ( for d being Nat st d in dom fr holds

((Poly-INT fp) . (fr . d)) mod p = 0 ) & ( for d, e being Nat st d in dom fr & e in dom fr & d <> e holds

not fr . d,fr . e are_congruent_mod p ) holds

len fr <= n + 1

per cases
( for x being Integer holds ((Poly-INT fp) . x) mod p <> 0 or ex a being Integer st ((Poly-INT fp) . a) mod p = 0 )
;

end;

suppose A6:
for x being Integer holds ((Poly-INT fp) . x) mod p <> 0
; :: thesis: for fr being FinSequence of INT st ( for d being Nat st d in dom fr holds

((Poly-INT fp) . (fr . d)) mod p = 0 ) & ( for d, e being Nat st d in dom fr & e in dom fr & d <> e holds

not fr . d,fr . e are_congruent_mod p ) holds

len fr <= n + 1

((Poly-INT fp) . (fr . d)) mod p = 0 ) & ( for d, e being Nat st d in dom fr & e in dom fr & d <> e holds

not fr . d,fr . e are_congruent_mod p ) holds

len fr <= n + 1

assume
ex fr being FinSequence of INT st

( ( for d being Nat st d in dom fr holds

((Poly-INT fp) . (fr . d)) mod p = 0 ) & ( for d, e being Nat st d in dom fr & e in dom fr & d <> e holds

not fr . d,fr . e are_congruent_mod p ) & len fr > n + 1 ) ; :: thesis: contradiction

then consider fr being FinSequence of INT such that

A7: for d being Nat st d in dom fr holds

((Poly-INT fp) . (fr . d)) mod p = 0 and

for d, e being Nat st d in dom fr & e in dom fr & d <> e holds

not fr . d,fr . e are_congruent_mod p and

A8: len fr > n + 1 ;

fr <> {} by A8;

then ((Poly-INT fp) . (fr . 1)) mod p = 0 by A7, FINSEQ_5:6;

hence contradiction by A6; :: thesis: verum

end;( ( for d being Nat st d in dom fr holds

((Poly-INT fp) . (fr . d)) mod p = 0 ) & ( for d, e being Nat st d in dom fr & e in dom fr & d <> e holds

not fr . d,fr . e are_congruent_mod p ) & len fr > n + 1 ) ; :: thesis: contradiction

then consider fr being FinSequence of INT such that

A7: for d being Nat st d in dom fr holds

((Poly-INT fp) . (fr . d)) mod p = 0 and

for d, e being Nat st d in dom fr & e in dom fr & d <> e holds

not fr . d,fr . e are_congruent_mod p and

A8: len fr > n + 1 ;

fr <> {} by A8;

then ((Poly-INT fp) . (fr . 1)) mod p = 0 by A7, FINSEQ_5:6;

hence contradiction by A6; :: thesis: verum

suppose
ex a being Integer st ((Poly-INT fp) . a) mod p = 0
; :: thesis: for fr being FinSequence of INT st ( for d being Nat st d in dom fr holds

((Poly-INT fp) . (fr . d)) mod p = 0 ) & ( for d, e being Nat st d in dom fr & e in dom fr & d <> e holds

not fr . d,fr . e are_congruent_mod p ) holds

len fr <= n + 1

((Poly-INT fp) . (fr . d)) mod p = 0 ) & ( for d, e being Nat st d in dom fr & e in dom fr & d <> e holds

not fr . d,fr . e are_congruent_mod p ) holds

len fr <= n + 1

then consider a being Integer such that

A9: ((Poly-INT fp) . a) mod p = 0 ;

assume ex f being FinSequence of INT st

( ( for d being Nat st d in dom f holds

((Poly-INT fp) . (f . d)) mod p = 0 ) & ( for d, e being Nat st d in dom f & e in dom f & d <> e holds

not f . d,f . e are_congruent_mod p ) & len f > n + 1 ) ; :: thesis: contradiction

then consider f being FinSequence of INT such that

A10: for d being Nat st d in dom f holds

((Poly-INT fp) . (f . d)) mod p = 0 and

A11: for d, e being Nat st d in dom f & e in dom f & d <> e holds

not f . d,f . e are_congruent_mod p and

A12: len f > n + 1 ;

consider fk being FinSequence of INT , r being Integer such that

A13: len fk = n + 1 and

A14: for x being Element of INT holds (Poly-INT fp) . x = ((x - a) * ((Poly-INT fk) . x)) + r and

A15: fp . (n + 2) = fk . (n + 1) by A3, Th6;

a is Element of INT by INT_1:def 2;

then A16: ((Poly-INT fp) . a) mod p = (((a - a) * ((Poly-INT fk) . a)) + r) mod p by A14

.= r mod p ;

A17: for d being Element of NAT st d in dom f holds

p divides ((f . d) - a) * ((Poly-INT fk) . (f . d))

end;A9: ((Poly-INT fp) . a) mod p = 0 ;

assume ex f being FinSequence of INT st

( ( for d being Nat st d in dom f holds

((Poly-INT fp) . (f . d)) mod p = 0 ) & ( for d, e being Nat st d in dom f & e in dom f & d <> e holds

not f . d,f . e are_congruent_mod p ) & len f > n + 1 ) ; :: thesis: contradiction

then consider f being FinSequence of INT such that

A10: for d being Nat st d in dom f holds

((Poly-INT fp) . (f . d)) mod p = 0 and

A11: for d, e being Nat st d in dom f & e in dom f & d <> e holds

not f . d,f . e are_congruent_mod p and

A12: len f > n + 1 ;

consider fk being FinSequence of INT , r being Integer such that

A13: len fk = n + 1 and

A14: for x being Element of INT holds (Poly-INT fp) . x = ((x - a) * ((Poly-INT fk) . x)) + r and

A15: fp . (n + 2) = fk . (n + 1) by A3, Th6;

a is Element of INT by INT_1:def 2;

then A16: ((Poly-INT fp) . a) mod p = (((a - a) * ((Poly-INT fk) . a)) + r) mod p by A14

.= r mod p ;

A17: for d being Element of NAT st d in dom f holds

p divides ((f . d) - a) * ((Poly-INT fk) . (f . d))

proof

let d be Element of NAT ; :: thesis: ( d in dom f implies p divides ((f . d) - a) * ((Poly-INT fk) . (f . d)) )

f . d is Element of INT by INT_1:def 2;

then A18: ((Poly-INT fp) . (f . d)) mod p = ((((f . d) - a) * ((Poly-INT fk) . (f . d))) + r) mod p by A14

.= (((((f . d) - a) * ((Poly-INT fk) . (f . d))) mod p) + (r mod p)) mod p by NAT_D:66

.= (((f . d) - a) * ((Poly-INT fk) . (f . d))) mod p by A9, A16, NAT_D:65 ;

assume d in dom f ; :: thesis: p divides ((f . d) - a) * ((Poly-INT fk) . (f . d))

then (((f . d) - a) * ((Poly-INT fk) . (f . d))) mod p = 0 by A10, A18;

hence p divides ((f . d) - a) * ((Poly-INT fk) . (f . d)) by INT_1:62; :: thesis: verum

end;f . d is Element of INT by INT_1:def 2;

then A18: ((Poly-INT fp) . (f . d)) mod p = ((((f . d) - a) * ((Poly-INT fk) . (f . d))) + r) mod p by A14

.= (((((f . d) - a) * ((Poly-INT fk) . (f . d))) mod p) + (r mod p)) mod p by NAT_D:66

.= (((f . d) - a) * ((Poly-INT fk) . (f . d))) mod p by A9, A16, NAT_D:65 ;

assume d in dom f ; :: thesis: p divides ((f . d) - a) * ((Poly-INT fk) . (f . d))

then (((f . d) - a) * ((Poly-INT fk) . (f . d))) mod p = 0 by A10, A18;

hence p divides ((f . d) - a) * ((Poly-INT fk) . (f . d)) by INT_1:62; :: thesis: verum

per cases
( for d being Nat st d in dom f holds

not p divides (f . d) - a or ex d being Nat st

( d in dom f & p divides (f . d) - a ) ) ;

end;

not p divides (f . d) - a or ex d being Nat st

( d in dom f & p divides (f . d) - a ) ) ;

suppose A19:
for d being Nat st d in dom f holds

not p divides (f . d) - a ; :: thesis: contradiction

not p divides (f . d) - a ; :: thesis: contradiction

for d being Nat st d in dom f holds

((Poly-INT fk) . (f . d)) mod p = 0

hence contradiction by A12, XREAL_1:145; :: thesis: verum

end;((Poly-INT fk) . (f . d)) mod p = 0

proof

then
len f <= n
by A2, A4, A5, A13, A15, A11;
let d be Nat; :: thesis: ( d in dom f implies ((Poly-INT fk) . (f . d)) mod p = 0 )

assume A20: d in dom f ; :: thesis: ((Poly-INT fk) . (f . d)) mod p = 0

then p divides ((f . d) - a) * ((Poly-INT fk) . (f . d)) by A17;

then ( p divides (f . d) - a or p divides (Poly-INT fk) . (f . d) ) by Th7;

hence ((Poly-INT fk) . (f . d)) mod p = 0 by A19, A20, INT_1:62; :: thesis: verum

end;assume A20: d in dom f ; :: thesis: ((Poly-INT fk) . (f . d)) mod p = 0

then p divides ((f . d) - a) * ((Poly-INT fk) . (f . d)) by A17;

then ( p divides (f . d) - a or p divides (Poly-INT fk) . (f . d) ) by Th7;

hence ((Poly-INT fk) . (f . d)) mod p = 0 by A19, A20, INT_1:62; :: thesis: verum

hence contradiction by A12, XREAL_1:145; :: thesis: verum

suppose
ex d being Nat st

( d in dom f & p divides (f . d) - a ) ; :: thesis: contradiction

( d in dom f & p divides (f . d) - a ) ; :: thesis: contradiction

then consider d9 being Element of NAT such that

A21: d9 in dom f and

A22: p divides (f . d9) - a ;

set f9 = f - {(f . d9)};

A23: for d being Nat st d in dom (f - {(f . d9)}) holds

not p divides ((f - {(f . d9)}) . d) - a

((Poly-INT fk) . ((f - {(f . d9)}) . d)) mod p = 0

then A33: f - {(f . d9)} is one-to-one by FINSEQ_3:87;

A34: for d, e being Nat st d in dom (f - {(f . d9)}) & e in dom (f - {(f . d9)}) & d <> e holds

not (f - {(f . d9)}) . d,(f - {(f . d9)}) . e are_congruent_mod p

then len (f - {(f . d9)}) = (len f) - 1 by A32, FINSEQ_3:90;

then len (f - {(f . d9)}) > (n + 1) - 1 by A12, XREAL_1:9;

hence contradiction by A2, A4, A5, A13, A15, A30, A34; :: thesis: verum

end;A21: d9 in dom f and

A22: p divides (f . d9) - a ;

set f9 = f - {(f . d9)};

A23: for d being Nat st d in dom (f - {(f . d9)}) holds

not p divides ((f - {(f . d9)}) . d) - a

proof

A30:
for d being Nat st d in dom (f - {(f . d9)}) holds
given k being Nat such that A24:
k in dom (f - {(f . d9)})
and

A25: p divides ((f - {(f . d9)}) . k) - a ; :: thesis: contradiction

(f - {(f . d9)}) . k in rng (f - {(f . d9)}) by A24, FUNCT_1:3;

then A26: (f - {(f . d9)}) . k in (rng f) \ {(f . d9)} by FINSEQ_3:65;

then (f - {(f . d9)}) . k in rng f by XBOOLE_0:def 5;

then consider w being object such that

A27: w in dom f and

A28: f . w = (f - {(f . d9)}) . k by FUNCT_1:def 3;

reconsider w = w as Element of NAT by A27;

p divides ((f . w) - a) - ((f . d9) - a) by A22, A25, A28, Th1;

then A29: f . w,f . d9 are_congruent_mod p ;

not (f - {(f . d9)}) . k in {(f . d9)} by A26, XBOOLE_0:def 5;

then w <> d9 by A28, TARSKI:def 1;

hence contradiction by A11, A21, A27, A29; :: thesis: verum

end;A25: p divides ((f - {(f . d9)}) . k) - a ; :: thesis: contradiction

(f - {(f . d9)}) . k in rng (f - {(f . d9)}) by A24, FUNCT_1:3;

then A26: (f - {(f . d9)}) . k in (rng f) \ {(f . d9)} by FINSEQ_3:65;

then (f - {(f . d9)}) . k in rng f by XBOOLE_0:def 5;

then consider w being object such that

A27: w in dom f and

A28: f . w = (f - {(f . d9)}) . k by FUNCT_1:def 3;

reconsider w = w as Element of NAT by A27;

p divides ((f . w) - a) - ((f . d9) - a) by A22, A25, A28, Th1;

then A29: f . w,f . d9 are_congruent_mod p ;

not (f - {(f . d9)}) . k in {(f . d9)} by A26, XBOOLE_0:def 5;

then w <> d9 by A28, TARSKI:def 1;

hence contradiction by A11, A21, A27, A29; :: thesis: verum

((Poly-INT fk) . ((f - {(f . d9)}) . d)) mod p = 0

proof

A32:
f is one-to-one
by A11, INT_1:11;
let d be Nat; :: thesis: ( d in dom (f - {(f . d9)}) implies ((Poly-INT fk) . ((f - {(f . d9)}) . d)) mod p = 0 )

assume A31: d in dom (f - {(f . d9)}) ; :: thesis: ((Poly-INT fk) . ((f - {(f . d9)}) . d)) mod p = 0

then (f - {(f . d9)}) . d in rng (f - {(f . d9)}) by FUNCT_1:3;

then (f - {(f . d9)}) . d in (rng f) \ {(f . d9)} by FINSEQ_3:65;

then (f - {(f . d9)}) . d in rng f by XBOOLE_0:def 5;

then ex w being object st

( w in dom f & f . w = (f - {(f . d9)}) . d ) by FUNCT_1:def 3;

then p divides (((f - {(f . d9)}) . d) - a) * ((Poly-INT fk) . ((f - {(f . d9)}) . d)) by A17;

then ( p divides ((f - {(f . d9)}) . d) - a or p divides (Poly-INT fk) . ((f - {(f . d9)}) . d) ) by Th7;

hence ((Poly-INT fk) . ((f - {(f . d9)}) . d)) mod p = 0 by A23, A31, INT_1:62; :: thesis: verum

end;assume A31: d in dom (f - {(f . d9)}) ; :: thesis: ((Poly-INT fk) . ((f - {(f . d9)}) . d)) mod p = 0

then (f - {(f . d9)}) . d in rng (f - {(f . d9)}) by FUNCT_1:3;

then (f - {(f . d9)}) . d in (rng f) \ {(f . d9)} by FINSEQ_3:65;

then (f - {(f . d9)}) . d in rng f by XBOOLE_0:def 5;

then ex w being object st

( w in dom f & f . w = (f - {(f . d9)}) . d ) by FUNCT_1:def 3;

then p divides (((f - {(f . d9)}) . d) - a) * ((Poly-INT fk) . ((f - {(f . d9)}) . d)) by A17;

then ( p divides ((f - {(f . d9)}) . d) - a or p divides (Poly-INT fk) . ((f - {(f . d9)}) . d) ) by Th7;

hence ((Poly-INT fk) . ((f - {(f . d9)}) . d)) mod p = 0 by A23, A31, INT_1:62; :: thesis: verum

then A33: f - {(f . d9)} is one-to-one by FINSEQ_3:87;

A34: for d, e being Nat st d in dom (f - {(f . d9)}) & e in dom (f - {(f . d9)}) & d <> e holds

not (f - {(f . d9)}) . d,(f - {(f . d9)}) . e are_congruent_mod p

proof

f . d9 in rng f
by A21, FUNCT_1:3;
let d, e be Nat; :: thesis: ( d in dom (f - {(f . d9)}) & e in dom (f - {(f . d9)}) & d <> e implies not (f - {(f . d9)}) . d,(f - {(f . d9)}) . e are_congruent_mod p )

assume that

A35: d in dom (f - {(f . d9)}) and

A36: e in dom (f - {(f . d9)}) and

A37: d <> e ; :: thesis: not (f - {(f . d9)}) . d,(f - {(f . d9)}) . e are_congruent_mod p

(f - {(f . d9)}) . e in rng (f - {(f . d9)}) by A36, FUNCT_1:3;

then (f - {(f . d9)}) . e in (rng f) \ {(f . d9)} by FINSEQ_3:65;

then (f - {(f . d9)}) . e in rng f by XBOOLE_0:def 5;

then consider w2 being object such that

A38: w2 in dom f and

A39: (f - {(f . d9)}) . e = f . w2 by FUNCT_1:def 3;

(f - {(f . d9)}) . d in rng (f - {(f . d9)}) by A35, FUNCT_1:3;

then (f - {(f . d9)}) . d in (rng f) \ {(f . d9)} by FINSEQ_3:65;

then (f - {(f . d9)}) . d in rng f by XBOOLE_0:def 5;

then consider w1 being object such that

A40: w1 in dom f and

A41: (f - {(f . d9)}) . d = f . w1 by FUNCT_1:def 3;

reconsider w1 = w1, w2 = w2 as Element of NAT by A40, A38;

w1 <> w2 by A33, A35, A36, A37, A41, A39;

hence not (f - {(f . d9)}) . d,(f - {(f . d9)}) . e are_congruent_mod p by A11, A40, A41, A38, A39; :: thesis: verum

end;assume that

A35: d in dom (f - {(f . d9)}) and

A36: e in dom (f - {(f . d9)}) and

A37: d <> e ; :: thesis: not (f - {(f . d9)}) . d,(f - {(f . d9)}) . e are_congruent_mod p

(f - {(f . d9)}) . e in rng (f - {(f . d9)}) by A36, FUNCT_1:3;

then (f - {(f . d9)}) . e in (rng f) \ {(f . d9)} by FINSEQ_3:65;

then (f - {(f . d9)}) . e in rng f by XBOOLE_0:def 5;

then consider w2 being object such that

A38: w2 in dom f and

A39: (f - {(f . d9)}) . e = f . w2 by FUNCT_1:def 3;

(f - {(f . d9)}) . d in rng (f - {(f . d9)}) by A35, FUNCT_1:3;

then (f - {(f . d9)}) . d in (rng f) \ {(f . d9)} by FINSEQ_3:65;

then (f - {(f . d9)}) . d in rng f by XBOOLE_0:def 5;

then consider w1 being object such that

A40: w1 in dom f and

A41: (f - {(f . d9)}) . d = f . w1 by FUNCT_1:def 3;

reconsider w1 = w1, w2 = w2 as Element of NAT by A40, A38;

w1 <> w2 by A33, A35, A36, A37, A41, A39;

hence not (f - {(f . d9)}) . d,(f - {(f . d9)}) . e are_congruent_mod p by A11, A40, A41, A38, A39; :: thesis: verum

then len (f - {(f . d9)}) = (len f) - 1 by A32, FINSEQ_3:90;

then len (f - {(f . d9)}) > (n + 1) - 1 by A12, XREAL_1:9;

hence contradiction by A2, A4, A5, A13, A15, A30, A34; :: thesis: verum

proof

for n being Nat holds S
let fp be FinSequence of INT ; :: thesis: ( len fp = 0 + 1 & p > 2 & not p divides fp . (0 + 1) implies for fr being FinSequence of INT st ( for d being Nat st d in dom fr holds

((Poly-INT fp) . (fr . d)) mod p = 0 ) & ( for d, e being Nat st d in dom fr & e in dom fr & d <> e holds

not fr . d,fr . e are_congruent_mod p ) holds

len fr <= 0 )

assume that

A43: len fp = 0 + 1 and

p > 2 and

A44: not p divides fp . (0 + 1) ; :: thesis: for fr being FinSequence of INT st ( for d being Nat st d in dom fr holds

((Poly-INT fp) . (fr . d)) mod p = 0 ) & ( for d, e being Nat st d in dom fr & e in dom fr & d <> e holds

not fr . d,fr . e are_congruent_mod p ) holds

len fr <= 0

assume ex fr being FinSequence of INT st

( ( for d being Nat st d in dom fr holds

((Poly-INT fp) . (fr . d)) mod p = 0 ) & ( for d, e being Nat st d in dom fr & e in dom fr & d <> e holds

not fr . d,fr . e are_congruent_mod p ) & len fr > 0 ) ; :: thesis: contradiction

then consider fr being FinSequence of INT such that

A45: for d being Nat st d in dom fr holds

((Poly-INT fp) . (fr . d)) mod p = 0 and

for d, e being Nat st d in dom fr & e in dom fr & d <> e holds

not fr . d,fr . e are_congruent_mod p and

A46: len fr > 0 ;

fr <> {} by A46;

then A47: ((Poly-INT fp) . (fr . 1)) mod p = 0 by A45, FINSEQ_5:6;

A48: fr . 1 in INT by INT_1:def 2;

(Poly-INT fp) . (fr . 1) = (INT --> (fp . 1)) . (fr . 1) by A43, Th3

.= fp . 1 by A48, FUNCOP_1:7 ;

hence contradiction by A44, A47, Lm1; :: thesis: verum

end;((Poly-INT fp) . (fr . d)) mod p = 0 ) & ( for d, e being Nat st d in dom fr & e in dom fr & d <> e holds

not fr . d,fr . e are_congruent_mod p ) holds

len fr <= 0 )

assume that

A43: len fp = 0 + 1 and

p > 2 and

A44: not p divides fp . (0 + 1) ; :: thesis: for fr being FinSequence of INT st ( for d being Nat st d in dom fr holds

((Poly-INT fp) . (fr . d)) mod p = 0 ) & ( for d, e being Nat st d in dom fr & e in dom fr & d <> e holds

not fr . d,fr . e are_congruent_mod p ) holds

len fr <= 0

assume ex fr being FinSequence of INT st

( ( for d being Nat st d in dom fr holds

((Poly-INT fp) . (fr . d)) mod p = 0 ) & ( for d, e being Nat st d in dom fr & e in dom fr & d <> e holds

not fr . d,fr . e are_congruent_mod p ) & len fr > 0 ) ; :: thesis: contradiction

then consider fr being FinSequence of INT such that

A45: for d being Nat st d in dom fr holds

((Poly-INT fp) . (fr . d)) mod p = 0 and

for d, e being Nat st d in dom fr & e in dom fr & d <> e holds

not fr . d,fr . e are_congruent_mod p and

A46: len fr > 0 ;

fr <> {} by A46;

then A47: ((Poly-INT fp) . (fr . 1)) mod p = 0 by A45, FINSEQ_5:6;

A48: fr . 1 in INT by INT_1:def 2;

(Poly-INT fp) . (fr . 1) = (INT --> (fp . 1)) . (fr . 1) by A43, Th3

.= fp . 1 by A48, FUNCOP_1:7 ;

hence contradiction by A44, A47, Lm1; :: thesis: verum

hence for fp being FinSequence of INT st len fp = n + 1 & p > 2 & not p divides fp . (n + 1) holds

for fr being FinSequence of INT st ( for d being Nat st d in dom fr holds

((Poly-INT fp) . (fr . d)) mod p = 0 ) & ( for d, e being Nat st d in dom fr & e in dom fr & d <> e holds

not fr . d,fr . e are_congruent_mod p ) holds

len fr <= n ; :: thesis: verum