let A, B, C be Category; 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; 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; for b being Object of B holds (F ?- a) . b = F . [a,b]
let b be Object of B; (F ?- a) . b = F . [a,b]
thus (F ?- a) . b =
(Obj F) . (a,b)
by CAT_2:37
.=
F . [a,b]
; verum