let I be set ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ; :: according to MSUALG_3:def 2 :: thesis: for b_{1} being set holds

( not i in dom F or not F . i = b_{1} or b_{1} is one-to-one )

let f be Function; :: thesis: ( 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 ; :: thesis: f is one-to-one

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( 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 ; :: thesis: 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

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

A = B ) holds

F is "1-1"

let F be ManySortedFunction of I; :: thesis: ( 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 ; :: thesis: 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 ; :: according to MSUALG_3:def 2 :: thesis: for b

( not i in dom F or not F . i = b

let f be Function; :: thesis: ( 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 ; :: thesis: f is one-to-one

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( 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 ; :: thesis: 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

proof

dom (K +* (i .--> x2)) = I
by A4, A9, PZFMISC1:1;
let s be object ; :: according to PBOOLE:def 1 :: thesis: ( not s in I or X1 . s in (doms F) . s )

assume A13: s in I ; :: thesis: X1 . s in (doms F) . s

end;assume A13: s in I ; :: thesis: X1 . s in (doms F) . s

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

proof

let s be object ; :: according to PBOOLE:def 1 :: thesis: ( not s in I or X2 . s in (doms F) . s )

assume A17: s in I ; :: thesis: X2 . s in (doms F) . s

end;assume A17: s in I ; :: thesis: X2 . s in (doms F) . s

now :: thesis: for s being object st s in I holds

(F .. X1) . s = (F .. X2) . s

hence
x1 = x2
by A2, A11, A15, A12, A16, PBOOLE:3; :: thesis: verum(F .. X1) . s = (F .. X2) . s

let s be object ; :: thesis: ( s in I implies (F .. X1) . b_{1} = (F .. X2) . b_{1} )

assume A18: s in I ; :: thesis: (F .. X1) . b_{1} = (F .. X2) . b_{1}

end;assume A18: s in I ; :: thesis: (F .. X1) . b

per cases
( s = i or s <> i )
;

end;

suppose A19:
s = i
; :: thesis: (F .. X1) . b_{1} = (F .. X2) . b_{1}

hence (F .. X1) . s =
f . (X2 . s)
by A4, A5, A8, A11, A15, PRALG_1:def 17

.= (F .. X2) . s by A4, A5, A19, PRALG_1:def 17 ;

:: thesis: verum

end;.= (F .. X2) . s by A4, A5, A19, PRALG_1:def 17 ;

:: thesis: verum

suppose A20:
s <> i
; :: thesis: (F .. X1) . b_{1} = (F .. X2) . b_{1}

then
not s in dom (i .--> x2)
by TARSKI:def 1;

then A21: X2 . s = K . s by FUNCT_4:11;

reconsider f1 = F . s as Function ;

A22: not s in dom (i .--> x1) by A20, TARSKI:def 1;

thus (F .. X1) . s = f1 . (X1 . s) by A9, A18, PRALG_1:def 17

.= f1 . (X2 . s) by A22, A21, FUNCT_4:11

.= (F .. X2) . s by A9, A18, PRALG_1:def 17 ; :: thesis: verum

end;then A21: X2 . s = K . s by FUNCT_4:11;

reconsider f1 = F . s as Function ;

A22: not s in dom (i .--> x1) by A20, TARSKI:def 1;

thus (F .. X1) . s = f1 . (X1 . s) by A9, A18, PRALG_1:def 17

.= f1 . (X2 . s) by A22, A21, FUNCT_4:11

.= (F .. X2) . s by A9, A18, PRALG_1:def 17 ; :: thesis: verum