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);

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

hence
poly_shift (p,0) = p
by FUNCT_2:12; :: thesis: verum(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;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