let C, C9, D, D9, E be 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))
let c be 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 c9 be 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 F be 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 C,D; 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; (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; verum