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:33;
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:21
.= F . f,(id b) by CAT_2:3 ;
:: thesis: verum