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

now :: thesis: for c being object st c in C holds
IT . c in X

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

end;

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