let p1, p2 be sequence of L; :: thesis:
assume that
A5: for i being Element of NAT ex r being FinSequence of the carrier of L st
( len r = i + 1 & p1 . i = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) and
A6: for i being Element of NAT ex r being FinSequence of the carrier of L st
( len r = i + 1 & p2 . i = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) ; :: thesis:

now :: thesis:

let i be Element of NAT ; :: thesis:
consider r1 being FinSequence of the carrier of L such that
A7: len r1 = i + 1 and
A8: p1 . i = Sum r1 and
A9: for k being Element of NAT st k in dom r1 holds
r1 . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by A5;
consider r2 being FinSequence of the carrier of L such that
A10: len r2 = i + 1 and
A11: p2 . i = Sum r2 and
A12: for k being Element of NAT st k in dom r2 holds
r2 . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by A6;
A13: dom r1 = Seg (len r2) by A7, A10, FINSEQ_1:def 3
.= dom r2 by FINSEQ_1:def 3 ;

now :: thesis:

let k be Nat; :: thesis:
assume A14: k in dom r1 ; :: thesis:
hence r1 . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by A9
.= r2 . k by A12, A13, A14 ;
:: thesis:

end;

hence p1 . i = p2 . i by A8, A11, A13, FINSEQ_1:13; :: thesis:

end;

hence p1 = p2 ; :: thesis: