let R be non degenerated comRing; :: thesis: for m being Nat
for x, y being Element of R
for D being Derivation of R holds LBZ0 (D,m,x,y) = (LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y))
let m be Nat; :: thesis: for x, y being Element of R
for D being Derivation of R holds LBZ0 (D,m,x,y) = (LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y))
let x, y be Element of R; :: thesis: for D being Derivation of R holds LBZ0 (D,m,x,y) = (LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y))
let D be Derivation of R; :: thesis: LBZ0 (D,m,x,y) = (LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y))
set p = LBZ1 (D,m,x,y);
set q = LBZ2 (D,m,x,y);
set r = LBZ0 (D,m,x,y);
A1: dom (LBZ1 (D,m,x,y)) = Seg (len (LBZ1 (D,m,x,y))) by FINSEQ_1:def 3
.= Seg m by Def6 ;
A2: dom (LBZ2 (D,m,x,y)) = Seg (len (LBZ2 (D,m,x,y))) by FINSEQ_1:def 3
.= Seg m by Def7 ;
A3: dom (LBZ0 (D,m,x,y)) = Seg (len (LBZ0 (D,m,x,y))) by FINSEQ_1:def 3
.= Seg m by Def5 ;
A4: dom ((LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y))) = Seg m by A1, BINOM:def 1;
A5: Seg (len ((LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y)))) = dom ((LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y))) by FINSEQ_1:def 3
.= dom (LBZ1 (D,m,x,y)) by BINOM:def 1
.= Seg (len (LBZ1 (D,m,x,y))) by FINSEQ_1:def 3
.= Seg m by Def6 ;
A6: len (LBZ0 (D,m,x,y)) = m by Def5
.= len ((LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y))) by A5, FINSEQ_1:6 ;
for k being Nat st 1 <= k & k <= len ((LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y))) holds
((LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y))) . k = (LBZ0 (D,m,x,y)) . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len ((LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y))) implies ((LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y))) . k = (LBZ0 (D,m,x,y)) . k )
assume A7: ( 1 <= k & k <= len ((LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y))) ) ; :: thesis: ((LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y))) . k = (LBZ0 (D,m,x,y)) . k
then A8: k in dom (LBZ1 (D,m,x,y)) by A1, A5;
then A9: (LBZ1 (D,m,x,y)) /. k = (LBZ1 (D,m,x,y)) . k by PARTFUN1:def 6
.= ((m choose (k -' 1)) * ((D |^ ((m + 1) -' k)) . x)) * ((D |^ k) . y) by A8, Def6 ;
A10: k in dom (LBZ2 (D,m,x,y)) by A2, A5, A7;
then A11: (LBZ2 (D,m,x,y)) /. k = (LBZ2 (D,m,x,y)) . k by PARTFUN1:def 6
.= ((m choose k) * ((D |^ ((m + 1) -' k)) . x)) * ((D |^ k) . y) by A10, Def7 ;
A12: k in dom (LBZ0 (D,m,x,y)) by A3, A5, A7;
k in dom ((LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y))) by A4, A5, A7;
then ((LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y))) . k = ((LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y))) /. k by PARTFUN1:def 6
.= (((m choose (k -' 1)) * ((D |^ ((m + 1) -' k)) . x)) * ((D |^ k) . y)) + (((m choose k) * ((D |^ ((m + 1) -' k)) . x)) * ((D |^ k) . y)) by A11, A9, A7, BINOM:def 1
.= ((m choose (k -' 1)) * (((D |^ ((m + 1) -' k)) . x) * ((D |^ k) . y))) + (((m choose k) * ((D |^ ((m + 1) -' k)) . x)) * ((D |^ k) . y)) by BINOM:19
.= ((m choose (k -' 1)) * (((D |^ ((m + 1) -' k)) . x) * ((D |^ k) . y))) + ((m choose k) * (((D |^ ((m + 1) -' k)) . x) * ((D |^ k) . y))) by BINOM:19
.= ((m choose (k -' 1)) + (m choose k)) * (((D |^ ((m + 1) -' k)) . x) * ((D |^ k) . y)) by BINOM:15
.= (((m choose (k -' 1)) + (m choose k)) * ((D |^ ((m + 1) -' k)) . x)) * ((D |^ k) . y) by BINOM:19
.= (LBZ0 (D,m,x,y)) . k by A12, Def5 ;
hence ((LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y))) . k = (LBZ0 (D,m,x,y)) . k ; :: thesis: verum

end;

hence LBZ0 (D,m,x,y) = (LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y)) by A6; :: thesis: verum