let R be non degenerated comRing; :: thesis: for a, b being Element of R
for n being Nat holds eval (((X+ a) `^ n),b) = (a + b) |^ n
let a, b be Element of R; :: thesis: for n being Nat holds eval (((X+ a) `^ n),b) = (a + b) |^ n
let n be Nat; :: thesis: eval (((X+ a) `^ n),b) = (a + b) |^ n
defpred S<sub>1</sub>[ Nat] means eval (((X+ a) `^ $1),b) = (a + b) |^ $1;
eval (((X+ a) `^ 0),b) = eval ((1_. R),b) by POLYNOM5:15
.= 1_ R by POLYNOM4:18
.= (a + b) |^ 0 by BINOM:8 ;
then IA: S₁[ 0 ] ;

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]
eval (((X+ a) `^ (k + 1)),b) = eval ((((X+ a) `^ k) *' (X+ a)),b) by POLYNOM5:19
.= ((a + b) |^ k) * (eval ((X+ a),b)) by IV, POLYNOM4:24
.= ((a + b) |^ k) * (b - (- a)) by HURWITZ:29
.= ((a + b) |^ k) * ((a + b) |^ 1) by BINOM:8
.= (a + b) |^ (k + 1) by BINOM:10 ;
hence S₁[k + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(IA, IS);
hence eval (((X+ a) `^ n),b) = (a + b) |^ n ; :: thesis: verum