let C, B be Category; :: thesis: for c being Object of
for b being Object of holds (Obj (B --> c)) . b = c
let c be Object of ; :: thesis: for b being Object of holds (Obj (B --> c)) . b = c
let b be Object of ; :: thesis: (Obj (B --> c)) . b = c
(B --> c) . (id b) = id c by FUNCOP_1:13;
hence (Obj (B --> c)) . b = c by CAT_1:103; :: thesis: verum