let C, C9, D, D9, E be non empty set ; :: thesis: 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))
let c be Element of C; :: thesis: 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))
let c9 be Element of C9; :: thesis: 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))
let F be Function of [:D,D9:],E; :: thesis: 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))
let f be Function of C,D; :: thesis: for g being Function of C9,D9 holds (F * (f,g)) . (c,c9) = F . ((f . c),(g . c9))
let g be Function of C9,D9; :: thesis: (F * (f,g)) . (c,c9) = F . ((f . c),(g . c9))
set H = F * (f,g);
F * (f,g) is Function of [:C,C9:],E by Th78;
then dom (F * (f,g)) = [:C,C9:] by FUNCT_2:def 1;
then [c,c9] in dom (F * (f,g)) by ZFMISC_1:def 2;
hence (F * (f,g)) . (c,c9) = F . ((f . c),(g . c9)) by Th77; :: thesis: verum