:: deftheorem Def7 defines LBZ2 RINGDER1:def 7 :
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₆ = LBZ2 (D,m,x,y) iff ( len b₆ = m & ( for i being Nat st i in dom b₆ holds
b₆ . i = ((m choose i) * ((D |^ ((m + 1) -' i)) . x)) * ((D |^ i) . y) ) ) );