deffunc H₁( Nat) -> Element of the carrier of G = (F /. $1) |^ (@ (I /. $1));
consider p being FinSequence such that
A1: len p = len F and
A2: for k being Nat st k in dom p holds
p . k = H₁(k) from FINSEQ_1:sch 2();
A3: dom p = dom F by A1, FINSEQ_3:29;
rng p c= the carrier of G

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng p or x in the carrier of G )
assume x in rng p ; :: thesis: x in the carrier of G
then consider y being object such that
A4: y in dom p and
A5: p . y = x by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A4;
x = (F /. y) |^ (@ (I /. y)) by A2, A4, A5;
hence x in the carrier of G ; :: thesis: verum

end;

then reconsider p = p as FinSequence of the carrier of G by FINSEQ_1:def 4;
take p ; :: thesis: ( len p = len F & ( for k being Nat st k in dom F holds
p . k = (F /. k) |^ (@ (I /. k)) ) )
thus ( len p = len F & ( for k being Nat st k in dom F holds
p . k = (F /. k) |^ (@ (I /. k)) ) ) by A1, A2, A3; :: thesis: verum