let R be non degenerated comRing; :: thesis: for x, y being Element of R
for D being Derivation of R
for n being Nat st 1 <= n holds
(LBZ2 (D,n,x,y)) /. n = (D . x) * ((D |^ n) . y)
let x, y be Element of R; :: thesis: for D being Derivation of R
for n being Nat st 1 <= n holds
(LBZ2 (D,n,x,y)) /. n = (D . x) * ((D |^ n) . y)
let D be Derivation of R; :: thesis: for n being Nat st 1 <= n holds
(LBZ2 (D,n,x,y)) /. n = (D . x) * ((D |^ n) . y)
let n be Nat; :: thesis: ( 1 <= n implies (LBZ2 (D,n,x,y)) /. n = (D . x) * ((D |^ n) . y) )
assume A1: n >= 1 ; :: thesis: (LBZ2 (D,n,x,y)) /. n = (D . x) * ((D |^ n) . y)
set p = LBZ (D,n,x,y);
set q = LBZ2 (D,n,x,y);
dom (LBZ2 (D,n,x,y)) = Seg (len (LBZ2 (D,n,x,y))) by FINSEQ_1:def 3
.= Seg n by Def7 ;
then A2: n in dom (LBZ2 (D,n,x,y)) by A1;
A3: (n + 1) -' n = (n + 1) - n by XREAL_1:233, NAT_1:12
.= 1 ;
(LBZ2 (D,n,x,y)) /. n = (LBZ2 (D,n,x,y)) . n by A2, PARTFUN1:def 6
.= ((n choose n) * ((D |^ ((n + 1) -' n)) . x)) * ((D |^ n) . y) by A2, Def7
.= (1 * ((D |^ ((n + 1) -' n)) . x)) * ((D |^ n) . y) by NEWTON:21
.= ((D |^ 1) . x) * ((D |^ n) . y) by A3, BINOM:13
.= (D . x) * ((D |^ n) . y) by VECTSP11:19 ;
hence (LBZ2 (D,n,x,y)) /. n = (D . x) * ((D |^ n) . y) ; :: thesis: verum