defpred S₁[ object , object ] means ex A being set st
( 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₁[e,u] )

A2: union D = X by Def4;
let e be object ; :: thesis: ( e in X implies ex u being object st
( u in D & S₁[e,u] ) )
assume e in X ; :: thesis: ex u being object st
( u in D & S₁[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₁[e,u] ) ; :: thesis: verum

end;

consider F being Function of X,D such that
A3: for e being object st e in X holds
S₁[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₁[p,F . p] by A3;
hence p in F . p ; :: thesis: verum