let R be non degenerated comRing; :: thesis: for n being Nat
for x, y being Element of R
for D being Derivation of R holds (D |^ n) . (x * y) = Sum (LBZ (D,n,x,y))
let n be Nat; :: thesis: for x, y being Element of R
for D being Derivation of R holds (D |^ n) . (x * y) = Sum (LBZ (D,n,x,y))
let x, y be Element of R; :: thesis: for D being Derivation of R holds (D |^ n) . (x * y) = Sum (LBZ (D,n,x,y))
let D be Derivation of R; :: thesis: (D |^ n) . (x * y) = Sum (LBZ (D,n,x,y))

per cases ( n <> 0 or n = 0 ) ;

suppose A1: n <> 0 ; :: thesis: (D |^ n) . (x * y) = Sum (LBZ (D,n,x,y))

defpred S₁[ Nat] means (D |^ $1) . (x * y) = Sum (LBZ (D,$1,x,y));
Sum (LBZ (D,1,x,y)) = Sum <*(y * (D . x)),(x * (D . y))*> by Th16
.= (Sum <*(y * (D . x))*>) + (x * (D . y)) by FVSUM_1:71
.= (y * (D . x)) + (x * (D . y)) by BINOM:3
.= D . (x * y) by Def1 ;
then A2: S₁[1] by VECTSP11:19;
A3: for n being non zero Nat st S₁[n] holds
S₁[n + 1]

proof

let n be non zero Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
reconsider k = n - 1 as Nat ;
(D |^ (n + 1)) . (x * y) = D . (Sum (LBZ (D,(k + 1),x,y))) by A4, Th9
.= Sum (LBZ (D,(k + 2),x,y)) by Th24
.= Sum (LBZ (D,(n + 1),x,y)) ;
hence S₁[n + 1] ; :: thesis: verum

end;

for n being non zero Nat holds S₁[n] from NAT_1:sch 10(A2, A3);
hence (D |^ n) . (x * y) = Sum (LBZ (D,n,x,y)) by A1; :: thesis: verum

end;

suppose A5: n = 0 ; :: thesis: (D |^ n) . (x * y) = Sum (LBZ (D,n,x,y))

Sum (LBZ (D,0,x,y)) = Sum <*(x * y)*> by Th15
.= (id R) . (x * y) by BINOM:3
.= (D |^ 0) . (x * y) by VECTSP11:18 ;
hence (D |^ n) . (x * y) = Sum (LBZ (D,n,x,y)) by A5; :: thesis: verum

end;

end;