let C, D be Category; :: thesis: for E being Subcategory of D
for F being Functor of C,D st rng F c= the carrier' of E holds
F is Functor of C,E
let E be Subcategory of D; :: thesis: for F being Functor of C,D st rng F c= the carrier' of E holds
F is Functor of C,E
let F be Functor of C,D; :: thesis: ( rng F c= the carrier' of E implies F is Functor of C,E )
assume A1: rng F c= the carrier' of E ; :: thesis: F is Functor of C,E
A2: ( dom F = the carrier' of C & dom (Obj F) = the carrier of C ) by FUNCT_2:def 1;
then reconsider G = F as Function of the carrier' of C,the carrier' of E by A1, FUNCT_2:def 1, RELSET_1:11;
A3: rng (Obj F) c= the carrier of E

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (Obj F) or y in the carrier of E )
assume y in rng (Obj F) ; :: thesis: y in the carrier of E
then consider x being set such that
A4: ( x in dom (Obj F) & y = (Obj F) . x ) by FUNCT_1:def 5;
reconsider x = x as Object of C by A4;
F . (id x) = id ((Obj F) . x) by CAT_1:104;
then id ((Obj F) . x) in rng F by A2, FUNCT_1:def 5;
then reconsider f = id ((Obj F) . x) as Morphism of E by A1;
( dom (id ((Obj F) . x)) = y & dom (id ((Obj F) . x)) = dom f ) by A4, CAT_1:44, CAT_2:15;
hence y in the carrier of E ; :: thesis: verum

end;

A5: now

let c be Object of C; :: thesis: ex d being Object of E st G . (id c) = id d
(Obj F) . c in rng (Obj F) by A2, FUNCT_1:def 5;
then reconsider d = (Obj F) . c as Object of E by A3;
take d = d; :: thesis: G . (id c) = id d
thus G . (id c) = id ((Obj F) . c) by CAT_1:104
.= id d by CAT_2:def 4 ; :: thesis: verum

end;

A6: now

let f be Morphism of C; :: thesis: ( G . (id (dom f)) = id (dom (G . f)) & G . (id (cod f)) = id (cod (G . f)) )
A7: ( dom (F . f) = dom (G . f) & cod (F . f) = cod (G . f) ) by CAT_2:15;
thus G . (id (dom f)) = id (F . (dom f)) by CAT_1:108
.= id (dom (F . f)) by CAT_1:109
.= id (dom (G . f)) by A7, CAT_2:def 4 ; :: thesis: G . (id (cod f)) = id (cod (G . f))
thus G . (id (cod f)) = id (F . (cod f)) by CAT_1:108
.= id (cod (F . f)) by CAT_1:109
.= id (cod (G . f)) by A7, CAT_2:def 4 ; :: thesis: verum

end;

now

let f, g be Morphism of C; :: thesis: ( dom g = cod f implies G . (g * f) = (G . g) * (G . f) )
assume dom g = cod f ; :: thesis: G . (g * f) = (G . g) * (G . f)
then ( F . (g * f) = (F . g) * (F . f) & dom (F . g) = cod (F . f) & dom (F . g) = dom (G . g) & cod (F . f) = cod (G . f) ) by CAT_1:99, CAT_2:15;
hence G . (g * f) = (G . g) * (G . f) by CAT_2:17; :: thesis: verum

end;

hence F is Functor of C,E by A5, A6, CAT_1:96; :: thesis: verum