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