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 S1[ 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: S1[1] by VECTSP11:19;
A3: for n being non zero Nat st S1[n] holds
S1[n + 1]
proof
let n be non zero Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A4: S1[n] ; :: thesis: S1[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 S1[n + 1] ; :: thesis: verum
end;
for n being non zero Nat holds S1[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;