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:134;
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 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
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 A5, A6, A11, A13, MSSUBFAM:14; :: 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 A3, A13; :: thesis: verum
end;
end;
end;
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
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 A5, A7, A15, A17, MSSUBFAM:14; :: 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 A3, A17; :: 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
B1: 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 ;
:: 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 A20, TARSKI:def 1;
thus (F .. X1) . s = f1 . (X1 . s) by A18, PRALG_1:def 20
.= f1 . (X2 . s) by A22, A21, FUNCT_4:11
.= (F .. X2) . s by A18, PRALG_1:def 20 ; :: thesis: verum
end;
end;
end;
hence x1 = x2 by A2, A11, A15, A12, A16, PBOOLE:3; :: thesis: verum