:: deftheorem Def9 defines 'G' E_TRANS1:def 8 :
for f being Element of the carrier of (Polynom-Ring INT.Ring)
for b₂ being FinSequence of the carrier of (Polynom-Ring INT.Ring) holds
( b₂ = 'G' f iff ( len b₂ = len f & ( for i being Nat st i in dom b₂ holds
b₂ . i = ((Der1 INT.Ring) |^ (i -' 1)) . f ) ) );