theorem Th15: :: E_TRANS1:16

for R being comRing
for f being Element of the carrier of (Polynom-Ring R)
for i being Nat st i >= 1 & i is_at_least_length_of f & f . (i - 1) <> 0. R holds
len f = i