set R = INT.Ring ;
set PR = Polynom-Ring INT.Ring;
let n be Nat; :: thesis: for f being Element of the carrier of (Polynom-Ring INT.Ring) holds n * f = (In (n,INT.Ring)) * f
let f be Element of the carrier of (Polynom-Ring INT.Ring); :: thesis: n * f = (In (n,INT.Ring)) * f
defpred S₁[ Nat] means $1 * f = (In ($1,INT.Ring)) * f;
(In (0,INT.Ring)) * f = 0_. INT.Ring by POLYNOM5:26
.= 0. (Polynom-Ring INT.Ring) by POLYNOM3:def 10 ;
then A1: S₁[ 0 ] by BINOM:12;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
set r = In (k,INT.Ring);
A4: ((In (k,INT.Ring)) * f) + f = ((In (k,INT.Ring)) * f) + ((1. INT.Ring) * f) by POLYALG1:9
.= ((In (k,INT.Ring)) + (1. INT.Ring)) * f by POLYALG1:7
.= (In ((k + 1),INT.Ring)) * f ;
((In (k,INT.Ring)) * f) + f = (k * f) + f by A3, POLYNOM3:def 10
.= (k * f) + (1 * f) by BINOM:13
.= (k + 1) * f by BINOM:15 ;
hence S₁[k + 1] by A4; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
hence n * f = (In (n,INT.Ring)) * f ; :: thesis: verum