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
A18: ( (len it1) + 1 = len p & ( for i being Nat holds it1 . i = eval (poly_shift p,(i + 1)),r ) ) and
A19: ( (len it2) + 1 = len p & ( for i being Nat holds it2 . i = eval (poly_shift p,(i + 1)),r ) ) ; :: thesis: it1 = it2

now

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 A19 ; :: thesis: verum

end;

hence it1 = it2 by A18, A19, ALGSEQ_1:28; :: thesis: verum

end;

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