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