let S be non empty non void ManySortedSign ; for X being non-empty ManySortedSet of the carrier of S holds Reverse X is "1-1"
let X be non-empty ManySortedSet of the carrier of S; Reverse X is "1-1"
for i being set st i in the carrier of S holds
(Reverse X) . i is one-to-one
proof
set D =
DTConMSA X;
let i be
set ;
( i in the carrier of S implies (Reverse X) . i is one-to-one )
assume
i in the
carrier of
S
;
(Reverse X) . i is one-to-one
then reconsider s =
i as
SortSymbol of
S ;
set f =
(Reverse X) . s;
let x1,
x2 be
object ;
FUNCT_1:def 4 ( not x1 in dom ((Reverse X) . i) or not x2 in dom ((Reverse X) . i) or not ((Reverse X) . i) . x1 = ((Reverse X) . i) . x2 or x1 = x2 )
assume that A1:
x1 in dom ((Reverse X) . i)
and A2:
x2 in dom ((Reverse X) . i)
and A3:
((Reverse X) . i) . x1 = ((Reverse X) . i) . x2
;
x1 = x2
A4:
(Reverse X) . s = Reverse (
s,
X)
by MSAFREE:def 18;
then A5:
dom ((Reverse X) . s) = FreeGen (
s,
X)
by FUNCT_2:def 1;
then consider a2 being
set such that A6:
a2 in X . s
and A7:
x2 = root-tree [a2,s]
by A2, MSAFREE:def 15;
A8:
[a2,s] in Terminals (DTConMSA X)
by A6, MSAFREE:7;
then reconsider t2 =
[a2,s] as
Symbol of
(DTConMSA X) ;
t2 `2 = s
;
then
root-tree t2 in { (root-tree tt) where tt is Symbol of (DTConMSA X) : ( tt in Terminals (DTConMSA X) & tt `2 = s ) }
by A8;
then
root-tree t2 in FreeGen (
s,
X)
by MSAFREE:13;
then A9:
((Reverse X) . s) . x2 =
[a2,s] `1
by A4, A7, MSAFREE:def 17
.=
a2
;
consider a1 being
set such that A10:
a1 in X . s
and A11:
x1 = root-tree [a1,s]
by A1, A5, MSAFREE:def 15;
A12:
[a1,s] in Terminals (DTConMSA X)
by A10, MSAFREE:7;
then reconsider t1 =
[a1,s] as
Symbol of
(DTConMSA X) ;
t1 `2 = s
;
then
root-tree t1 in { (root-tree tt) where tt is Symbol of (DTConMSA X) : ( tt in Terminals (DTConMSA X) & tt `2 = s ) }
by A12;
then
root-tree t1 in FreeGen (
s,
X)
by MSAFREE:13;
then ((Reverse X) . s) . x1 =
[a1,s] `1
by A4, A11, MSAFREE:def 17
.=
a1
;
hence
x1 = x2
by A3, A11, A7, A9;
verum
end;
hence
Reverse X is "1-1"
by MSUALG_3:1; verum