let p1, p2 be sequence of L; :: thesis: ( ( 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)) ) ) ) & ( 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)) ) ) ) implies p1 = p2 )
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: p1 = p2

now :: thesis: for i being Element of NAT holds p1 . i = p2 . i

let i be Element of NAT ; :: thesis: p1 . i = p2 . i
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: for k being Nat st k in dom r1 holds
r1 . k = r2 . k

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

end;

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

end;

hence p1 = p2 ; :: thesis: verum