let L be non empty non degenerated multLoopStr_0 ; :: thesis: for n being Element of NAT
for p being Polynomial of L st n <= len p holds
(len (poly_shift (p,n))) + n = len p
let n be Element of NAT ; :: thesis: for p being Polynomial of L st n <= len p holds
(len (poly_shift (p,n))) + n = len p
let p be Polynomial of L; :: thesis: ( n <= len p implies (len (poly_shift (p,n))) + n = len p )
assume A1: n <= len p ; :: thesis: (len (poly_shift (p,n))) + n = len p
set ps = poly_shift (p,n);
set lpn = (len p) - n;
n - n <= (len p) - n by A1, XREAL_1:9;
then reconsider lpn = (len p) - n as Element of NAT by INT_1:3;

A2: now :: thesis: for m being Nat st m is_at_least_length_of poly_shift (p,n) holds
not lpn > m

let m be Nat; :: thesis: ( m is_at_least_length_of poly_shift (p,n) implies not lpn > m )
assume that
A3: m is_at_least_length_of poly_shift (p,n) and
A4: lpn > m ; :: thesis: contradiction
lpn >= m + 1 by A4, NAT_1:13;
then A5: lpn - 1 >= (m + 1) - 1 by XREAL_1:9;
then reconsider lpn1 = lpn - 1 as Element of NAT by INT_1:3;
(n + lpn1) + 1 = len p ;
then A6: p . (n + lpn1) <> 0. L by ALGSEQ_1:10;
(poly_shift (p,n)) . lpn1 = p . (n + lpn1) by Def5;
hence contradiction by A3, A5, A6, ALGSEQ_1:def 2; :: thesis: verum

end;

now :: thesis: for i being Nat st i >= lpn holds
(poly_shift (p,n)) . i = 0. L

let i be Nat; :: thesis: ( i >= lpn implies (poly_shift (p,n)) . i = 0. L )
assume i >= lpn ; :: thesis: (poly_shift (p,n)) . i = 0. L
then A7: i + n >= len p by XREAL_1:20;
thus (poly_shift (p,n)) . i = p . (n + i) by Def5
.= 0. L by A7, ALGSEQ_1:8 ; :: thesis: verum

end;

then lpn is_at_least_length_of poly_shift (p,n) by ALGSEQ_1:def 2;
hence (len (poly_shift (p,n))) + n = lpn + n by A2, ALGSEQ_1:def 3
.= len p ;
:: thesis: verum