let R be Ring; :: thesis: for q being Element of the carrier of (Polynom-Ring R)
for p being Polynomial of R
for n, j being Nat st p = n * q holds
p . j = n * (q . j)
let q be Element of the carrier of (Polynom-Ring R); :: thesis: for p being Polynomial of R
for n, j being Nat st p = n * q holds
p . j = n * (q . j)
let p be Polynomial of R; :: thesis: for n, j being Nat st p = n * q holds
p . j = n * (q . j)
let n, j be Nat; :: thesis: ( p = n * q implies p . j = n * (q . j) )
assume AS: p = n * q ; :: thesis: p . j = n * (q . j)
defpred S₁[ Nat] means for q being Element of the carrier of (Polynom-Ring R)
for p being Polynomial of R
for j being Nat st p = $1 * q holds
p . j = $1 * (q . j);
IA: S₁[ 0 ]

proof

now :: thesis: for q being Element of the carrier of (Polynom-Ring R)
for p being Polynomial of R
for j being Nat st p = 0 * q holds
p . j = 0 * (q . j)

let q be Element of the carrier of (Polynom-Ring R); :: thesis: for p being Polynomial of R
for j being Nat st p = 0 * q holds
p . j = 0 * (q . j)
let p be Polynomial of R; :: thesis: for j being Nat st p = 0 * q holds
p . j = 0 * (q . j)
let j be Nat; :: thesis: ( p = 0 * q implies p . j = 0 * (q . j) )
assume p = 0 * q ; :: thesis: p . j = 0 * (q . j)
then p = 0. (Polynom-Ring R) by BINOM:12
.= 0_. R by POLYNOM3:def 10 ;
hence p . j = 0. R by ORDINAL1:def 12, FUNCOP_1:7
.= 0 * (q . j) by BINOM:12 ;
:: thesis: verum

end;

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

end;

IS: 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 IV: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for q being Element of the carrier of (Polynom-Ring R)
for p being Polynomial of R
for j being Nat st p = (k + 1) * q holds
p . j = (k + 1) * (q . j)

let q be Element of the carrier of (Polynom-Ring R); :: thesis: for p being Polynomial of R
for j being Nat st p = (k + 1) * q holds
p . j = (k + 1) * (q . j)
let p be Polynomial of R; :: thesis: for j being Nat st p = (k + 1) * q holds
p . j = (k + 1) * (q . j)
let j be Nat; :: thesis: ( p = (k + 1) * q implies p . j = (k + 1) * (q . j) )
assume AS: p = (k + 1) * q ; :: thesis: p . j = (k + 1) * (q . j)
reconsider p1 = k * q, r = q as Polynomial of R by POLYNOM3:def 10;
p = (k * q) + (1 * q) by AS, BINOM:15
.= (k * q) + q by BINOM:13
.= p1 + r by POLYNOM3:def 10 ;
hence p . j = (p1 . j) + (r . j) by NORMSP_1:def 2
.= (k * (q . j)) + (q . j) by IV
.= (k * (q . j)) + (1 * (q . j)) by BINOM:13
.= (k + 1) * (q . j) by BINOM:15 ;
:: thesis: verum

end;

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

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(IA, IS);
hence p . j = n * (q . j) by AS; :: thesis: verum