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

now :: thesis: for n being Nat st n in dom f holds
v1 . n = v2 . n

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

end;

hence v1 = v2 by A4, A6, A10, A8, A9, FINSEQ_1:13; :: thesis: verum