theorem t3: :: FIELD_15:22

for R being commutative Ring
for p being Polynomial of R
for n being non zero Nat holds (p `^ n) . 0 = (p . 0) |^ n