deffunc H_{1}( 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_{1}(n)
from FINSEQ_1:sch 2();

rng G c= the carrier of V

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

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

rng G c= the carrier of V

proof

then reconsider G = G as FinSequence of the carrier of V by FINSEQ_1:def 4;
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;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

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