let R be commutative Ring; :: thesis: for p being Polynomial of R
for n being non zero Nat holds (p `^ n) . 0 = (p . 0) |^ n
let p be Polynomial of R; :: thesis: for n being non zero Nat holds (p `^ n) . 0 = (p . 0) |^ n
let n be non zero Nat; :: thesis: (p `^ n) . 0 = (p . 0) |^ n
defpred S<sub>1</sub>[ Nat] means (p `^ $1) . 0 = (p . 0) |^ $1;
(p `^ 1) . 0 = p . 0 by POLYNOM5:16
.= (p . 0) |^ 1 by BINOM:8 ;
then IA: S₁[1] ;

IS: now :: thesis: for k being Nat st k >= 1 & S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( k >= 1 & S₁[k] implies S₁[k + 1] )
assume k >= 1 ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume IV: S₁[k] ; :: thesis: S₁[k + 1]
(p `^ (k + 1)) . 0 = ((p `^ k) *' p) . 0 by POLYNOM5:19
.= ((p `^ k) . 0) * (p . 0) by t3a
.= ((p . 0) |^ k) * ((p . 0) |^ 1) by IV, BINOM:8
.= (p . 0) |^ (k + 1) by BINOM:10 ;
hence S₁[k + 1] ; :: thesis: verum

end;

I: for k being Nat st k >= 1 holds
S₁[k] from NAT_1:sch 8(IA, IS);
n >= 0 + 1 by INT_1:7;
hence (p `^ n) . 0 = (p . 0) |^ n by I; :: thesis: verum