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
(LBZ1 (D,n,x,y)) /. 1 = ((D |^ n) . x) * (D . y)
let x, y be Element of R; :: thesis: for D being Derivation of R
for n being Nat st 1 <= n holds
(LBZ1 (D,n,x,y)) /. 1 = ((D |^ n) . x) * (D . y)
let D be Derivation of R; :: thesis: for n being Nat st 1 <= n holds
(LBZ1 (D,n,x,y)) /. 1 = ((D |^ n) . x) * (D . y)
let n be Nat; :: thesis: ( 1 <= n implies (LBZ1 (D,n,x,y)) /. 1 = ((D |^ n) . x) * (D . y) )
assume A1: n >= 1 ; :: thesis: (LBZ1 (D,n,x,y)) /. 1 = ((D |^ n) . x) * (D . y)
set p = LBZ (D,n,x,y);
set q = LBZ1 (D,n,x,y);
dom (LBZ1 (D,n,x,y)) = Seg (len (LBZ1 (D,n,x,y))) by FINSEQ_1:def 3
.= Seg n by Def6 ;
then A2: 1 in dom (LBZ1 (D,n,x,y)) by A1;
then (LBZ1 (D,n,x,y)) /. 1 = (LBZ1 (D,n,x,y)) . 1 by PARTFUN1:def 6
.= ((n choose (1 -' 1)) * ((D |^ ((n + 1) -' 1)) . x)) * ((D |^ 1) . y) by A2, Def6
.= ((n choose 0) * ((D |^ ((n + 1) -' 1)) . x)) * ((D |^ 1) . y) by XREAL_1:232
.= (1 * ((D |^ ((n + 1) -' 1)) . x)) * ((D |^ 1) . y) by NEWTON:19
.= ((D |^ ((n + 1) -' 1)) . x) * ((D |^ 1) . y) by BINOM:13
.= ((D |^ n) . x) * ((D |^ 1) . y) by NAT_D:34
.= ((D |^ n) . x) * (D . y) by VECTSP11:19 ;
hence (LBZ1 (D,n,x,y)) /. 1 = ((D |^ n) . x) * (D . y) ; :: thesis: verum