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 a9 = a as Object of C by Th2;
id a9 = id a by Def4
.= (incl E) . (id a) by FUNCT_1:18
.= id ((Obj (incl E)) . a) by CAT_1:68 ;
hence (Obj (incl E)) . a = a by CAT_1:59; :: thesis: verum