let L be non empty ZeroStr ; :: thesis: for n being Element of NAT
for p being Polynomial of L st n >= len p holds
poly_shift (p,n) = 0_. L
let n be Element of NAT ; :: thesis: for p being Polynomial of L st n >= len p holds
poly_shift (p,n) = 0_. L
let p be Polynomial of L; :: thesis: ( n >= len p implies poly_shift (p,n) = 0_. L )
set ps = poly_shift (p,n);
assume A1: n >= len p ; :: thesis: poly_shift (p,n) = 0_. L

A2: now :: thesis: for z being object st z in dom (poly_shift (p,n)) holds
(poly_shift (p,n)) . z = 0. L

let z be object ; :: thesis: ( z in dom (poly_shift (p,n)) implies (poly_shift (p,n)) . z = 0. L )
assume z in dom (poly_shift (p,n)) ; :: thesis: (poly_shift (p,n)) . z = 0. L
then reconsider i = z as Element of NAT ;
thus (poly_shift (p,n)) . z = p . (n + i) by Def5
.= 0. L by A1, ALGSEQ_1:8, NAT_1:12 ; :: thesis: verum

end;

dom (poly_shift (p,n)) = NAT by FUNCT_2:def 1;
hence poly_shift (p,n) = 0_. L by A2, FUNCOP_1:11; :: thesis: verum