deffunc H₁( object ) -> set = rng (F₁() . $1);
consider p being XFinSequence such that
A1: len p = len F₁() and
A2: for k being Nat st k in len F₁() holds
p . k = H₁(k) from AFINSQ_1:sch 2();
for X being set st X in rng p holds
X is finite

proof

let X be set ; :: thesis: ( X in rng p implies X is finite )
assume A3: X in rng p ; :: thesis: X is finite
consider x being object such that
A4: ( x in dom p & p . x = X ) by A3, FUNCT_1:def 3;
p . x = H₁(x) by A1, A2, A4;
hence X is finite by A4; :: thesis: verum

end;

then A5: union (rng p) is finite by FINSET_1:7;
{ ((F₁() . i) . j) where i, j is Nat : P₁[i,j] } c= {0} \/ (union (rng p))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ((F₁() . i) . j) where i, j is Nat : P₁[i,j] } or x in {0} \/ (union (rng p)) )
assume x in { ((F₁() . i) . j) where i, j is Nat : P₁[i,j] } ; :: thesis: x in {0} \/ (union (rng p))
then consider i, j being Nat such that
A6: ( x = (F₁() . i) . j & P₁[i,j] ) ;

now :: thesis: ( not x in {0} implies x in union (rng p) )

assume not x in {0} ; :: thesis: x in union (rng p)
then A7: x <> 0 by TARSKI:def 1;
then j in dom (F₁() . i) by A6, FUNCT_1:def 2;
then A8: (F₁() . i) . j in rng (F₁() . i) by FUNCT_1:def 3;
F₁() . i <> {} by A6, A7;
then i in dom F₁() by FUNCT_1:def 2;
then ( F₁() . i in rng F₁() & p . i = H₁(i) & p . i in rng p ) by A1, A2, FUNCT_1:def 3;
hence x in union (rng p) by A8, A6, TARSKI:def 4; :: thesis: verum

end;

hence x in {0} \/ (union (rng p)) by XBOOLE_0:def 3; :: thesis: verum

end;

hence { ((F₁() . i) . j) where i, j is Nat : P₁[i,j] } is finite by A5; :: thesis: verum