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:23;
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:27;
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
.= 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: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 CAT_2:3 ; :: 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