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 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; :: thesis: 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; :: thesis: 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; :: thesis: 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)) ; :: thesis: verum