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