let A, B, C be Category; :: thesis: for F being Functor of [:A,B:],C
for a being Object of A holds id (F ?- a) = F ?- (id a)
let F be Functor of [:A,B:],C; :: thesis: for a being Object of A holds id (F ?- a) = F ?- (id a)
let a be Object of A; :: thesis: id (F ?- a) = F ?- (id a)
reconsider G = F as Function of [: the carrier' of A, the carrier' of B:], the carrier' of C ;
reconsider Ff = (curry G) . (id a) as Function of the carrier' of B, the carrier' of C ;
reconsider I = F ?- (id a) as transformation of F ?- a,F ?- a ;

now :: thesis: for b being Object of B holds I . b = id ((F ?- a) . b)

let b be Object of B; :: thesis: I . b = id ((F ?- a) . b)
A1: id b = (IdMap B) . b by ISOCAT_1:def 12;
thus I . b = Ff . (id b) by A1, FUNCT_2:15
.= F . ((id a),(id b)) by FUNCT_5:69
.= F . (id [a,b]) by CAT_2:31
.= id (F . [a,b]) by CAT_1:71
.= id ((F ?- a) . b) by Th8 ; :: thesis: verum

end;

hence id (F ?- a) = F ?- (id a) by NATTRA_1:def 4; :: thesis: verum