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

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

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

dom (poly_shift (p,n)) = NAT
by FUNCT_2:def 1;(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;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

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