let I be set ; :: thesis:
let A, B, C be non-empty ManySortedSet of I; :: thesis:
let F be ManySortedFunction of A,B; :: thesis:
let G be ManySortedFunction of B,C; :: thesis:
assume that
A1: ( F is "1-1" & F is "onto" ) and
A2: ( G is "1-1" & G is "onto" ) ; :: thesis:

now :: thesis:

let i be object ; :: thesis:
assume A3: i in I ; :: thesis:
then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def 15;
A4: f is one-to-one by A1, A3, MSUALG_3:1;
reconsider g = G . i as Function of (B . i),(C . i) by A3, PBOOLE:def 15;
A5: g is one-to-one by A2, A3, MSUALG_3:1;
( (F "") . i = f " & rng f = B . i ) by A1, A3, MSUALG_3:def 4;
then reconsider ff = (F "") . i as Function of (B . i),(A . i) by A4, FUNCT_2:25;
A6: ( G ** F is "1-1" & G ** F is "onto" ) by A1, A2, Th14, Th15;
(G ** F) . i = g * f by A3, MSUALG_3:2;
then A7: ((G ** F) "") . i = (g * f) " by A3, A6, MSUALG_3:def 4;
( (G "") . i = g " & rng g = C . i ) by A2, A3, MSUALG_3:def 4;
then reconsider gg = (G "") . i as Function of (C . i),(B . i) by A5, FUNCT_2:25;
((F "") ** (G "")) . i = ff * gg by A3, MSUALG_3:2
.= ff * (g ") by A2, A3, MSUALG_3:def 4
.= (f ") * (g ") by A1, A3, MSUALG_3:def 4 ;
hence ((G ** F) "") . i = ((F "") ** (G "")) . i by A4, A5, A7, FUNCT_1:44; :: thesis:

end;

hence (G ** F) "" = (F "") ** (G "") by PBOOLE:3; :: thesis: