((product (doms F)) --> J) . f = J by FUNCOP_1:13;
hence G . f is Function of J,D ; :: thesis: verum