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

end;

then reconsider I = [(A --> C),(B --> (id C))] as Indexing of F,G by A2, 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 A2, 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 ( (I `2 ) . (c . [m2,m1]) = id C & (I `2 ) . m1 = id C & (I `2 ) . m2 = id C ) by A2, FUNCOP_1:13, PARTFUN1:27;
hence (I `2 ) . (c . [m2,m1]) = ((I `2 ) . m2) * ((I `2 ) . m1) by FUNCT_2:23; :: thesis: verum