let R be non degenerated comRing; :: thesis: for x, y being Element of R
for D being Derivation of R holds LBZ (D,0,x,y) = <*(x * y)*>
let x, y be Element of R; :: thesis: for D being Derivation of R holds LBZ (D,0,x,y) = <*(x * y)*>
let D be Derivation of R; :: thesis: LBZ (D,0,x,y) = <*(x * y)*>
A1: len (LBZ (D,0,x,y)) = 0 + 1 by Def4;
then dom (LBZ (D,0,x,y)) = Seg 1 by FINSEQ_1:def 3;
then A2: 1 in dom (LBZ (D,0,x,y)) ;
A3: 0 choose (1 -' 1) = 0 choose 0 by XREAL_1:232
.= 1 by NEWTON:19 ;
A4: 1 -' 1 = 0 by XREAL_1:232;
(LBZ (D,0,x,y)) . 1 = (1 * ((D |^ ((0 + 1) -' 1)) . x)) * ((D |^ (1 -' 1)) . y) by A3, A2, Def4
.= ((D |^ (0 + 0)) . x) * ((D |^ 0) . y) by A4, BINOM:13
.= ((D |^ 0) . x) * ((id R) . y) by VECTSP11:18
.= ((id R) . x) * ((id R) . y) by VECTSP11:18
.= x * y ;
hence LBZ (D,0,x,y) = <*(x * y)*> by A1, FINSEQ_1:40; :: thesis: verum