defpred S1[ Object of C, Object of D] means for d being Element of D st F . (id $1) = id d holds
$2 = d;
A2: for c being Element of C ex y being Element of D st S1[c,y]
proof
let c be Element of C; :: thesis: ex y being Element of D st S1[c,y]
consider y being Element of D such that
A3: F . (id c) = id y by A1;
take y ; :: thesis: S1[c,y]
let d be Element of D; :: thesis: ( F . (id c) = id d implies y = d )
assume F . (id c) = id d ; :: thesis: y = d
hence y = d by A3, Th54; :: 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 S1[x,f . x] from FUNCT_2:sch 3(A2); :: thesis: verum