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

let x be set ; :: 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 Def6
.= p . x ; :: thesis: verum

end;

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