let f1, f2 be FinSequence of F_Real; :: thesis: ( len f1 = len F & ( for i being Nat st i in dom f1 holds
f1 . i = <;v,((f . (F /. i)) * (F /. i));> ) & len f2 = len F & ( for i being Nat st i in dom f2 holds
f2 . i = <;v,((f . (F /. i)) * (F /. i));> ) implies f1 = f2 )

assume AS1: ( len f1 = len F & ( for i being Nat st i in dom f1 holds
f1 . i = <;v,((f . (F /. i)) * (F /. i));> ) ) ; :: thesis: ( not len f2 = len F or ex i being Nat st
( i in dom f2 & not f2 . i = <;v,((f . (F /. i)) * (F /. i));> ) or f1 = f2 )

assume AS2: ( len f2 = len F & ( for i being Nat st i in dom f2 holds
f2 . i = <;v,((f . (F /. i)) * (F /. i));> ) ) ; :: thesis: f1 = f2
A2: dom f1 = dom f2 by ;
for k being Nat st k in dom f1 holds
f1 . k = f2 . k
proof
let k be Nat; :: thesis: ( k in dom f1 implies f1 . k = f2 . k )
assume B1: k in dom f1 ; :: thesis: f1 . k = f2 . k
hence f1 . k = <;v,((f . (F /. k)) * (F /. k));> by AS1
.= f2 . k by AS2, A2, B1 ;
:: thesis: verum
end;
hence f1 = f2 by ; :: thesis: verum