theorem Th15: :: E_TRANS2:14

for f being Element of the carrier of (Polynom-Ring INT.Ring)
for i being Nat holds
( ((tau 0) *' f) . (i + 1) = f . i & ((tau 0) *' f) . 0 = 0. INT.Ring )