let H1, H2 be FinSequence of the carrier of V; :: thesis: ( len H1 = len F & ( for i being Nat st i in dom H1 holds
H1 . i = (f . (F /. i)) * (F /. i) ) & len H2 = len F & ( for i being Nat st i in dom H2 holds
H2 . i = (f . (F /. i)) * (F /. i) ) implies H1 = H2 )
assume that
A5: len H1 = len F and
A6: for i being Nat st i in dom H1 holds
H1 . i = (f . (F /. i)) * (F /. i) and
A7: len H2 = len F and
A8: for i being Nat st i in dom H2 holds
H2 . i = (f . (F /. i)) * (F /. i) ; :: thesis: H1 = H2

now :: thesis: for k being Nat st 1 <= k & k <= len H1 holds
H1 . k = H2 . k

let k be Nat; :: thesis: ( 1 <= k & k <= len H1 implies H1 . k = H2 . k )
assume ( 1 <= k & k <= len H1 ) ; :: thesis: H1 . k = H2 . k
then A9: k in Seg (len H1) by FINSEQ_1:1;
then k in dom H1 by FINSEQ_1:def 3;
then A10: H1 . k = (f . (F /. k)) * (F /. k) by A6;
k in dom H2 by A5, A7, A9, FINSEQ_1:def 3;
hence H1 . k = H2 . k by A8, A10; :: thesis: verum

end;

hence H1 = H2 by A5, A7, FINSEQ_1:14; :: thesis: verum