deffunc H1( 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 = H1(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