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

proof

let i be Nat; :: thesis: ( ((tau 0) *' f) . (i + 1) = f . i & ((tau 0) *' f) . 0 = 0. INT.Ring )
A1: i in NAT by ORDINAL1:def 12;
tau 0 = <%(0. INT.Ring),(1. INT.Ring)%> `^ 1 by POLYNOM5:16
.= anpoly ((1. INT.Ring),1) by FIELD_1:12 ;
hence ( ((tau 0) *' f) . (i + 1) = f . i & ((tau 0) *' f) . 0 = 0. INT.Ring ) by A1, RINGDER1:31; :: thesis: verum

end;

hence for i being Nat holds
( ((tau 0) *' f) . (i + 1) = f . i & ((tau 0) *' f) . 0 = 0. INT.Ring ) ; :: thesis: verum