let I be set ; :: thesis: for A, B being ManySortedSet of st A is_transformable_to B holds
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 ManySortedSet of ; :: thesis: ( A is_transformable_to B implies 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 ) )
assume A1:
A is_transformable_to B
; :: thesis: 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; :: thesis: 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; :: thesis: ( H is "1-1" & H is "onto" & H1 = H "" implies ( H ** H1 = id B & H1 ** H = id A ) )
assume A2:
( H is "1-1" & H is "onto" & H1 = H "" )
; :: thesis: ( H ** H1 = id B & H1 ** H = id A )
A3:
for i being set st i in I holds
(H1 ** H) . i = id (A . i)
proof
let i be
set ;
:: thesis: ( i in I implies (H1 ** H) . i = id (A . i) )
assume A4:
i in I
;
:: thesis: (H1 ** H) . i = id (A . i)
then A5:
i in dom H
by PARTFUN1:def 4;
reconsider h =
H . i as
Function of
(A . i),
(B . i) by A4, PBOOLE:def 18;
reconsider h1 =
H1 . i as
Function of
(B . i),
(A . i) by A4, PBOOLE:def 18;
A6:
h1 = h "
by A2, A4, MSUALG_3:def 5;
A7:
h is
one-to-one
by A2, A5, MSUALG_3:def 2;
(
B . i = {} implies
A . i = {} )
by A1, A4, PZFMISC1:def 3;
then
(
dom h = A . i &
rng h c= B . i )
by FUNCT_2:def 1, RELAT_1:def 19;
then
h1 * h = id (A . i)
by A6, A7, FUNCT_1:61;
hence
(H1 ** H) . i = id (A . i)
by A4, MSUALG_3:2;
:: thesis: verum
end;
reconsider F = H1 ** H as ManySortedFunction of ;
then reconsider F = F as ManySortedFunction of A,A by PBOOLE:def 18;
A8:
F = id A
by A3, MSUALG_3:def 1;
A9:
now let i be
set ;
:: thesis: ( i in I implies (H ** H1) . i = id (B . i) )assume A10:
i in I
;
:: thesis: (H ** H1) . i = id (B . i)then A11:
i in dom H
by PARTFUN1:def 4;
reconsider h =
H . i as
Function of
(A . i),
(B . i) by A10, PBOOLE:def 18;
reconsider h1 =
H1 . i as
Function of
(B . i),
(A . i) by A10, PBOOLE:def 18;
A12:
h1 = h "
by A2, A10, MSUALG_3:def 5;
h is
one-to-one
by A2, A11, MSUALG_3:def 2;
then
h * h1 = id (rng h)
by A12, FUNCT_1:61;
then
h * h1 = id (B . i)
by A2, A10, MSUALG_3:def 3;
hence
(H ** H1) . i = id (B . i)
by A10, MSUALG_3:2;
:: thesis: verum end;
reconsider F1 = H ** H1 as ManySortedFunction of ;
then
F1 is ManySortedFunction of B,B
by PBOOLE:def 18;
hence
( H ** H1 = id B & H1 ** H = id A )
by A8, A9, MSUALG_3:def 1; :: thesis: verum