theorem Th80: :: FINSEQOP:81

for C, C9, D, D9, E being non empty set
for c being Element of C
for c9 being Element of C9
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)) . (c,c9) = F . ((f . c),(g . c9))