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)
the carrier' of [:A,B:] = [: the carrier' of A, the carrier' of B:] by CAT_2:23;
then 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 ;
dom (id a) = a by CAT_1:19;
then reconsider I = F ?- (id a) as transformation of F ?- a,F ?- a by CAT_1:19;

now

let b be Object of B; :: thesis: I . b = id ((F ?- a) . b)
thus I . b = Ff . (id b) by FUNCT_2:15
.= F . ((id a),(id b)) by CAT_2:3
.= F . (id [a,b]) by CAT_2:31
.= id (F . [a,b]) by CAT_1:71
.= id ((F ?- a) . b) by Th12 ; :: thesis: verum

end;

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