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)

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

hence
G ** F is ManySortedFunction of A,C
by PBOOLE:def 15; :: thesis: verum
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;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