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

( 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

hence
p1 = p2
; :: thesis: verumlet 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 ;

end;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

hence
p1 . i = p2 . i
by A8, A11, A13, FINSEQ_1:13; :: thesis: verumr1 . 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;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