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