let I be set ; for A, B being V2() ManySortedSet of I
for H being ManySortedFunction of A,B
for H1 being ManySortedFunction of B,A st H is "1-1" & H is "onto" & H1 = H "" holds
( H ** H1 = id B & H1 ** H = id A )
let A, B be V2() ManySortedSet of I; for H being ManySortedFunction of A,B
for H1 being ManySortedFunction of B,A st H is "1-1" & H is "onto" & H1 = H "" holds
( H ** H1 = id B & H1 ** H = id A )
let H be ManySortedFunction of A,B; for H1 being ManySortedFunction of B,A st H is "1-1" & H is "onto" & H1 = H "" holds
( H ** H1 = id B & H1 ** H = id A )
let H1 be ManySortedFunction of B,A; ( H is "1-1" & H is "onto" & H1 = H "" implies ( H ** H1 = id B & H1 ** H = id A ) )
assume that
A1:
( H is "1-1" & H is "onto" )
and
A2:
H1 = H ""
; ( H ** H1 = id B & H1 ** H = id A )
A3:
now for i being set st i in I holds
(H ** H1) . i = id (B . i)let i be
set ;
( i in I implies (H ** H1) . i = id (B . i) )assume A4:
i in I
;
(H ** H1) . i = id (B . i)then reconsider h =
H . i as
Function of
(A . i),
(B . i) by PBOOLE:def 15;
reconsider h1 =
H1 . i as
Function of
(B . i),
(A . i) by A4, PBOOLE:def 15;
i in dom H
by A4, PARTFUN1:def 2;
then A5:
h is
one-to-one
by A1;
h1 = h "
by A1, A2, A4, Def4;
then
h * h1 = id (rng h)
by A5, FUNCT_1:39;
then
h * h1 = id (B . i)
by A1, A4;
hence
(H ** H1) . i = id (B . i)
by A4, Th2;
verum end;
for i being set st i in I holds
(H1 ** H) . i = id (A . i)
proof
let i be
set ;
( i in I implies (H1 ** H) . i = id (A . i) )
assume A6:
i in I
;
(H1 ** H) . i = id (A . i)
then reconsider h =
H . i as
Function of
(A . i),
(B . i) by PBOOLE:def 15;
reconsider h1 =
H1 . i as
Function of
(B . i),
(A . i) by A6, PBOOLE:def 15;
i in dom H
by A6, PARTFUN1:def 2;
then A7:
h is
one-to-one
by A1;
(
h1 = h " &
dom h = A . i )
by A1, A2, A6, Def4, FUNCT_2:def 1;
then
h1 * h = id (A . i)
by A7, FUNCT_1:39;
hence
(H1 ** H) . i = id (A . i)
by A6, Th2;
verum
end;
hence
( H ** H1 = id B & H1 ** H = id A )
by A3, Def1; verum