dom (G ** F) = I by Th2;
then reconsider fg = G ** F as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;
reconsider fg = fg as ManySortedFunction of I ;
for i being object st i in I holds
fg . i is Function of (A . i),(C . i)

proof

let i be object ; :: thesis: ( i in I implies fg . i is Function of (A . i),(C . i) )
assume A1: i in I ; :: thesis: fg . i is Function of (A . i),(C . i)
then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def 15;
reconsider g = G . i as Function of (B . i),(C . i) by A1, PBOOLE:def 15;
(G ** F) . i = g * f by A1, Th2;
hence fg . i is Function of (A . i),(C . i) by A1; :: thesis: verum

end;

hence G ** F is ManySortedFunction of A,C by PBOOLE:def 15; :: thesis: verum