set I2 = B --> (id C);
set I1 = A --> C;
A2: [(A --> C),(B --> (id C))] `1 = A --> C by MCART_1:7;
A3: [(A --> C),(B --> (id C))] `2 = B --> (id C) by MCART_1:7;
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 FUNCOP_1:13, PARTFUN1:def 4;
then A4: ( (B --> (id C)) . a = id C & ((A --> C) * F) . a = C ) by FUNCOP_1:13, FUNCT_1:22;
( (A --> C) . (G . a) = C & dom ((A --> C) * G) = B ) by FUNCOP_1:13, PARTFUN1:def 4;
hence (B --> (id C)) . a is Functor of ((A --> C) * F) . a,((A --> C) * G) . a by A4, FUNCT_1:22; :: 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) ) )

hereby :: 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 a be Element of A; :: thesis: (I `2) . (i . a) = id ((I `1) . a)
thus (I `2) . (i . a) = id C by A3, FUNCOP_1:13
.= id ((I `1) . a) by A2, FUNCOP_1:13 ; :: thesis: verum

end;

let m1, m2 be Element of B; :: thesis: ( F . m2 = G . m1 implies (I `2) . (c . [m2,m1]) = ((I `2) . m2) * ((I `2) . m1) )
assume F . m2 = G . m1 ; :: thesis: (I `2) . (c . [m2,m1]) = ((I `2) . m2) * ((I `2) . m1)
then [m2,m1] in dom c by A1, CAT_1:def 8;
then A5: (I `2) . (c . [m2,m1]) = id C by A3, FUNCOP_1:13, PARTFUN1:27;
( (I `2) . m1 = id C & (I `2) . m2 = id C ) by A3, FUNCOP_1:13;
hence (I `2) . (c . [m2,m1]) = ((I `2) . m2) * ((I `2) . m1) by A5, FUNCT_2:23; :: thesis: verum