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

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

hence
H1 = H2
by A5, A7, FINSEQ_1:14; :: thesis: verumH1 . 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;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