for C, D, C9 being Category
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)