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 = (ScProductDM L) . (v,((f . (F /. i)) * (F /. i))) ) & len f2 = len F & ( for i being Nat st i in dom f2 holds
f2 . i = (ScProductDM L) . (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 = (ScProductDM L) . (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 = (ScProductDM L) . (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 = (ScProductDM L) . (v,((f . (F /. i)) * (F /. i))) ) ) ; :: thesis: f1 = f2
A2: dom f1 = dom f2 by AS1, AS2, FINSEQ_3:29;
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 = (ScProductDM L) . (v,((f . (F /. k)) * (F /. k))) by AS1
.= f2 . k by AS2, A2, B1 ;
:: thesis: verum

end;

hence f1 = f2 by AS1, AS2, FINSEQ_3:29; :: thesis: verum