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 that
A4: len z1 = len F and
A5: 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 that
A6: len z2 = len F and
A7: 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
A8: dom z1 = Seg (len F) by A4, FINSEQ_1:def 3
.= dom z2 by A6, FINSEQ_1:def 3 ;
now :: thesis: for k being Nat st k in dom z1 holds
z1 . k = z2 . k
let k be Nat; :: thesis: ( k in dom z1 implies z1 . k = z2 . k )
assume A9: k in dom z1 ; :: thesis: z1 . k = z2 . k
then A10: ex p1 being Polynomial of L st
( p1 = F . k & z1 . k = p1 . i ) by A5;
ex p2 being Polynomial of L st
( p2 = F . k & z2 . k = p2 . i ) by A7, A8, A9;
hence z1 . k = z2 . k by A10; :: thesis: verum
end;
hence z1 = z2 by A8, FINSEQ_1:13; :: thesis: verum