let C, C', D be Category; :: thesis: for S being Functor of [:C,C':],D
for c being Object of C
for c' being Object of C' holds (Obj (S ?- c)) . c' = (Obj S) . c,c'
let S be Functor of [:C,C':],D; :: thesis: for c being Object of C
for c' being Object of C' holds (Obj (S ?- c)) . c' = (Obj S) . c,c'
let c be Object of C; :: thesis: for c' being Object of C' holds (Obj (S ?- c)) . c' = (Obj S) . c,c'
let c' be Object of C'; :: thesis: (Obj (S ?- c)) . c' = (Obj S) . c,c'
(S ?- c) . (id c') = S . (id c),(id c') by Th3
.= 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