set B = { F_{2}(x) where x is Element of F_{1}() : x in F_{1}() } ;

A1: { F_{2}(x) where x is Element of F_{1}() : P_{1}[x] } c= { F_{2}(x) where x is Element of F_{1}() : x in F_{1}() }
_{1}() is finite
;

{ F_{2}(x) where x is Element of F_{1}() : x in F_{1}() } is finite
from FRAENKEL:sch 21(A2);

hence { F_{2}(x) where x is Element of F_{1}() : P_{1}[x] } is finite
by A1; :: thesis: verum

A1: { F

proof

A2:
F
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { F_{2}(x) where x is Element of F_{1}() : P_{1}[x] } or a in { F_{2}(x) where x is Element of F_{1}() : x in F_{1}() } )

assume a in { F_{2}(x) where x is Element of F_{1}() : P_{1}[x] }
; :: thesis: a in { F_{2}(x) where x is Element of F_{1}() : x in F_{1}() }

then ex b being Element of F_{1}() st

( F_{2}(b) = a & P_{1}[b] )
;

hence a in { F_{2}(x) where x is Element of F_{1}() : x in F_{1}() }
; :: thesis: verum

end;assume a in { F

then ex b being Element of F

( F

hence a in { F

{ F

hence { F