let R be non degenerated comRing; for n being Nat
for x, y being Element of R
for D being Derivation of R holds Sum ((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>) = ((((D |^ (n + 1)) . x) * y) + (Sum (LBZ0 (D,n,x,y)))) + (x * ((D |^ (n + 1)) . y))
let n be Nat; for x, y being Element of R
for D being Derivation of R holds Sum ((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>) = ((((D |^ (n + 1)) . x) * y) + (Sum (LBZ0 (D,n,x,y)))) + (x * ((D |^ (n + 1)) . y))
let x, y be Element of R; for D being Derivation of R holds Sum ((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>) = ((((D |^ (n + 1)) . x) * y) + (Sum (LBZ0 (D,n,x,y)))) + (x * ((D |^ (n + 1)) . y))
let D be Derivation of R; Sum ((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>) = ((((D |^ (n + 1)) . x) * y) + (Sum (LBZ0 (D,n,x,y)))) + (x * ((D |^ (n + 1)) . y))
set p1 = <*(((D |^ (n + 1)) . x) * y)*>;
set p2 = <*(x * ((D |^ (n + 1)) . y))*>;
set q = LBZ0 (D,n,x,y);
set r = (<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>;
set r1 = <*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y));
set r2 = (<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>;
set r3 = (LBZ0 (D,n,x,y)) ^ <*(x * ((D |^ (n + 1)) . y))*>;
A1:
Sum <*(((D |^ (n + 1)) . x) * y)*> = ((D |^ (n + 1)) . x) * y
by RLVECT_1:44;
(<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*> = <*(((D |^ (n + 1)) . x) * y)*> ^ ((LBZ0 (D,n,x,y)) ^ <*(x * ((D |^ (n + 1)) . y))*>)
by FINSEQ_1:32;
then Sum ((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>) =
(Sum <*(((D |^ (n + 1)) . x) * y)*>) + (Sum ((LBZ0 (D,n,x,y)) ^ <*(x * ((D |^ (n + 1)) . y))*>))
by RLVECT_1:41
.=
(((D |^ (n + 1)) . x) * y) + ((Sum (LBZ0 (D,n,x,y))) + (Sum <*(x * ((D |^ (n + 1)) . y))*>))
by A1, RLVECT_1:41
.=
(((D |^ (n + 1)) . x) * y) + ((Sum (LBZ0 (D,n,x,y))) + (x * ((D |^ (n + 1)) . y)))
by RLVECT_1:44
.=
((((D |^ (n + 1)) . x) * y) + (Sum (LBZ0 (D,n,x,y)))) + (x * ((D |^ (n + 1)) . y))
by RLVECT_1:def 3
;
hence
Sum ((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>) = ((((D |^ (n + 1)) . x) * y) + (Sum (LBZ0 (D,n,x,y)))) + (x * ((D |^ (n + 1)) . y))
; verum