let F be Field; :: thesis: for p being Element of the carrier of (Polynom-Ring F)
for a being Element of F
for n being Element of NAT
for q being Polynomial of F st q = n * p & eval (p,a) = 0. F holds
eval (q,a) = 0. F
let p be Element of the carrier of (Polynom-Ring F); :: thesis: for a being Element of F
for n being Element of NAT
for q being Polynomial of F st q = n * p & eval (p,a) = 0. F holds
eval (q,a) = 0. F
let a be Element of F; :: thesis: for n being Element of NAT
for q being Polynomial of F st q = n * p & eval (p,a) = 0. F holds
eval (q,a) = 0. F
let n be Element of NAT ; :: thesis: for q being Polynomial of F st q = n * p & eval (p,a) = 0. F holds
eval (q,a) = 0. F
let q be Polynomial of F; :: thesis: ( q = n * p & eval (p,a) = 0. F implies eval (q,a) = 0. F )
assume AS: ( q = n * p & eval (p,a) = 0. F ) ; :: thesis: eval (q,a) = 0. F
defpred S₁[ Nat] means for q being Polynomial of F st q = $1 * p holds
eval (q,a) = 0. F;
A: S₁[ 0 ]

proof

now :: thesis: for q being Polynomial of F st q = 0 * p holds
eval (q,a) = 0. F

let q be Polynomial of F; :: thesis: ( q = 0 * p implies eval (q,a) = 0. F )
assume q = 0 * p ; :: thesis: eval (q,a) = 0. F
then q = 0. (Polynom-Ring F) by BINOM:12
.= 0_. F by POLYNOM3:def 10 ;
hence eval (q,a) = 0. F by POLYNOM4:17; :: thesis: verum

end;

hence S₁[ 0 ] ; :: thesis: verum

end;

B: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume B0: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for q being Polynomial of F st q = (k + 1) * p holds
eval (q,a) = 0. F

let q be Polynomial of F; :: thesis: ( q = (k + 1) * p implies eval (q,a) = 0. F )
assume B1: q = (k + 1) * p ; :: thesis: eval (q,a) = 0. F
reconsider q1 = k * p as Polynomial of F by POLYNOM3:def 10;
q = (k * p) + (1 * p) by B1, BINOM:15
.= (k * p) + p by BINOM:13
.= q1 + p by POLYNOM3:def 10 ;
hence eval (q,a) = (eval (q1,a)) + (eval (p,a)) by POLYNOM4:19
.= 0. F by B0, AS ;
:: thesis: verum

end;

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

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A, B);
hence eval (q,a) = 0. F by AS; :: thesis: verum