For d>=k, (d/dt)^k E_d(lambda*t)=lambda^k E_(d-k)(lambda*t); for d<k the formal derivative is zero. Derivative means the finite coefficient-list operation.
Method: native-induction. Induction: k and polynomial degree. Risk: routine.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.