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