let D, D', E, C, C' be non empty set ; :: thesis: for c being Element of C
for c' being Element of C'
for F being Function of [:D,D':],E
for f being Function of C,D
for g being Function of C',D' holds (F * f,g) . c,c' = F . (f . c),(g . c')
let c be Element of C; :: thesis: for c' being Element of C'
for F being Function of [:D,D':],E
for f being Function of C,D
for g being Function of C',D' holds (F * f,g) . c,c' = F . (f . c),(g . c')
let c' be Element of C'; :: thesis: for F being Function of [:D,D':],E
for f being Function of C,D
for g being Function of C',D' holds (F * f,g) . c,c' = F . (f . c),(g . c')
let F be Function of [:D,D':],E; :: thesis: for f being Function of C,D
for g being Function of C',D' holds (F * f,g) . c,c' = F . (f . c),(g . c')
let f be Function of C,D; :: thesis: for g being Function of C',D' holds (F * f,g) . c,c' = F . (f . c),(g . c')
let g be Function of C',D'; :: thesis: (F * f,g) . c,c' = F . (f . c),(g . c')
set H = F * f,g;
F * f,g is Function of [:C,C':],E by Th84;
then ( dom (F * f,g) = [:C,C':] & c in C & c' in C' ) by FUNCT_2:def 1;
then [c,c'] in dom (F * f,g) by ZFMISC_1:def 2;
hence (F * f,g) . c,c' = F . (f . c),(g . c') by Th82; :: thesis: verum