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 "")

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

hence
(G ** F) "" = (F "") ** (G "")
by PBOOLE:3; :: thesis: verum((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 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: verum

end;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 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: verum