let L be non empty ZeroStr ; :: thesis: for p being Polynomial of L holds poly_shift (p,0) = p
let p be Polynomial of L; :: thesis: poly_shift (p,0) = p
set ps = poly_shift (p,0);

now :: thesis: for x being object st x in NAT holds
(poly_shift (p,0)) . x = p . x

let x be object ; :: thesis: ( x in NAT implies (poly_shift (p,0)) . x = p . x )
assume x in NAT ; :: thesis: (poly_shift (p,0)) . x = p . x
then reconsider i = x as Element of NAT ;
thus (poly_shift (p,0)) . x = p . (0 + i) by Def5
.= p . x ; :: thesis: verum

end;

hence poly_shift (p,0) = p by FUNCT_2:12; :: thesis: verum