let R be non degenerated comRing; :: thesis: for D being Derivation of R
for n being Nat
for x being Element of R holds D . (n * x) = n * (D . x)
let D be Derivation of R; :: thesis: for n being Nat
for x being Element of R holds D . (n * x) = n * (D . x)
let n be Nat; :: thesis: for x being Element of R holds D . (n * x) = n * (D . x)
let x be Element of R; :: thesis: D . (n * x) = n * (D . x)
defpred S₁[ Nat] means D . ($1 * x) = $1 * (D . x);
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]
D . ((n + 1) * x) = D . ((n * x) + (1 * x)) by BINOM:15
.= (D . (n * x)) + (D . (1 * x)) by Def1
.= (D . (n * x)) + (D . x) by BINOM:13
.= (n * (D . x)) + (1 * (D . x)) by A2, BINOM:13
.= (n + 1) * (D . x) by BINOM:15 ;
hence S₁[n + 1] ; :: thesis: verum

end;

0 * (D . x) = 0. R by BINOM:12
.= D . (0. R) by Th5
.= D . (0 * x) by BINOM:12 ;
then A3: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A1);
hence D . (n * x) = n * (D . x) ; :: thesis: verum