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 is Functor of B,C
let F be Functor of [:A,B:],C; :: thesis: for a being Object of A holds (export F) . a is Functor of B,C
let a be Object of A; :: thesis: (export F) . a is Functor of B,C
(export F) . a = F ?- a by Th18;
hence (export F) . a is Functor of B,C ; :: thesis: verum