let A, B, C be Category; :: thesis: for F being Functor of [:A,B:],C
for a being Object of A holds (export F) . a = F ?- a
let F be Functor of [:A,B:],C; :: thesis: for a being Object of A holds (export F) . a = F ?- a
let a be Object of A; :: thesis: (export F) . a = F ?- a
reconsider o = F ?- a as Object of (Functors (B,C)) by Th5;
reconsider i = id a as Morphism of A ;
(export F) . i = [[(F ?- a),(F ?- a)],(F ?- (id a))] by Def4
.= [[(F ?- a),(F ?- a)],(id (F ?- a))] by Th16
.= id o by NATTRA_1:def 17 ;
hence (export F) . a = F ?- a by CAT_1:67; :: thesis: verum