let I be set ; :: thesis: for A, B, C being V2() ManySortedSet of I
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C st F is "1-1" & F is "onto" & G is "1-1" & G is "onto" holds
(G ** F) "" = (F "") ** (G "")

let A, B, C be V2() ManySortedSet of I; :: thesis: for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C st F is "1-1" & F is "onto" & G is "1-1" & G is "onto" holds
(G ** F) "" = (F "") ** (G "")

let F be ManySortedFunction of A,B; :: thesis: for G being ManySortedFunction of B,C st F is "1-1" & F is "onto" & G is "1-1" & G is "onto" holds
(G ** F) "" = (F "") ** (G "")

let G be ManySortedFunction of B,C; :: thesis: ( F is "1-1" & F is "onto" & G is "1-1" & G is "onto" implies (G ** F) "" = (F "") ** (G "") )
assume that
A1: ( F is "1-1" & F is "onto" ) and
A2: ( G is "1-1" & G is "onto" ) ; :: thesis: (G ** F) "" = (F "") ** (G "")
now :: thesis: for i being object st i in I holds
((G ** F) "") . i = ((F "") ** (G "")) . i
let i be object ; :: thesis: ( i in I implies ((G ** F) "") . i = ((F "") ** (G "")) . i )
assume A3: i in I ; :: thesis: ((G ** F) "") . i = ((F "") ** (G "")) . i
then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def 15;
A4: f is one-to-one by ;
reconsider g = G . i as Function of (B . i),(C . i) by ;
A5: g is one-to-one by ;
( (F "") . i = f " & rng f = B . i ) by ;
then reconsider ff = (F "") . i as Function of (B . i),(A . i) by ;
A6: ( G ** F is "1-1" & G ** F is "onto" ) by A1, A2, Th14, Th15;
(G ** F) . i = g * f by ;
then A7: ((G ** F) "") . i = (g * f) " by ;
( (G "") . i = g " & rng g = C . i ) by ;
then reconsider gg = (G "") . i as Function of (C . i),(B . i) by ;
((F "") ** (G "")) . i = ff * gg by
.= ff * (g ") by
.= (f ") * (g ") by ;
hence ((G ** F) "") . i = ((F "") ** (G "")) . i by ; :: thesis: verum
end;
hence (G ** F) "" = (F "") ** (G "") by PBOOLE:3; :: thesis: verum