let C be set ; :: thesis: for A, B being non empty set
for F being PartFunc of C,A
for G being Function of A,B holds G * F is Function of (dom F),B
let A, B be non empty set ; :: thesis: for F being PartFunc of C,A
for G being Function of A,B holds G * F is Function of (dom F),B
let F be PartFunc of C,A; :: thesis: for G being Function of A,B holds G * F is Function of (dom F),B
let G be Function of A,B; :: thesis: G * F is Function of (dom F),B
dom G = A by FUNCT_2:def 1;
then rng F c= dom G by RELAT_1:def 19;
then A1: dom (G * F) = dom F by RELAT_1:27;
rng (G * F) c= B by RELAT_1:def 19;
hence G * F is Function of (dom F),B by A1, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum