set M = { x where x is Element of F_{2}() : ex w being Element of F_{1}() st

( P_{1}[w,x] & w in F_{3}() ) } ;

defpred S_{1}[ object , object ] means ( P_{1}[$1,$2] & $1 in F_{3}() & $2 in F_{2}() );

A3: for x, y being object st x in F_{1}() & S_{1}[x,y] holds

y in F_{2}()
;

A4: for x, y1, y2 being object st x in F_{1}() & S_{1}[x,y1] & S_{1}[x,y2] holds

y1 = y2 by A2;

consider f being PartFunc of F_{1}(),F_{2}() such that

A5: for x being object holds

( x in dom f iff ( x in F_{1}() & ex y being object st S_{1}[x,y] ) )
and

A6: for x being object st x in dom f holds

S_{1}[x,f . x]
from PARTFUN1:sch 2(A3, A4);

{ x where x is Element of F_{2}() : ex w being Element of F_{1}() st

( P_{1}[w,x] & w in F_{3}() ) } = f .: F_{3}()
_{2}() : ex w being Element of F_{1}() st

( P_{1}[w,x] & w in F_{3}() ) } is finite
by A1; :: thesis: verum

( P

defpred S

A3: for x, y being object st x in F

y in F

A4: for x, y1, y2 being object st x in F

y1 = y2 by A2;

consider f being PartFunc of F

A5: for x being object holds

( x in dom f iff ( x in F

A6: for x being object st x in dom f holds

S

{ x where x is Element of F

( P

proof

hence
{ x where x is Element of F
thus
{ x where x is Element of F_{2}() : ex w being Element of F_{1}() st

( P_{1}[w,x] & w in F_{3}() ) } c= f .: F_{3}()
:: according to XBOOLE_0:def 10 :: thesis: f .: F_{3}() c= { x where x is Element of F_{2}() : ex w being Element of F_{1}() st

( P_{1}[w,x] & w in F_{3}() ) } _{3}() or x in { x where x is Element of F_{2}() : ex w being Element of F_{1}() st

( P_{1}[w,x] & w in F_{3}() ) } )

assume x in f .: F_{3}()
; :: thesis: x in { x where x is Element of F_{2}() : ex w being Element of F_{1}() st

( P_{1}[w,x] & w in F_{3}() ) }

then consider y being object such that

A12: y in dom f and

A13: y in F_{3}()
and

A14: x = f . y by FUNCT_1:def 6;

reconsider x = x as Element of F_{2}() by A6, A12, A14;

P_{1}[y,x]
by A6, A12, A14;

hence x in { x where x is Element of F_{2}() : ex w being Element of F_{1}() st

( P_{1}[w,x] & w in F_{3}() ) }
by A12, A13; :: thesis: verum

end;( P

( P

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in f .: F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { x where x is Element of F_{2}() : ex w being Element of F_{1}() st

( P_{1}[w,x] & w in F_{3}() ) } or x in f .: F_{3}() )

assume x in { x where x is Element of F_{2}() : ex w being Element of F_{1}() st

( P_{1}[w,x] & w in F_{3}() ) }
; :: thesis: x in f .: F_{3}()

then consider u being Element of F_{2}() such that

A7: x = u and

A8: ex w being Element of F_{1}() st

( P_{1}[w,u] & w in F_{3}() )
;

consider w being Element of F_{1}() such that

A9: P_{1}[w,u]
and

A10: w in F_{3}()
by A8;

A11: w in dom f by A5, A9, A10;

then S_{1}[w,f . w]
by A6;

then f . w = x by A2, A7, A9;

hence x in f .: F_{3}()
by A10, A11, FUNCT_1:def 6; :: thesis: verum

end;( P

assume x in { x where x is Element of F

( P

then consider u being Element of F

A7: x = u and

A8: ex w being Element of F

( P

consider w being Element of F

A9: P

A10: w in F

A11: w in dom f by A5, A9, A10;

then S

then f . w = x by A2, A7, A9;

hence x in f .: F

( P

assume x in f .: F

( P

then consider y being object such that

A12: y in dom f and

A13: y in F

A14: x = f . y by FUNCT_1:def 6;

reconsider x = x as Element of F

P

hence x in { x where x is Element of F

( P

( P