set I2 = B --> (id C);
set I1 = A --> C;
A2:
[(A --> C),(B --> (id C))] `1 = A --> C
;
A3:
[(A --> C),(B --> (id C))] `2 = B --> (id C)
;
B --> (id C) is ManySortedFunctor of (A --> C) * F,(A --> C) * G
then reconsider I = [(A --> C),(B --> (id C))] as Indexing of F,G by A2, A3, Def8;
take
I
; ( ( for a being Element of A holds (I `2) . (i . a) = id ((I `1) . a) ) & ( for m1, m2 being Element of B st F . m2 = G . m1 holds
(I `2) . (c . [m2,m1]) = ((I `2) . m2) * ((I `2) . m1) ) )
thus
for a being Element of A holds (I `2) . (i . a) = id ((I `1) . a)
; for m1, m2 being Element of B st F . m2 = G . m1 holds
(I `2) . (c . [m2,m1]) = ((I `2) . m2) * ((I `2) . m1)
let m1, m2 be Element of B; ( F . m2 = G . m1 implies (I `2) . (c . [m2,m1]) = ((I `2) . m2) * ((I `2) . m1) )
reconsider mm1 = m1, mm2 = m2 as Morphism of C by A1;
assume
F . m2 = G . m1
; (I `2) . (c . [m2,m1]) = ((I `2) . m2) * ((I `2) . m1)
then
cod mm1 = dom mm2
by A1;
then
[m2,m1] in dom c
by A1, CAT_1:def 6;
then A5:
(I `2) . (c . [m2,m1]) = id C
by FUNCOP_1:7, PARTFUN1:4;
thus
(I `2) . (c . [m2,m1]) = ((I `2) . m2) * ((I `2) . m1)
by A5, FUNCT_2:17; verum