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;
then A3:
Obj F = Obj G
by FUNCT_1:9;
then A4:
( the carrier of S = rng (Obj G) & rng G c= the carrier' of S )
by A1, Def3;
now 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 A5:
( the
carrier of
T = rng (Obj G) &
rng G c= the
carrier' of
T )
;
:: thesis: S is Subcategory of Tconsider x being
Object of
C;
A6:
(
(Obj G) . x in rng (Obj G) &
(Obj G) . x = (Obj F) . x )
by A2, FUNCT_1:def 5;
then
(Obj G) . x in the
carrier of
T /\ the
carrier of
E
by A5, XBOOLE_0:def 4;
then A7:
the
carrier of
T meets the
carrier of
E
by XBOOLE_0:def 7;
then reconsider E1 =
T /\ E as
Subcategory of
E by Th6;
(
rng (Obj F) c= the
carrier of
E & the
carrier of
E1 = the
carrier of
T /\ the
carrier of
E )
by A5, A6, Def2;
then A8:
the
carrier of
E1 = rng (Obj F)
by A3, A5, XBOOLE_1:28;
( the
carrier' of
E1 = the
carrier' of
T /\ the
carrier' of
E &
rng F c= the
carrier' of
E )
by A5, A6, Def2;
then
rng F c= the
carrier' of
E1
by A1, A5, XBOOLE_1:19;
then
(
Image F is
Subcategory of
E1 &
E1 is
Subcategory of
T )
by A7, A8, Def3, Th6;
hence
S is
Subcategory of
T
by Th4;
:: thesis: verum end;
hence
Image F = Image G
by A4, Def3; :: thesis: verum