let C, C9, D, D9, E 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