let I be set ; :: thesis: for F being ManySortedFunction of I st doms F is non-empty & ( 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 non-empty & ( 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 non-empty 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:146;
let i be set ; :: according to MSUALG_3:def 2 :: thesis: for b₁ being set holds
( not i in dom F or not F . i = b₁ or b₁ 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 set ; :: according to FUNCT_1:def 8 :: 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 & x2 in dom f ) and
A7: f . x1 = f . x2 ; :: thesis: x1 = x2
A8: dom F = I by PBOOLE:def 3;
then dom (K +* (i .--> x1)) = I by A4, PZFMISC1:1;
then reconsider X1 = K +* (i .--> x1) as ManySortedSet of I by PBOOLE:def 3;
A9: dom (i .--> x1) = {i} by FUNCOP_1:19;
i in {i} by TARSKI:def 1;
then A10: X1 . i = (i .--> x1) . i by A9, FUNCT_4:14
.= x1 by FUNCOP_1:87 ;
dom (K +* (i .--> x2)) = I by A4, A8, PZFMISC1:1;
then reconsider X2 = K +* (i .--> x2) as ManySortedSet of I by PBOOLE:def 3;
A11: dom (i .--> x2) = {i} by FUNCOP_1:19;
i in {i} by TARSKI:def 1;
then A12: X2 . i = (i .--> x2) . i by A11, FUNCT_4:14
.= x2 by FUNCOP_1:87 ;
A13: X1 in doms F

proof

let s be set ; :: according to PBOOLE:def 4 :: thesis: ( not s in I or X1 . s in (doms F) . s )
assume A14: 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 A5, A6, A10, A14, MSSUBFAM:14; :: thesis: verum

end;

suppose s <> i ; :: thesis: X1 . s in (doms F) . s

then not s in dom (i .--> x1) by A9, TARSKI:def 1;
then X1 . s = K . s by FUNCT_4:12;
hence X1 . s in (doms F) . s by A3, A14, PBOOLE:def 4; :: thesis: verum

end;

end;

end;

A15: X2 in doms F

proof

let s be set ; :: according to PBOOLE:def 4 :: thesis: ( not s in I or X2 . s in (doms F) . s )
assume A16: 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 A5, A6, A12, A16, MSSUBFAM:14; :: thesis: verum

end;

suppose s <> i ; :: thesis: X2 . s in (doms F) . s

then not s in dom (i .--> x2) by A11, TARSKI:def 1;
then X2 . s = K . s by FUNCT_4:12;
hence X2 . s in (doms F) . s by A3, A16, PBOOLE:def 4; :: thesis: verum

end;

end;

end;

now

let s be set ; :: thesis: ( s in I implies (F .. X1) . b₁ = (F .. X2) . b₁ )
assume A17: s in I ; :: thesis: (F .. X1) . b₁ = (F .. X2) . b₁

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

suppose A18: s = i ; :: thesis: (F .. X1) . b₁ = (F .. X2) . b₁

hence (F .. X1) . s = f . (X2 . s) by A4, A5, A7, A10, A12, PRALG_1:def 17
.= (F .. X2) . s by A4, A5, A18, PRALG_1:def 17 ;
:: thesis: verum

end;

suppose A19: s <> i ; :: thesis: (F .. X1) . b₁ = (F .. X2) . b₁

then A20: not s in dom (i .--> x1) by A9, TARSKI:def 1;
not s in dom (i .--> x2) by A11, A19, TARSKI:def 1;
then A21: X2 . s = K . s by FUNCT_4:12;
reconsider f1 = F . s as Function ;
thus (F .. X1) . s = f1 . (X1 . s) by A8, A17, PRALG_1:def 17
.= f1 . (X2 . s) by A20, A21, FUNCT_4:12
.= (F .. X2) . s by A8, A17, PRALG_1:def 17 ; :: thesis: verum

end;

end;

end;

then F .. X1 = F .. X2 by PBOOLE:3;
hence x1 = x2 by A2, A10, A12, A13, A15; :: thesis: verum