let C be Category; :: thesis: for E being Subcategory of C holds id E is Functor of E,C
let E be Subcategory of C; :: thesis: id E is Functor of E,C
rng (id E) c= the carrier' of C by Th3;
then reconsider T = id E as Function of the carrier' of E, the carrier' of C by FUNCT_2:6;

now :: thesis: ( ( for e being Object of E ex c being Object of C st T . (id e) = id c ) & ( for f being Morphism of E holds
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) ) & ( for f, g being Morphism of E st dom g = cod f holds
T . (g (*) f) = (T . g) (*) (T . f) ) )

thus for e being Object of E ex c being Object of C st T . (id e) = id c :: thesis: ( ( for f being Morphism of E holds
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) ) & ( for f, g being Morphism of E st dom g = cod f holds
T . (g (*) f) = (T . g) (*) (T . f) ) )

proof

let e be Object of E; :: thesis: ex c being Object of C st T . (id e) = id c
reconsider c = e as Object of C by Th2;
T . (id e) = id e by FUNCT_1:18
.= id c by Def4 ;
hence ex c being Object of C st T . (id e) = id c ; :: thesis: verum

end;

thus for f being Morphism of E holds
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) :: thesis: for f, g being Morphism of E st dom g = cod f holds
T . (g (*) f) = (T . g) (*) (T . f)

proof

let f be Morphism of E; :: thesis: ( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) )
A1: T . (id (dom f)) = id (dom f) by FUNCT_1:18
.= id (dom ((id E) . f)) by FUNCT_1:18 ;
A2: T . (id (cod f)) = id (cod f) by FUNCT_1:18
.= id (cod ((id E) . f)) by FUNCT_1:18 ;
( dom (T . f) = dom ((id E) . f) & cod (T . f) = cod ((id E) . f) ) by Th5;
hence ( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) by A1, A2, Def4; :: thesis: verum

end;

let f, g be Morphism of E; :: thesis: ( dom g = cod f implies T . (g (*) f) = (T . g) (*) (T . f) )
A3: ( T . f = f & T . g = g ) by FUNCT_1:18;
assume A4: dom g = cod f ; :: thesis: T . (g (*) f) = (T . g) (*) (T . f)
then T . (g (*) f) = ((id E) . g) (*) ((id E) . f) by CAT_1:64;
hence T . (g (*) f) = (T . g) (*) (T . f) by A4, A3, Th7; :: thesis: verum

end;

hence id E is Functor of E,C by CAT_1:61; :: thesis: verum