set M = { x where x is Element of F₂() : ex w being Element of F₁() st
( P₁[w,x] & w in F₃() ) } ;
defpred S₁[ object , object ] means ( P₁[$1,$2] & $1 in F₃() & $2 in F₂() );
A3: for x, y being object st x in F₁() & S₁[x,y] holds
y in F₂() ;
A4: for x, y1, y2 being object st x in F₁() & S₁[x,y1] & S₁[x,y2] holds
y1 = y2 by A2;
consider f being PartFunc of F₁(),F₂() such that
A5: for x being object holds
( x in dom f iff ( x in F₁() & ex y being object st S₁[x,y] ) ) and
A6: for x being object st x in dom f holds
S₁[x,f . x] from PARTFUN1:sch 2(A3, A4);
{ x where x is Element of F₂() : ex w being Element of F₁() st
( P₁[w,x] & w in F₃() ) } = f .: F₃()

proof

thus { x where x is Element of F₂() : ex w being Element of F₁() st
( P₁[w,x] & w in F₃() ) } c= f .: F₃() :: according to XBOOLE_0:def 10 :: thesis: f .: F₃() c= { x where x is Element of F₂() : ex w being Element of F₁() st
( P₁[w,x] & w in F₃() ) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { x where x is Element of F₂() : ex w being Element of F₁() st
( P₁[w,x] & w in F₃() ) } or x in f .: F₃() )
assume x in { x where x is Element of F₂() : ex w being Element of F₁() st
( P₁[w,x] & w in F₃() ) } ; :: thesis: x in f .: F₃()
then consider u being Element of F₂() such that
A7: x = u and
A8: ex w being Element of F₁() st
( P₁[w,u] & w in F₃() ) ;
consider w being Element of F₁() such that
A9: P₁[w,u] and
A10: w in F₃() by A8;
A11: w in dom f by A5, A9, A10;
then S₁[w,f . w] by A6;
then f . w = x by A2, A7, A9;
hence x in f .: F₃() by A10, A11, FUNCT_1:def 6; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in f .: F₃() or x in { x where x is Element of F₂() : ex w being Element of F₁() st
( P₁[w,x] & w in F₃() ) } )
assume x in f .: F₃() ; :: thesis: x in { x where x is Element of F₂() : ex w being Element of F₁() st
( P₁[w,x] & w in F₃() ) }
then consider y being object such that
A12: y in dom f and
A13: y in F₃() and
A14: x = f . y by FUNCT_1:def 6;
reconsider x = x as Element of F₂() by A6, A12, A14;
P₁[y,x] by A6, A12, A14;
hence x in { x where x is Element of F₂() : ex w being Element of F₁() st
( P₁[w,x] & w in F₃() ) } by A12, A13; :: thesis: verum

end;

hence { x where x is Element of F₂() : ex w being Element of F₁() st
( P₁[w,x] & w in F₃() ) } is finite by A1; :: thesis: verum