theorem Th78: :: FINSEQOP:79

for C, C9, D, D9, E being non empty set
for F being Function of [:D,D9:],E
for f being Function of C,D
for g being Function of C9,D9 holds F * (f,g) is Function of [:C,C9:],E