let it1, it2 be Polynomial of L; :: thesis: ( ( len p > 0 & (len it1) + 1 = len p & ( for i being Nat holds it1 . i = eval ((poly_shift (p,(i + 1))),r) ) & (len it2) + 1 = len p & ( for i being Nat holds it2 . i = eval ((poly_shift (p,(i + 1))),r) ) implies it1 = it2 ) & ( not len p > 0 & it1 = 0_. L & it2 = 0_. L implies it1 = it2 ) )

hereby :: thesis: ( not len p > 0 & it1 = 0_. L & it2 = 0_. L implies it1 = it2 )

assume len p > 0 ; :: thesis: ( (len it1) + 1 = len p & ( for i being Nat holds it1 . i = eval ((poly_shift (p,(i + 1))),r) ) & (len it2) + 1 = len p & ( for i being Nat holds it2 . i = eval ((poly_shift (p,(i + 1))),r) ) implies it1 = it2 )
assume that
A17: (len it1) + 1 = len p and
A18: for i being Nat holds it1 . i = eval ((poly_shift (p,(i + 1))),r) and
A19: (len it2) + 1 = len p and
A20: for i being Nat holds it2 . i = eval ((poly_shift (p,(i + 1))),r) ; :: thesis: it1 = it2

now :: thesis: for k being Nat st k < len it1 holds
it1 . k = it2 . k

let k be Nat; :: thesis: ( k < len it1 implies it1 . k = it2 . k )
assume k < len it1 ; :: thesis: it1 . k = it2 . k
thus it1 . k = eval ((poly_shift (p,(k + 1))),r) by A18
.= it2 . k by A20 ; :: thesis: verum

end;

hence it1 = it2 by A17, A19, ALGSEQ_1:12; :: thesis: verum

end;

thus ( not len p > 0 & it1 = 0_. L & it2 = 0_. L implies it1 = it2 ) ; :: thesis: verum