let z1, z2 be FinSequence of L; :: thesis: ( len z1 = len F & ( for j being Element of NAT st j in dom z1 holds
ex p being Polynomial of L st
( p = F . j & z1 . j = p . i ) ) & len z2 = len F & ( for j being Element of NAT st j in dom z2 holds
ex p being Polynomial of L st
( p = F . j & z2 . j = p . i ) ) implies z1 = z2 )
assume A4: ( len z1 = len F & ( for j being Element of NAT st j in dom z1 holds
ex p being Polynomial of L st
( p = F . j & z1 . j = p . i ) ) ) ; :: thesis: ( not len z2 = len F or ex j being Element of NAT st
( j in dom z2 & ( for p being Polynomial of L holds
( not p = F . j or not z2 . j = p . i ) ) ) or z1 = z2 )
assume A5: ( len z2 = len F & ( for j being Element of NAT st j in dom z2 holds
ex p being Polynomial of L st
( p = F . j & z2 . j = p . i ) ) ) ; :: thesis: z1 = z2
A6: dom z1 = Seg (len F) by A4, FINSEQ_1:def 3
.= dom z2 by A5, FINSEQ_1:def 3 ;

now

let k be Nat; :: thesis: ( k in dom z1 implies z1 . k = z2 . k )
assume A7: k in dom z1 ; :: thesis: z1 . k = z2 . k
then consider p1 being Polynomial of L such that
A8: ( p1 = F . k & z1 . k = p1 . i ) by A4;
consider p2 being Polynomial of L such that
A9: ( p2 = F . k & z2 . k = p2 . i ) by A5, A6, A7;
thus z1 . k = z2 . k by A8, A9; :: thesis: verum

end;

hence z1 = z2 by A6, FINSEQ_1:17; :: thesis: verum