let I be set ; for F being ManySortedFunction of I st doms F is V8() & ( for A, B being ManySortedSet of I st A in doms F & B in doms F & F .. A = F .. B holds
A = B ) holds
F is "1-1"
let F be ManySortedFunction of I; ( doms F is V8() & ( for A, B being ManySortedSet of I st A in doms F & B in doms F & F .. A = F .. B holds
A = B ) implies F is "1-1" )
assume that
A1:
doms F is V8()
and
A2:
for A, B being ManySortedSet of I st A in doms F & B in doms F & F .. A = F .. B holds
A = B
; F is "1-1"
consider K being ManySortedSet of I such that
A3:
K in doms F
by A1, PBOOLE:134;
let i be set ; MSUALG_3:def 2 for b1 being set holds
( not i in dom F or not F . i = b1 or b1 is one-to-one )
let f be Function; ( not i in dom F or not F . i = f or f is one-to-one )
assume that
A4:
i in dom F
and
A5:
F . i = f
; f is one-to-one
let x1, x2 be object ; FUNCT_1:def 4 ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume that
A6:
x1 in dom f
and
A7:
x2 in dom f
and
A8:
f . x1 = f . x2
; x1 = x2
A9:
dom F = I
by PARTFUN1:def 2;
then
dom (K +* (i .--> x1)) = I
by A4, PZFMISC1:1;
then reconsider X1 = K +* (i .--> x1) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;
A10:
dom (i .--> x1) = {i}
;
i in {i}
by TARSKI:def 1;
then A11: X1 . i =
(i .--> x1) . i
by A10, FUNCT_4:13
.=
x1
by FUNCOP_1:72
;
A12:
X1 in doms F
dom (K +* (i .--> x2)) = I
by A4, A9, PZFMISC1:1;
then reconsider X2 = K +* (i .--> x2) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;
A14:
dom (i .--> x2) = {i}
;
i in {i}
by TARSKI:def 1;
then A15: X2 . i =
(i .--> x2) . i
by A14, FUNCT_4:13
.=
x2
by FUNCOP_1:72
;
A16:
X2 in doms F
now for s being object st s in I holds
(F .. X1) . s = (F .. X2) . slet s be
object ;
( s in I implies (F .. X1) . b1 = (F .. X2) . b1 )assume A18:
s in I
;
(F .. X1) . b1 = (F .. X2) . b1per cases
( s = i or s <> i )
;
suppose A19:
s = i
;
(F .. X1) . b1 = (F .. X2) . b1B1:
s in dom F
by A18, PARTFUN1:def 2;
B2:
(
s in dom X2 &
s in dom X1 )
by A18, PARTFUN1:def 2;
then
s in (dom F) /\ (dom X2)
by B1, XBOOLE_0:def 4;
then a20:
s in dom (F .. X2)
by PRALG_1:def 19;
s in (dom F) /\ (dom X1)
by B1, B2, XBOOLE_0:def 4;
then
s in dom (F .. X1)
by PRALG_1:def 19;
hence (F .. X1) . s =
f . (X2 . s)
by A5, A8, A11, A15, A19, PRALG_1:def 19
.=
(F .. X2) . s
by A5, A19, PRALG_1:def 19, a20
;
verum end; end; end;
hence
x1 = x2
by A2, A11, A15, A12, A16, PBOOLE:3; verum