let C, D be Category; 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; 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; for G being Functor of C,D st F = G holds
Image F = Image G
let G be Functor of C,D; ( F = G implies Image F = Image G )
assume A1:
F = G
; Image F = Image G
reconsider S = Image F as strict Subcategory of D by Th4;
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 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 Tlet T be
Subcategory of
D;
( 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
;
S is Subcategory of Tset 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;
verum end;
hence
Image F = Image G
by A4, A5, Def3; verum