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

now

dom G = A by FUNCT_2:def 1;
then rng F c= dom G by RELAT_1:def 19;
hence dom (G * F) = dom F by RELAT_1:46; :: thesis: rng (G * F) c= B
thus rng (G * F) c= B by RELAT_1:def 19; :: thesis: verum

end;

hence G * F is Function of (dom F),B by FUNCT_2:def 1, RELSET_1:11; :: thesis: verum