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

proof

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

let q be Element of the carrier of (Polynom-Ring R); :: thesis: for p being Polynomial of R holds (0 * (1. R)) * p = 0 * q
let p be Polynomial of R; :: thesis: (0 * (1. R)) * p = 0 * q
thus (0 * (1. R)) * p = (0. R) * p by BINOM:12
.= 0_. R by POLYNOM5:26
.= 0. (Polynom-Ring R) by POLYNOM3:def 10
.= 0 * q 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 st p = q holds
((k + 1) * (1. R)) * p = (k + 1) * q

let q be Element of the carrier of (Polynom-Ring R); :: thesis: for p being Polynomial of R st p = q holds
((k + 1) * (1. R)) * p = (k + 1) * q
let p be Polynomial of R; :: thesis: ( p = q implies ((k + 1) * (1. R)) * p = (k + 1) * q )
assume AS: p = q ; :: thesis: ((k + 1) * (1. R)) * p = (k + 1) * q
then A: (k * (1. R)) * p = k * q by IV;
thus ((k + 1) * (1. R)) * p = ((k * (1. R)) + (1 * (1. R))) * p by BINOM:15
.= ((k * (1. R)) + (1. R)) * p by BINOM:13
.= ((k * (1. R)) * p) + ((1. R) * p) by BBD
.= (k * q) + q by AS, A, POLYNOM3:def 10
.= (k * q) + (1 * q) by BINOM:13
.= (k + 1) * q 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 (n * (1. R)) * p = n * q by AS; :: thesis: verum