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
proof
let a be Element of B; :: according to INDEX_1:def 7 :: thesis: (B --> (id C)) . a is Functor of ((A --> C) * F) . a,((A --> C) * G) . a
( (A --> C) . (F . a) = C & dom ((A --> C) * F) = B ) by PARTFUN1:def 2;
then A4: ( (B --> (id C)) . a = id C & ((A --> C) * F) . a = C ) by FUNCT_1:12;
( (A --> C) . (G . a) = C & dom ((A --> C) * G) = B ) by PARTFUN1:def 2;
hence (B --> (id C)) . a is Functor of ((A --> C) * F) . a,((A --> C) * G) . a by A4, FUNCT_1:12; :: thesis: verum
end;
then reconsider I = [(A --> C),(B --> (id C))] as Indexing of F,G by A2, A3, Def8;
take I ; :: thesis: ( ( 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) ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: (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; :: thesis: verum