for C being set
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