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)
the carrier of [:A,B:] = [:the carrier of A,the carrier of B:] by CAT_2:33;
then reconsider s = id F as Function of [:the carrier of A,the carrier of B:],the carrier' of C ;

now

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 Th8;

A1: now

let b be Object of B; :: thesis: (id ff) . b = ((curry s) . a) . b
A2: Hom b,b <> {} by CAT_1:56;
thus (id ff) . b = (id ff) . b by NATTRA_1:def 5
.= id (ff . b) by NATTRA_1:21
.= ff . (id b) by CAT_1:108
.= ff . (id b) by A2, NATTRA_1:def 1
.= (F ?- a) . (id b) by Th24
.= (F ?- a) . (id b) by A2, NATTRA_1:def 1
.= F . (id a),(id b) by CAT_2:47
.= F . (id [a,b]) by CAT_2:41
.= id (F . [a,b]) by CAT_1:108
.= (id F) . [a,b] by NATTRA_1:21
.= (id F) . a,b by NATTRA_1:def 5
.= ((curry s) . a) . b by CAT_2:3 ; :: thesis: verum

end;

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

end;

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