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 ?- c)) . c9 = (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 ?- c)) . c9 = (Obj S) . c,c9
let c be Object of C; :: thesis: for c9 being Object of C9 holds (Obj (S ?- c)) . c9 = (Obj S) . c,c9
let c9 be Object of C9; :: thesis: (Obj (S ?- c)) . c9 = (Obj S) . c,c9
(S ?- c) . (id c9) = S . (id c),(id c9) by Th3
.= S . (id [c,c9]) by Th41
.= id ((Obj S) . [c,c9]) by CAT_1:104 ;
hence (Obj (S ?- c)) . c9 = (Obj S) . c,c9 by CAT_1:103; :: thesis: verum