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 ;
let i be set ; :: according to MSUALG_3:def 2 :: thesis: 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; :: 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 ;
then reconsider X1 = K +* (i .--> x1) as ManySortedSet of I by ;
A10: dom (i .--> x1) = {i} ;
i in {i} by TARSKI:def 1;
then A11: X1 . i = (i .--> x1) . i by
.= x1 by FUNCOP_1:72 ;
A12: X1 in doms F
proof
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
per cases ( s = i or s <> i ) ;
suppose s = i ; :: thesis: X1 . s in (doms F) . s
hence X1 . s in (doms F) . s by ; :: thesis: verum
end;
suppose s <> i ; :: thesis: X1 . s in (doms F) . s
then not s in dom (i .--> x1) by TARSKI:def 1;
then X1 . s = K . s by FUNCT_4:11;
hence X1 . s in (doms F) . s by ; :: thesis: verum
end;
end;
end;
dom (K +* (i .--> x2)) = I by ;
then reconsider X2 = K +* (i .--> x2) as ManySortedSet of I by ;
A14: dom (i .--> x2) = {i} ;
i in {i} by TARSKI:def 1;
then A15: X2 . i = (i .--> x2) . i by
.= 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
per cases ( s = i or s <> i ) ;
suppose s = i ; :: thesis: X2 . s in (doms F) . s
hence X2 . s in (doms F) . s by ; :: thesis: verum
end;
suppose s <> i ; :: thesis: X2 . s in (doms F) . s
then not s in dom (i .--> x2) by TARSKI:def 1;
then X2 . s = K . s by FUNCT_4:11;
hence X2 . s in (doms F) . s by ; :: thesis: verum
end;
end;
end;
now :: thesis: for s being object st s in I holds
(F .. X1) . s = (F .. X2) . s
let s be object ; :: thesis: ( s in I implies (F .. X1) . b1 = (F .. X2) . b1 )
assume A18: s in I ; :: thesis: (F .. X1) . b1 = (F .. X2) . b1
per cases ( s = i or s <> i ) ;
suppose A19: s = i ; :: thesis: (F .. X1) . b1 = (F .. X2) . b1
hence (F .. X1) . s = f . (X2 . s) by
.= (F .. X2) . s by ;
:: thesis: verum
end;
suppose A20: s <> i ; :: thesis: (F .. X1) . b1 = (F .. X2) . b1
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 ;
thus (F .. X1) . s = f1 . (X1 . s) by
.= f1 . (X2 . s) by
.= (F .. X2) . s by ; :: thesis: verum
end;
end;
end;
hence x1 = x2 by ; :: thesis: verum