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) `2 ) & len v2 = len f & ( for n being Nat st n in dom v2 holds
v2 . n = (f /. n) `2 ) implies v1 = v2 )
assume that
A15: len v1 = len f and
A16: for n being Nat st n in dom v1 holds
v1 . n = (f /. n) `2 and
A17: len v2 = len f and
A18: for n being Nat st n in dom v2 holds
v2 . n = (f /. n) `2 ; :: thesis: v1 = v2
A19: dom v2 = Seg (len v2) by FINSEQ_1:def 3;
A20: dom f = Seg (len f) by FINSEQ_1:def 3;
A21: 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 A22: n in dom f ; :: thesis: v1 . n = v2 . n
hence v1 . n = (f /. n) `2 by A15, A16, A21, A20
.= v2 . n by A17, A18, A19, A20, A22 ;
:: thesis: verum

end;

hence v1 = v2 by A15, A17, A21, A19, A20, FINSEQ_1:13; :: thesis: verum