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;

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) ) )

hence
id E is Functor of E,C
by CAT_1:61; :: thesis: verum( 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) ) )

( 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)

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;( 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

thus
for f being Morphism of E holds
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;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

( 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, g be Morphism of E; :: thesis: ( dom g = cod f implies T . (g (*) f) = (T . g) (*) (T . f) )
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;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

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