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
.= 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 ;
:: thesis: verum
end;
hence p1 . i = p2 . i by ; :: thesis: verum
end;
hence p1 = p2 ; :: thesis: verum