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

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