let D, D', E, C, C' be non empty set ; :: 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 is Function of [:C,C':],E
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 is Function of [:C,C':],E
let f be Function of C,D; :: thesis: for g being Function of C',D' holds F * f,g is Function of [:C,C':],E
let g be Function of C',D'; :: thesis: F * f,g is Function of [:C,C':],E
F * f,g = F * [:f,g:] ;
hence F * f,g is Function of [:C,C':],E ; :: thesis: verum