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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { H₁(i) where i is Element of NAT : ( i in dom 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 Element of NAT : ( i in dom F₂() & P₁[i] ) } ; :: thesis: x in { H₁(i) where i is Element of NAT : i in dom F₂() }
then ex i being Element of NAT st
( x = F₃(F₂(),i) & i in dom F₂() & P₁[i] ) ;
hence x in { H₁(i) where i is Element of NAT : i in dom F₂() } ; :: thesis: verum

end;

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