deffunc H₁( Nat) -> object = F₂(F₁(),$1);
set F = { H₁(i) where i is Nat : ( 1 <= i & i <= len F₁() & P₁[i] ) } ;
set F9 = { H₁(i) where i is Element of NAT : i in dom F₁() } ;
A1: { H₁(i) where i is Nat : ( 1 <= i & i <= len F₁() & P₁[i] ) } c= { H₁(i) where i is Element of NAT : i in dom F₁() }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { H₁(i) where i is Nat : ( 1 <= i & i <= len F₁() & P₁[i] ) } or x in { H₁(i) where i is Element of NAT : i in dom F₁() } )
assume x in { H₁(i) where i is Nat : ( 1 <= i & i <= len F₁() & P₁[i] ) } ; :: thesis: x in { H₁(i) where i is Element of NAT : i in dom F₁() }
then consider i being Nat such that
A2: x = F₂(F₁(),i) and
A3: ( 1 <= i & i <= len F₁() ) and
P₁[i] ;
i in dom F₁() by A3, FINSEQ_3:25;
hence x in { H₁(i) where i is Element of NAT : i in dom F₁() } by A2; :: thesis: verum

end;

A4: dom F₁() is finite ;
{ H₁(i) where i is Element of NAT : i in dom F₁() } is finite from FRAENKEL:sch 21(A4);
hence { F₂(F₁(),i) where i is Nat : ( 1 <= i & i <= len F₁() & P₁[i] ) } is finite by A1; :: thesis: verum