deffunc H₁( Nat) -> Element of the carrier of V = (f . (F /. $1)) * (F /. $1);
consider G being FinSequence such that
A1: len G = len F and
A2: for n being Nat st n in dom G holds
G . n = H₁(n) from FINSEQ_1:sch 2();
rng G c= the carrier of V

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng G or x in the carrier of V )
assume x in rng G ; :: thesis: x in the carrier of V
then consider y being object such that
A3: y in dom G and
A4: G . y = x by FUNCT_1:def 3;
y in Seg (len F) by A1, A3, FINSEQ_1:def 3;
then reconsider y = y as Element of NAT ;
G . y = (f . (F /. y)) * (F /. y) by A2, A3;
hence x in the carrier of V by A4; :: thesis: verum

end;

then reconsider G = G as FinSequence of the carrier of V by FINSEQ_1:def 4;
take G ; :: thesis: ( len G = len F & ( for i being Nat st i in dom G holds
G . i = (f . (F /. i)) * (F /. i) ) )
thus ( len G = len F & ( for i being Nat st i in dom G holds
G . i = (f . (F /. i)) * (F /. i) ) ) by A1, A2; :: thesis: verum