let C, D be Category; :: thesis: for E being Subcategory of D
for F being Functor of C,E
for G being Functor of C,D st F = G holds
Image F = Image G
let E be Subcategory of D; :: thesis: for F being Functor of C,E
for G being Functor of C,D st F = G holds
Image F = Image G
let F be Functor of C,E; :: thesis: for G being Functor of C,D st F = G holds
Image F = Image G
let G be Functor of C,D; :: thesis: ( F = G implies Image F = Image G )
assume A1: F = G ; :: thesis: Image F = Image G
reconsider S = Image F as strict Subcategory of D by Th4;

A2: now :: thesis: ( dom (Obj F) = the carrier of C & dom (Obj G) = the carrier of C & ( for x being object st x in the carrier of C holds
(Obj G) . x = (Obj F) . x ) )

thus ( dom (Obj F) = the carrier of C & dom (Obj G) = the carrier of C ) by FUNCT_2:def 1; :: thesis: for x being object st x in the carrier of C holds
(Obj G) . x = (Obj F) . x
let x be object ; :: thesis: ( x in the carrier of C implies (Obj G) . x = (Obj F) . x )
assume x in the carrier of C ; :: thesis: (Obj G) . x = (Obj F) . x
then reconsider a = x as Object of C ;
reconsider b = (Obj F) . a as Object of D by CAT_2:6;
G . (id a) = id ((Obj F) . a) by A1, CAT_1:68
.= id b by CAT_2:def 4 ;
hence (Obj G) . x = (Obj F) . x by CAT_1:67; :: thesis: verum

end;

then A3: Obj F = Obj G ;
then A4: the carrier of S = rng (Obj G) by Def3;
A5: rng G c= the carrier' of S by A1, Def3;

now :: thesis: for T being Subcategory of D st the carrier of T = rng (Obj G) & rng G c= the carrier' of T holds
S is Subcategory of T

let T be Subcategory of D; :: thesis: ( the carrier of T = rng (Obj G) & rng G c= the carrier' of T implies S is Subcategory of T )
assume that
A6: the carrier of T = rng (Obj G) and
A7: rng G c= the carrier' of T ; :: thesis: S is Subcategory of T
set x = the Object of C;
A8: (Obj G) . the Object of C in rng (Obj G) by A2, FUNCT_1:def 3;
A9: (Obj G) . the Object of C = (Obj F) . the Object of C by A2;
then (Obj G) . the Object of C in the carrier of T /\ the carrier of E by A6, A8, XBOOLE_0:def 4;
then A10: the carrier of T meets the carrier of E ;
then reconsider E1 = T /\ E as Subcategory of E by Th6;
the carrier of E1 = the carrier of T /\ the carrier of E by A6, A8, A9, Def2;
then A11: the carrier of E1 = rng (Obj F) by A3, A6, XBOOLE_1:28;
the carrier' of E1 = the carrier' of T /\ the carrier' of E by A6, A8, A9, Def2;
then rng F c= the carrier' of E1 by A1, A7, XBOOLE_1:19;
then A12: Image F is Subcategory of E1 by A11, Def3;
E1 is Subcategory of T by A10, Th6;
hence S is Subcategory of T by A12, Th4; :: thesis: verum

end;

hence Image F = Image G by A4, A5, Def3; :: thesis: verum