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:18; :: thesis: verum