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

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