defpred S_{1}[ object , object ] means ex A being set st

( A = $2 & $1 in A );

A3: for e being object st e in X holds

S_{1}[e,F . e]
from FUNCT_2:sch 1(A1);

take F ; :: thesis: for p being Element of X holds p in F . p

let p be Element of X; :: thesis: p in F . p

S_{1}[p,F . p]
by A3;

hence p in F . p ; :: thesis: verum

( A = $2 & $1 in A );

A1: now :: thesis: for e being object st e in X holds

ex u being object st

( u in D & S_{1}[e,u] )

consider F being Function of X,D such that ex u being object st

( u in D & S

A2:
union D = X
by Def4;

let e be object ; :: thesis: ( e in X implies ex u being object st

( u in D & S_{1}[e,u] ) )

assume e in X ; :: thesis: ex u being object st

( u in D & S_{1}[e,u] )

then ex u being set st

( e in u & u in D ) by A2, TARSKI:def 4;

hence ex u being object st

( u in D & S_{1}[e,u] )
; :: thesis: verum

end;let e be object ; :: thesis: ( e in X implies ex u being object st

( u in D & S

assume e in X ; :: thesis: ex u being object st

( u in D & S

then ex u being set st

( e in u & u in D ) by A2, TARSKI:def 4;

hence ex u being object st

( u in D & S

A3: for e being object st e in X holds

S

take F ; :: thesis: for p being Element of X holds p in F . p

let p be Element of X; :: thesis: p in F . p

S

hence p in F . p ; :: thesis: verum