let C be Category; :: thesis: for E being Subcategory of C
for a being Object of E holds (Obj (incl E)) . a = a
let E be Subcategory of C; :: thesis: for a being Object of E holds (Obj (incl E)) . a = a
let a be Object of E; :: thesis: (Obj (incl E)) . a = a
reconsider a' = a as Object of C by Th12;
id a' = id a by Def4
.= (incl E) . (id a) by FUNCT_1:35
.= id ((Obj (incl E)) . a) by CAT_1:104 ;
hence (Obj (incl E)) . a = a by CAT_1:45; :: thesis: verum