defpred S1[ object , object ] means ex D2 being set st
( D2 = \$2 & \$1 in D2 );
let P be mutually-disjoint set ; :: thesis: for x being Subset of () ex f being Function of x,P st
for a being object st a in x holds
a in f . a

let x be Subset of (); :: thesis: ex f being Function of x,P st
for a being object st a in x holds
a in f . a

A1: now :: thesis: for a being object st a in x holds
ex y being object st
( y in P & S1[a,y] )
let a be object ; :: thesis: ( a in x implies ex y being object st
( y in P & S1[a,y] ) )

assume a in x ; :: thesis: ex y being object st
( y in P & S1[a,y] )

then a in the carrier of () ;
then a in union P by Def7;
then ex y being set st
( a in y & y in P ) by TARSKI:def 4;
hence ex y being object st
( y in P & S1[a,y] ) ; :: thesis: verum
end;
consider f being Function of x,P such that
A2: for a being object st a in x holds
S1[a,f . a] from take f ; :: thesis: for a being object st a in x holds
a in f . a

let a be object ; :: thesis: ( a in x implies a in f . a )
assume a in x ; :: thesis: a in f . a
then S1[a,f . a] by A2;
hence a in f . a ; :: thesis: verum