let C be Category; :: thesis: for D1, D2 being Categorial Category
for F1 being Functor of C,D1
for F2 being Functor of C,D2 st F1 = F2 holds
Image F1 = Image F2
let D1, D2 be Categorial Category; :: thesis: for F1 being Functor of C,D1
for F2 being Functor of C,D2 st F1 = F2 holds
Image F1 = Image F2
let F1 be Functor of C,D1; :: thesis: for F2 being Functor of C,D2 st F1 = F2 holds
Image F1 = Image F2
let F2 be Functor of C,D2; :: thesis: ( F1 = F2 implies Image F1 = Image F2 )
assume A1: F1 = F2 ; :: thesis: Image F1 = Image F2
reconsider DD = the carrier of D1 \/ the carrier of D2 as non empty set ;
DD is categorial
proof
let d be Element of DD; :: according to CAT_5:def 5 :: thesis: d is Category
( d is Object of D1 or d is Object of D2 ) by XBOOLE_0:def 3;
hence d is Category by Th12; :: thesis: verum
end;
then reconsider DD = the carrier of D1 \/ the carrier of D2 as non empty categorial set ;
consider D being strict Categorial full Category such that
A2: the carrier of D = DD by Th20;
reconsider D1 = D1, D2 = D2 as Subcategory of D by A2, Th21, XBOOLE_1:7;
reconsider F1 = F1 as Functor of C,D1 ;
reconsider F2 = F2 as Functor of C,D2 ;
rng F1 c= the carrier' of D1 ;
then F1 = (incl D1) * F1 by RELAT_1:53;
then reconsider G1 = F1 as Functor of C,D ;
Image F1 = Image G1 by Th9
.= Image F2 by A1, Th9 ;
hence Image F1 = Image F2 ; :: thesis: verum