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;

hence (len (poly_shift (p,n))) + n = lpn + n by A2, ALGSEQ_1:def 3

.= len p ;

:: thesis: verum

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

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

now :: thesis: for i being Nat st i >= lpn holds

(poly_shift (p,n)) . i = 0. L

then
lpn is_at_least_length_of poly_shift (p,n)
by ALGSEQ_1:def 2;(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;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

hence (len (poly_shift (p,n))) + n = lpn + n by A2, ALGSEQ_1:def 3

.= len p ;

:: thesis: verum