let A, B, C be Category; :: thesis: for F being Functor of [:A,B:],C holds id (export F) = export (id F)
let F be Functor of [:A,B:],C; :: thesis: id (export F) = export (id F)
reconsider s = id F as Function of [: the carrier of A, the carrier of B:], the carrier' of C ;

now :: thesis: for a being Object of A holds (id (export F)) . a = (export (id F)) . a

let a be Object of A; :: thesis: (id (export F)) . a = (export (id F)) . a
reconsider ff = (export F) . a as Functor of B,C by Th5;

A1: now :: thesis: for b being Object of B holds (id ff) . b = ((curry s) . a) . b

let b be Object of B; :: thesis: (id ff) . b = ((curry s) . a) . b
thus (id ff) . b = (id ff) . b by NATTRA_1:def 5
.= id (ff . b) by NATTRA_1:20
.= ff . (id b) by CAT_1:71
.= (F ?- a) . (id b) by Th18
.= F . ((id a),(id b)) by CAT_2:36
.= F . (id [a,b]) by CAT_2:31
.= id (F . [a,b]) by CAT_1:71
.= (id F) . [a,b] by NATTRA_1:20
.= (id F) . (a,b) by NATTRA_1:def 5
.= ((curry s) . a) . b by FUNCT_5:69 ; :: thesis: verum

end;

thus (id (export F)) . a = id ((export F) . a) by NATTRA_1:20
.= [[ff,ff],(id ff)] by NATTRA_1:def 17
.= [[((export F) . a),((export F) . a)],((curry s) . a)] by A1, FUNCT_2:63
.= (export (id F)) . a by Def5 ; :: thesis: verum

end;

hence id (export F) = export (id F) by NATTRA_1:19; :: thesis: verum