  A syntactical proof is given that all functions definable in a certain affine
linear typed lambda-calculus with iteration in all types are polynomial time
computable. The proof provides explicit polynomial bounds that can easily be
calculated.
