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 * (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))
let n be Nat; :: thesis: for x, y being Element of R
for D being Derivation of R holds 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))
let x, y be Element of R; :: thesis: for D being Derivation of R holds 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))
let D be Derivation of R; :: thesis: 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))
set p = LBZ2 (D,(n + 1),x,y);
set q = LBZ1 (D,(n + 1),x,y);
set r = LBZ0 (D,n,x,y);
A1: len (LBZ2 (D,(n + 1),x,y)) = n + 1 by Def7;
A2: len (LBZ1 (D,(n + 1),x,y)) = n + 1 by Def6;
A3: 1 <= n + 1 by NAT_1:12;
then A4: n + 1 in dom (LBZ2 (D,(n + 1),x,y)) by A1, FINSEQ_3:25;
A5: 1 in dom (LBZ1 (D,(n + 1),x,y)) by A2, A3, FINSEQ_3:25;
set p1 = Del ((LBZ2 (D,(n + 1),x,y)),(n + 1));
set q1 = Del ((LBZ1 (D,(n + 1),x,y)),1);
set r1 = D * (LBZ0 (D,n,x,y));
A6: dom (Del ((LBZ2 (D,(n + 1),x,y)),(n + 1))) = Seg (len (Del ((LBZ2 (D,(n + 1),x,y)),(n + 1)))) by FINSEQ_1:def 3
.= Seg n by A1, A4, FINSEQ_3:109 ;
A7: dom (Del ((LBZ1 (D,(n + 1),x,y)),1)) = Seg (len (Del ((LBZ1 (D,(n + 1),x,y)),1))) by FINSEQ_1:def 3
.= Seg n by A2, A5, FINSEQ_3:109 ;
reconsider p1 = Del ((LBZ2 (D,(n + 1),x,y)),(n + 1)), p = LBZ2 (D,(n + 1),x,y), q1 = Del ((LBZ1 (D,(n + 1),x,y)),1), q = LBZ1 (D,(n + 1),x,y) as FinSequence of R ;
len p >= 1 by NAT_1:12, A1;
then A8: len p in dom p by FINSEQ_3:25;
reconsider a = p . (len p) as Element of R by A8, FINSEQ_2:11;
A9: a = (LBZ2 (D,(n + 1),x,y)) /. (n + 1) by A1, A8, PARTFUN1:def 6;
len q >= 1 by NAT_1:12, A2;
then A10: 1 in dom q by FINSEQ_3:25;
then reconsider b = q . 1 as Element of R by FINSEQ_2:11;
A11: b = (LBZ1 (D,(n + 1),x,y)) /. 1 by A10, PARTFUN1:def 6;
p <> {} by Def7;
then A13: Sum p = Sum (p1 ^ <*a*>) by A1, PRE_POLY:13
.= (Sum p1) + (Sum <*a*>) by RLVECT_1:41
.= (Sum p1) + a by BINOM:3 ;
q <> {} by Def6;
then A15: Sum q = Sum (<*b*> ^ q1) by FINSEQ_5:86
.= (Sum <*b*>) + (Sum q1) by RLVECT_1:41
.= b + (Sum q1) by BINOM:3 ;
Sum (D * (LBZ0 (D,n,x,y))) = Sum (p1 + q1) by Th20
.= (Sum p1) + (Sum q1) by A6, A7, BINOM:7
.= ((Sum p) - a) + (Sum q1) by A13, VECTSP_2:2
.= ((Sum p) + (- a)) + ((Sum q) - b) by A15, VECTSP_2:2
.= (((Sum p) + (- a)) + (Sum q)) - b by RLVECT_1:def 3
.= (- b) + (((Sum p) + (Sum q)) - a) by RLVECT_1:def 3
.= ((- ((LBZ1 (D,(n + 1),x,y)) /. 1)) + ((Sum p) + (Sum q))) - ((LBZ2 (D,(n + 1),x,y)) /. (n + 1)) by A9, A11, RLVECT_1:def 3 ;
hence 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 Th19; :: thesis: verum