let A, B, C be Category; :: thesis: for F being Functor of [:A,B:],C
for a being Object of A
for b being Object of B holds (F ?- a) . b = F . [a,b]
let F be Functor of [:A,B:],C; :: thesis: for a being Object of A
for b being Object of B holds (F ?- a) . b = F . [a,b]
let a be Object of A; :: thesis: for b being Object of B holds (F ?- a) . b = F . [a,b]
let b be Object of B; :: thesis: (F ?- a) . b = F . [a,b]
thus (F ?- a) . b = (Obj F) . (a,b) by CAT_2:37
.= F . [a,b] ; :: thesis: verum