deffunc H1( object ) -> set = rng (F1() . $1);
consider p being XFinSequence such that
A1: len p = len F1() and
A2: for k being Nat st k in len F1() holds
p . k = H1(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 = H1(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;
{ ((F1() . i) . j) where i, j is Nat : P1[i,j] } c= {0} \/ (union (rng p))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ((F1() . i) . j) where i, j is Nat : P1[i,j] } or x in {0} \/ (union (rng p)) )
assume x in { ((F1() . i) . j) where i, j is Nat : P1[i,j] } ; :: thesis: x in {0} \/ (union (rng p))
then consider i, j being Nat such that
A6: ( x = (F1() . i) . j & P1[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 (F1() . i) by A6, FUNCT_1:def 2;
then A8: (F1() . i) . j in rng (F1() . i) by FUNCT_1:def 3;
F1() . i <> {} by A6, A7;
then i in dom F1() by FUNCT_1:def 2;
then ( F1() . i in rng F1() & p . i = H1(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 { ((F1() . i) . j) where i, j is Nat : P1[i,j] } is finite by A5; :: thesis: verum