let I be set ; 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; 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; 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; ( 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" )
; (G ** F) "" = (F "" ) ** (G "" )
now let i be
set ;
( i in I implies ((G ** F) "" ) . i = ((F "" ) ** (G "" )) . i )assume A3:
i in I
;
((G ** F) "" ) . i = ((F "" ) ** (G "" )) . ithen reconsider f =
F . i as
Function of
(A . i),
(B . i) by PBOOLE:def 18;
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 18;
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 3, MSUALG_3:def 5;
then reconsider ff =
(F "" ) . i as
Function of
(B . i),
(A . i) by A4, FUNCT_2:31;
A6:
(
G ** F is
"1-1" &
G ** F is
"onto" )
by A1, A2, Th16, Th17;
(G ** F) . i = g * f
by A3, MSUALG_3:2;
then A7:
((G ** F) "" ) . i = (g * f) "
by A3, A6, MSUALG_3:def 5;
(
(G "" ) . i = g " &
rng g = C . i )
by A2, A3, MSUALG_3:def 3, MSUALG_3:def 5;
then reconsider gg =
(G "" ) . i as
Function of
(C . i),
(B . i) by A5, FUNCT_2:31;
((F "" ) ** (G "" )) . i =
ff * gg
by A3, MSUALG_3:2
.=
ff * (g " )
by A2, A3, MSUALG_3:def 5
.=
(f " ) * (g " )
by A1, A3, MSUALG_3:def 5
;
hence
((G ** F) "" ) . i = ((F "" ) ** (G "" )) . i
by A4, A5, A7, FUNCT_1:66;
verum end;
hence
(G ** F) "" = (F "" ) ** (G "" )
by PBOOLE:3; verum