let C, C9, D be Category; :: thesis: for S being Functor of [:C,C9:],D
for c being Object of C
for c9 being Object of C9 holds (Obj (S -? c9)) . c = (Obj S) . c,c9
let S be Functor of [:C,C9:],D; :: thesis: for c being Object of C
for c9 being Object of C9 holds (Obj (S -? c9)) . c = (Obj S) . c,c9
let c be Object of C; :: thesis: for c9 being Object of C9 holds (Obj (S -? c9)) . c = (Obj S) . c,c9
let c9 be Object of C9; :: thesis: (Obj (S -? c9)) . c = (Obj S) . c,c9
(S -? c9) . (id c) = S . (id c),(id c9) by Th4
.= S . (id [c,c9]) by Th41
.= id ((Obj S) . [c,c9]) by CAT_1:104 ;
hence (Obj (S -? c9)) . c = (Obj S) . c,c9 by CAT_1:103; :: thesis: verum