let v1, v2 be FinSequence of REAL ; :: thesis: ( len v1 = len f & ( for n being Element of NAT st n in dom v1 holds
v1 . n = (f /. n) `1 ) & len v2 = len f & ( for n being Element of NAT st n in dom v2 holds
v2 . n = (f /. n) `1 ) implies v1 = v2 )
assume that
A4: ( len v1 = len f & ( for n being Element of NAT st n in dom v1 holds
v1 . n = (f /. n) `1 ) ) and
A5: ( len v2 = len f & ( for n being Element of NAT st n in dom v2 holds
v2 . n = (f /. n) `1 ) ) ; :: thesis: v1 = v2
A6: ( dom v1 = Seg (len v1) & dom v2 = Seg (len v2) & dom f = Seg (len f) ) by FINSEQ_1:def 3;

now

let n be Nat; :: thesis: ( n in dom f implies v1 . n = v2 . n )
assume A7: n in dom f ; :: thesis: v1 . n = v2 . n
hence v1 . n = (f /. n) `1 by A4, A6
.= v2 . n by A5, A6, A7 ;
:: thesis: verum

end;

hence v1 = v2 by A4, A5, A6, FINSEQ_1:17; :: thesis: verum