set B = { F2(x) where x is Element of F1() : x in F1() } ;
A1: { F2(x) where x is Element of F1() : P1[x] } c= { F2(x) where x is Element of F1() : x in F1() }
proof
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { F2(x) where x is Element of F1() : P1[x] } or a in { F2(x) where x is Element of F1() : x in F1() } )
assume a in { F2(x) where x is Element of F1() : P1[x] } ; :: thesis: a in { F2(x) where x is Element of F1() : x in F1() }
then ex b being Element of F1() st
( F2(b) = a & P1[b] ) ;
hence a in { F2(x) where x is Element of F1() : x in F1() } ; :: thesis: verum
end;
A2: F1() is finite ;
{ F2(x) where x is Element of F1() : x in F1() } is finite from FRAENKEL:sch 21(A2);
 hence { F2(x) where x is Element of F1() : P1[x] } is finite by A1; :: thesis: verum