let A, B, C be Category; :: thesis: for F being Functor of [:A,B:],C
for f being Morphism of A
for b being Object of B holds (F ?- f) . b = F . (f,(id b))
let F be Functor of [:A,B:],C; :: thesis: for f being Morphism of A
for b being Object of B holds (F ?- f) . b = F . (f,(id b))
let f be Morphism of A; :: thesis: for b being Object of B holds (F ?- f) . b = F . (f,(id b))
let b be Object of B; :: thesis: (F ?- f) . b = F . (f,(id b))
the carrier' of [:A,B:] = [: the carrier' of A, the carrier' of B:] by CAT_2:23;
then reconsider G = F as Function of [: the carrier' of A, the carrier' of B:], the carrier' of C ;
reconsider Ff = (curry G) . f as Function of the carrier' of B, the carrier' of C ;
F ?- (dom f) is_naturally_transformable_to F ?- (cod f) by Th18;
then F ?- (dom f) is_transformable_to F ?- (cod f) by NATTRA_1:def 7;
hence (F ?- f) . b = ((curry (F,f)) * the Id of B) . b by NATTRA_1:def 5
.= Ff . (id b) by FUNCT_2:15
.= F . (f,(id b)) by CAT_2:3 ;
:: thesis: verum