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))
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 ;
A1: id b = (IdMap B) . b by ISOCAT_1:def 12;
F ?- (dom f) is_naturally_transformable_to F ?- (cod f) by Th14;
then F ?- (dom f) is_transformable_to F ?- (cod f) ;
hence (F ?- f) . b = ((curry (F,f)) * (IdMap B)) . b by NATTRA_1:def 5
.= Ff . (id b) by A1, FUNCT_2:15
.= F . (f,(id b)) by FUNCT_5:69 ;
:: thesis: verum