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