set R = F_Rat ;
set PR = Polynom-Ring F_Rat;
let n be Nat; :: thesis: for f being Element of the carrier of (Polynom-Ring F_Rat) holds n * f = (In (n,F_Rat)) * f
let f be Element of the carrier of (Polynom-Ring F_Rat); :: thesis: n * f = (In (n,F_Rat)) * f
defpred S₁[ Nat] means $1 * f = (In ($1,F_Rat)) * f;
A1: S₁[ 0 ]

proof

(In (0,F_Rat)) * f = 0_. F_Rat by POLYNOM5:26, GAUSSINT:def 14
.= 0. (Polynom-Ring F_Rat) by POLYNOM3:def 10 ;
hence S₁[ 0 ] by BINOM:12; :: thesis: verum

end;

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]
reconsider r = In (k,F_Rat) as Element of F_Rat ;
A4: In ((k + 1),F_Rat) = r + (1. F_Rat) by GAUSSINT:def 14;
A5: ((In (k,F_Rat)) * f) + f = (r * f) + ((1. F_Rat) * f)
.= (In ((k + 1),F_Rat)) * f by A4, POLYALG1:7 ;
((In (k,F_Rat)) * 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 A5; :: thesis: verum

end;

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