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 (LBZ0 (D,n,x,y)) = (Sum (LBZ1 (D,n,x,y))) + (Sum (LBZ2 (D,n,x,y)))
let n be Nat; :: thesis: for x, y being Element of R
for D being Derivation of R holds Sum (LBZ0 (D,n,x,y)) = (Sum (LBZ1 (D,n,x,y))) + (Sum (LBZ2 (D,n,x,y)))
let x, y be Element of R; :: thesis: for D being Derivation of R holds Sum (LBZ0 (D,n,x,y)) = (Sum (LBZ1 (D,n,x,y))) + (Sum (LBZ2 (D,n,x,y)))
let D be Derivation of R; :: thesis: Sum (LBZ0 (D,n,x,y)) = (Sum (LBZ1 (D,n,x,y))) + (Sum (LBZ2 (D,n,x,y)))
set p = LBZ1 (D,n,x,y);
set q = LBZ2 (D,n,x,y);
set r = LBZ0 (D,n,x,y);
A1: dom (LBZ1 (D,n,x,y)) = Seg (len (LBZ1 (D,n,x,y))) by FINSEQ_1:def 3
.= Seg n by Def6 ;
A2: dom (LBZ2 (D,n,x,y)) = Seg (len (LBZ2 (D,n,x,y))) by FINSEQ_1:def 3
.= Seg n by Def7 ;
Sum (LBZ0 (D,n,x,y)) = Sum ((LBZ1 (D,n,x,y)) + (LBZ2 (D,n,x,y))) by Th18
.= (Sum (LBZ1 (D,n,x,y))) + (Sum (LBZ2 (D,n,x,y))) by A1, A2, BINOM:7 ;
hence Sum (LBZ0 (D,n,x,y)) = (Sum (LBZ1 (D,n,x,y))) + (Sum (LBZ2 (D,n,x,y))) ; :: thesis: verum