:: deftheorem Def6 defines LBZ1 RINGDER1:def 6 :
for R being non degenerated comRing
for D being Derivation of R
for m being Nat
for x, y being Element of R
for b₆ being FinSequence of the carrier of R holds
( b₆ = LBZ1 (D,m,x,y) iff ( len b₆ = m & ( for i being Nat st i in dom b₆ holds
b₆ . i = ((m choose (i -' 1)) * ((D |^ ((m + 1) -' i)) . x)) * ((D |^ i) . y) ) ) );