let C be Category; for D being Categorial Category
for F being Functor of C,D holds [(Obj F),(pr2 F)] is Indexing of C
let D be Categorial Category; for F being Functor of C,D holds [(Obj F),(pr2 F)] is Indexing of C
let F be Functor of C,D; [(Obj F),(pr2 F)] is Indexing of C
set I = [(Obj F),(pr2 F)];
A1:
dom F = the carrier' of C
by FUNCT_2:def 1;
dom (Obj F) = the carrier of C
by FUNCT_2:def 1;
then A2:
Obj F is ManySortedSet of the carrier of C
by PARTFUN1:def 2;
A3:
[(Obj F),(pr2 F)] `2 = pr2 F
;
A4:
dom (pr2 F) = dom F
by MCART_1:def 13;
then
pr2 F is ManySortedSet of the carrier' of C
by A1, PARTFUN1:def 2, RELAT_1:def 18;
then reconsider I = [(Obj F),(pr2 F)] as ManySortedSet of the carrier of C, the carrier' of C by A2, Def4;
pr2 F is Function-yielding
then reconsider FF = pr2 F as ManySortedFunction of the carrier' of C by A4, A1, PARTFUN1:def 2, RELAT_1:def 18;
I `1 is Category-yielding
;
then reconsider I = I as Category-yielding_on_first ManySortedSet of the carrier of C, the carrier' of C by Def5;
FF is ManySortedFunctor of (I `1) * the Source of C,(I `1) * the Target of C
proof
let m be
Morphism of
C;
INDEX_1:def 7 FF . m is Functor of ((I `1) * the Source of C) . m,((I `1) * the Target of C) . m
reconsider x =
F . m as
Morphism of
D ;
A5:
x `11 = dom (F . m)
by CAT_5:13;
x `12 = cod (F . m)
by CAT_5:13;
then consider f being
Functor of
x `11 ,
x `12 such that A6:
F . m = [[(x `11),(x `12)],f]
by A5, CAT_5:def 6;
A7:
((Obj F) * the Source of C) . m =
(Obj F) . (dom m)
by FUNCT_2:15
.=
dom (F . m)
by CAT_1:69
;
A8:
((Obj F) * the Target of C) . m =
(Obj F) . (cod m)
by FUNCT_2:15
.=
cod (F . m)
by CAT_1:69
;
FF . m =
x `2
by A1, MCART_1:def 13
.=
f
by A6
;
hence
FF . m is
Functor of
((I `1) * the Source of C) . m,
((I `1) * the Target of C) . m
by A5, A7, A8, CAT_5:13;
verum
end;
then reconsider I = I as Indexing of the Source of C, the Target of C by A3, Def8;
A9:
dom F = the carrier' of C
by FUNCT_2:def 1;
A10:
now for m1, m2 being Morphism of C st dom m2 = cod m1 holds
(I `2) . (m2 (*) m1) = ((I `2) . m2) * ((I `2) . m1)let m1,
m2 be
Morphism of
C;
( dom m2 = cod m1 implies (I `2) . (m2 (*) m1) = ((I `2) . m2) * ((I `2) . m1) )assume A11:
dom m2 = cod m1
;
(I `2) . (m2 (*) m1) = ((I `2) . m2) * ((I `2) . m1)set h1 =
F . m1;
set h2 =
F . m2;
A12:
dom (F . m2) =
F . (dom m2)
by CAT_1:72
.=
cod (F . m1)
by A11, CAT_1:72
;
A13:
dom (F . m2) = (F . m2) `11
by CAT_5:13;
cod (F . m2) = (F . m2) `12
by CAT_5:13;
then consider f2 being
Functor of
(F . m2) `11 ,
(F . m2) `12 such that A14:
F . m2 = [[((F . m2) `11),((F . m2) `12)],f2]
by A13, CAT_5:def 6;
A15:
cod (F . m1) = (F . m1) `12
by CAT_5:13;
dom (F . m1) = (F . m1) `11
by CAT_5:13;
then consider f1 being
Functor of
(F . m1) `11 ,
(F . m1) `12 such that A16:
F . m1 = [[((F . m1) `11),((F . m1) `12)],f1]
by A15, CAT_5:def 6;
thus (I `2) . (m2 (*) m1) =
(F . (m2 (*) m1)) `2
by A9, MCART_1:def 13
.=
((F . m2) (*) (F . m1)) `2
by A11, CAT_1:64
.=
[[((F . m1) `11),((F . m2) `12)],(f2 * f1)] `2
by A13, A15, A14, A16, A12, CAT_5:def 6
.=
f2 * f1
.=
((F . m2) `2) * f1
by A14
.=
((F . m2) `2) * ((F . m1) `2)
by A16
.=
((I `2) . m2) * ((F . m1) `2)
by A9, MCART_1:def 13
.=
((I `2) . m2) * ((I `2) . m1)
by A9, MCART_1:def 13
;
verum end;
hence
[(Obj F),(pr2 F)] is Indexing of C
by A10, Th6; verum