let R be non degenerated comRing; for n being Nat
for x, y being Element of R
for D being Derivation of R holds D . (Sum (LBZ (D,(n + 1),x,y))) = Sum (LBZ (D,(n + 2),x,y))
let n be Nat; for x, y being Element of R
for D being Derivation of R holds D . (Sum (LBZ (D,(n + 1),x,y))) = Sum (LBZ (D,(n + 2),x,y))
let x, y be Element of R; for D being Derivation of R holds D . (Sum (LBZ (D,(n + 1),x,y))) = Sum (LBZ (D,(n + 2),x,y))
let D be Derivation of R; D . (Sum (LBZ (D,(n + 1),x,y))) = Sum (LBZ (D,(n + 2),x,y))
set p1 = <*(((D |^ (n + 1)) . x) * y)*>;
set p2 = LBZ0 (D,n,x,y);
set p3 = <*(x * ((D |^ (n + 1)) . y))*>;
set q = LBZ (D,(n + 1),x,y);
A1: D . (((D |^ (n + 1)) . x) * y) =
((D . ((D |^ (n + 1)) . x)) * y) + (((D |^ (n + 1)) . x) * (D . y))
by Def1
.=
(((D |^ ((n + 1) + 1)) . x) * y) + (((D |^ (n + 1)) . x) * (D . y))
by Th9
;
A2: D . (x * ((D |^ (n + 1)) . y)) =
((D . x) * ((D |^ (n + 1)) . y)) + (x * (D . ((D |^ (n + 1)) . y)))
by Def1
.=
((D . x) * ((D |^ (n + 1)) . y)) + (x * ((D |^ ((n + 1) + 1)) . y))
by Th9
;
A3: Sum (D * (LBZ0 (D,n,x,y))) =
((- ((LBZ1 (D,(n + 1),x,y)) /. 1)) + (Sum (LBZ0 (D,(n + 1),x,y)))) - ((LBZ2 (D,(n + 1),x,y)) /. (n + 1))
by Th21
.=
((- (((D |^ (n + 1)) . x) * (D . y))) + (Sum (LBZ0 (D,(n + 1),x,y)))) - ((LBZ2 (D,(n + 1),x,y)) /. (n + 1))
by NAT_1:12, Lm1
.=
((- (((D |^ (n + 1)) . x) * (D . y))) + (Sum (LBZ0 (D,(n + 1),x,y)))) - ((D . x) * ((D |^ (n + 1)) . y))
by NAT_1:12, Lm2
;
D . (Sum (LBZ (D,(n + 1),x,y))) =
Sum (D * (LBZ (D,(n + 1),x,y)))
by Th11
.=
Sum (D * ((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>))
by Th22
.=
Sum ((D * (<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y)))) ^ (D * <*(x * ((D |^ (n + 1)) . y))*>))
by FINSEQOP:9
.=
(Sum (D * (<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))))) + (Sum (D * <*(x * ((D |^ (n + 1)) . y))*>))
by RLVECT_1:41
.=
(Sum ((D * <*(((D |^ (n + 1)) . x) * y)*>) ^ (D * (LBZ0 (D,n,x,y))))) + (Sum (D * <*(x * ((D |^ (n + 1)) . y))*>))
by FINSEQOP:9
.=
((Sum (D * <*(((D |^ (n + 1)) . x) * y)*>)) + (Sum (D * (LBZ0 (D,n,x,y))))) + (Sum (D * <*(x * ((D |^ (n + 1)) . y))*>))
by RLVECT_1:41
.=
((Sum <*(D . (((D |^ (n + 1)) . x) * y))*>) + (Sum (D * (LBZ0 (D,n,x,y))))) + (Sum (D * <*(x * ((D |^ (n + 1)) . y))*>))
by FINSEQ_2:35
.=
((D . (((D |^ (n + 1)) . x) * y)) + (Sum (D * (LBZ0 (D,n,x,y))))) + (Sum (D * <*(x * ((D |^ (n + 1)) . y))*>))
by BINOM:3
.=
((D . (((D |^ (n + 1)) . x) * y)) + (Sum (D * (LBZ0 (D,n,x,y))))) + (Sum <*(D . (x * ((D |^ (n + 1)) . y)))*>)
by FINSEQ_2:35
.=
(((((D |^ ((n + 1) + 1)) . x) * y) + (((D |^ (n + 1)) . x) * (D . y))) + (((- (((D |^ (n + 1)) . x) * (D . y))) + (Sum (LBZ0 (D,(n + 1),x,y)))) - ((D . x) * ((D |^ (n + 1)) . y)))) + (D . (x * ((D |^ (n + 1)) . y)))
by A3, A1, BINOM:3
.=
(((((D |^ ((n + 1) + 1)) . x) * y) + (((D |^ (n + 1)) . x) * (D . y))) + ((- (((D |^ (n + 1)) . x) * (D . y))) + ((Sum (LBZ0 (D,(n + 1),x,y))) - ((D . x) * ((D |^ (n + 1)) . y))))) + (D . (x * ((D |^ (n + 1)) . y)))
by RLVECT_1:def 3
.=
((((((D |^ ((n + 1) + 1)) . x) * y) + (((D |^ (n + 1)) . x) * (D . y))) - (((D |^ (n + 1)) . x) * (D . y))) + ((Sum (LBZ0 (D,(n + 1),x,y))) - ((D . x) * ((D |^ (n + 1)) . y)))) + (D . (x * ((D |^ (n + 1)) . y)))
by RLVECT_1:def 3
.=
(((((D |^ ((n + 1) + 1)) . x) * y) + ((((D |^ (n + 1)) . x) * (D . y)) - (((D |^ (n + 1)) . x) * (D . y)))) + ((Sum (LBZ0 (D,(n + 1),x,y))) - ((D . x) * ((D |^ (n + 1)) . y)))) + (D . (x * ((D |^ (n + 1)) . y)))
by RLVECT_1:def 3
.=
(((((D |^ ((n + 1) + 1)) . x) * y) + (0. R)) + ((Sum (LBZ0 (D,(n + 1),x,y))) - ((D . x) * ((D |^ (n + 1)) . y)))) + (D . (x * ((D |^ (n + 1)) . y)))
by RLVECT_1:15
.=
(((((D |^ ((n + 1) + 1)) . x) * y) + (Sum (LBZ0 (D,(n + 1),x,y)))) + (- ((D . x) * ((D |^ (n + 1)) . y)))) + (((D . x) * ((D |^ (n + 1)) . y)) + (x * ((D |^ ((n + 1) + 1)) . y)))
by A2, RLVECT_1:def 3
.=
((((D |^ ((n + 1) + 1)) . x) * y) + (Sum (LBZ0 (D,(n + 1),x,y)))) + ((- ((D . x) * ((D |^ (n + 1)) . y))) + (((D . x) * ((D |^ (n + 1)) . y)) + (x * ((D |^ ((n + 1) + 1)) . y))))
by RLVECT_1:def 3
.=
((((D |^ ((n + 1) + 1)) . x) * y) + (Sum (LBZ0 (D,(n + 1),x,y)))) + (((- ((D . x) * ((D |^ (n + 1)) . y))) + ((D . x) * ((D |^ (n + 1)) . y))) + (x * ((D |^ ((n + 1) + 1)) . y)))
by RLVECT_1:def 3
.=
((((D |^ ((n + 1) + 1)) . x) * y) + (Sum (LBZ0 (D,(n + 1),x,y)))) + ((0. R) + (x * ((D |^ ((n + 1) + 1)) . y)))
by RLVECT_1:5
.=
Sum ((<*(((D |^ ((n + 1) + 1)) . x) * y)*> ^ (LBZ0 (D,(n + 1),x,y))) ^ <*(x * ((D |^ ((n + 1) + 1)) . y))*>)
by Th23
.=
Sum (LBZ (D,((n + 1) + 1),x,y))
by Th22
;
hence
D . (Sum (LBZ (D,(n + 1),x,y))) = Sum (LBZ (D,(n + 2),x,y))
; verum