deffunc H₁( Element of D) -> Element of X = F . (c,$1);
consider IT being Function such that
A1: ( dom IT = D & ( for d being Element of D holds IT . d = H₁(d) ) ) from FUNCT_1:sch 4();

now :: thesis: for d being object st d in D holds
IT . d in X

let d be object ; :: thesis: ( d in D implies IT . d in X )
assume A2: d in D ; :: thesis: IT . d in X
then A3: [c,d] in [:C,D:] by ZFMISC_1:87;
IT . d = F . (c,d) by A1, A2;
hence IT . d in X by A3, FUNCT_2:5; :: thesis: verum

end;

then reconsider IT = IT as Function of D,X by A1, FUNCT_2:3;
take IT ; :: thesis: for d being Element of D holds IT . d = F . (c,d)
let d be Element of D; :: thesis: IT . d = F . (c,d)
thus IT . d = F . (c,d) by A1; :: thesis: verum