deffunc H₁( Nat) -> object = F₂(F₁(),$1);
set F = { H₁(i) where i is 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 Nat : ( i in dom 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 : ( 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 Nat : ( i in dom 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
A3: ( x = F₂(F₁(),i) & i in dom F₁() & P₁[i] ) ;
i in NAT by ORDINAL1:def 12;
hence x in { H₁(i) where i is Element of NAT : i in dom F₁() } by A3; :: 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 Nat : ( i in dom F₁() & P₁[i] ) } is finite by A1; :: thesis: verum