defpred S₁[ set , set ] means for d being Element of D st F . ( the Id of C . $1) = the Id of D . d holds
$2 = d;
A2: for c being Element of C ex y being Element of D st S₁[c,y]

proof

let c be Element of C; :: thesis: ex y being Element of D st S₁[c,y]
consider y being Element of D such that
A3: F . ( the Id of C . c) = the Id of D . y by A1;
take y ; :: thesis: S₁[c,y]
let d be Element of D; :: thesis: ( F . ( the Id of C . c) = the Id of D . d implies y = d )
A4: ( id d = the Id of D . d & id y = the Id of D . y ) ;
assume F . ( the Id of C . c) = the Id of D . d ; :: thesis: y = d
hence y = d by A3, A4, Th45; :: thesis: verum

end;

thus ex f being Function of the carrier of C, the carrier of D st
for x being Element of C holds S₁[x,f . x] from FUNCT_2:sch 3(A2); :: thesis: verum