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