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