:: Partial Functions from a Domain to a Domain :: by Jaros{\l}aw Kotowicz :: :: Received May 31, 1990 :: Copyright (c) 1990-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, SUBSET_1, ZFMISC_1, PARTFUN1, RELAT_1, FUNCT_1, TARSKI, FUNCOP_1; notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1; constructors PARTFUN1, FUNCOP_1, RELSET_1; registrations FUNCT_1, RELSET_1; requirements SUBSET, BOOLE; definitions TARSKI, XBOOLE_0, FUNCT_1; equalities XBOOLE_0; expansions XBOOLE_0, FUNCT_1; theorems TARSKI, FUNCT_1, FUNCT_2, GRFUNC_1, FUNCOP_1, PARTFUN1, RELAT_1, RELSET_1, XBOOLE_0; schemes FUNCT_2, XBOOLE_0; begin reserve x,y,X,Y for set; reserve C,D,E for non empty set; reserve SC for Subset of C; reserve SD for Subset of D; reserve SE for Subset of E; reserve c,c1,c2 for Element of C; reserve d,d1,d2 for Element of D; reserve e for Element of E; reserve f,f1,g for PartFunc of C,D; reserve t for PartFunc of D,C; reserve s for PartFunc of D,E; reserve h for PartFunc of C,E; reserve F for PartFunc of D,D; theorem Th1: dom f = dom g & (for c st c in dom f holds f/.c = g/.c) implies f = g proof assume that A1: dom f = dom g and A2: for c st c in dom f holds f/.c = g/.c; now let x be object; assume A3: x in dom f; then reconsider y=x as Element of C; f/.y=g/.y by A2,A3; then (f qua Function).y = g/.y by A3,PARTFUN1:def 6; hence (f qua Function).x = (g qua Function).x by A1,A3,PARTFUN1:def 6; end; hence thesis by A1; end; theorem Th2: y in rng f iff ex c st c in dom f & y = f/.c proof thus y in rng f implies ex c st c in dom f & y = f/.c proof assume y in rng f; then consider x being object such that A1: x in dom f and A2: y = (f qua Function).x by FUNCT_1:def 3; reconsider x as Element of C by A1; take x; thus thesis by A1,A2,PARTFUN1:def 6; end; given c such that A3: c in dom f and A4: y = f/.c; (f qua Function).c in rng f by A3,FUNCT_1:def 3; hence thesis by A3,A4,PARTFUN1:def 6; end; theorem Th3: h = s*f iff (for c holds c in dom h iff c in dom f & f/.c in dom s) & for c st c in dom h holds h/.c = s/.(f/.c) proof thus h = s*f implies (for c holds c in dom h iff c in dom f & f/.c in dom s) & for c st c in dom h holds h/.c = s/.(f/.c) proof assume A1: h = s*f; A2: now let c; thus c in dom h implies c in dom f & f/.c in dom s proof assume c in dom h; then c in dom f & (f qua Function).c in dom s by A1,FUNCT_1:11; hence thesis by PARTFUN1:def 6; end; assume that A3: c in dom f and A4: f/.c in dom s; (f qua Function).c in dom s by A3,A4,PARTFUN1:def 6; hence c in dom h by A1,A3,FUNCT_1:11; end; hence for c holds c in dom h iff c in dom f & f/.c in dom s; let c; assume A5: c in dom h; then (h qua Function).c = (s qua Function).((f qua Function).c) by A1, FUNCT_1:12; then A6: h/.c = (s qua Function).((f qua Function).c) by A5,PARTFUN1:def 6; c in dom f by A2,A5; then A7: h/.c = (s qua Function).(f/.c) by A6,PARTFUN1:def 6; f/.c in dom s by A2,A5; hence thesis by A7,PARTFUN1:def 6; end; assume that A8: for c holds c in dom h iff c in dom f & f/.c in dom s and A9: for c st c in dom h holds h/.c = s/.(f/.c); A10: now let x be object; thus x in dom h implies x in dom f & (f qua Function).x in dom s proof assume A11: x in dom h; then reconsider y=x as Element of C; y in dom f & f/.y in dom s by A8,A11; hence thesis by PARTFUN1:def 6; end; thus x in dom f & (f qua Function).x in dom s implies x in dom h proof assume that A12: x in dom f and A13: (f qua Function).x in dom s; reconsider y=x as Element of C by A12; f/.y in dom s by A12,A13,PARTFUN1:def 6; hence thesis by A8,A12; end; end; now let x be object; assume A14: x in dom h; then reconsider y=x as Element of C; h/.y = s/.(f/.y) by A9,A14; then A15: (h qua Function).y = s/.(f/.y) by A14,PARTFUN1:def 6; f/.y in dom s by A8,A14; then A16: (h qua Function).x = (s qua Function).(f/.y) by A15,PARTFUN1:def 6; y in dom f by A8,A14; hence (h qua Function).x = (s qua Function).((f qua Function).x) by A16, PARTFUN1:def 6; end; hence thesis by A10,FUNCT_1:10; end; theorem Th4: c in dom f & f/.c in dom s implies (s*f)/.c = s/.(f/.c) proof assume c in dom f & f/.c in dom s; then c in dom (s*f) by Th3; hence thesis by Th3; end; theorem rng f c= dom s & c in dom f implies (s*f)/.c = s/.(f/.c) proof assume that A1: rng f c= dom s and A2: c in dom f; f/.c in rng f by A2,Th2; hence thesis by A1,A2,Th4; end; definition let D; let SD; redefine func id SD -> PartFunc of D,D; coherence proof dom id SD = SD & rng id SD = SD by RELAT_1:45; hence thesis by RELSET_1:4; end; end; theorem Th6: F = id SD iff dom F = SD & for d st d in SD holds F/.d = d proof thus F = id SD implies dom F = SD & for d st d in SD holds F/.d = d proof assume A1: F = id SD; hence A2: dom F = SD by RELAT_1:45; let d; assume A3: d in SD; then (F qua Function).d = d by A1,FUNCT_1:18; hence thesis by A2,A3,PARTFUN1:def 6; end; assume that A4: dom F = SD and A5: for d st d in SD holds F/.d = d; now let x be object; assume A6: x in SD; then reconsider x1=x as Element of D; F/.x1=x1 by A5,A6; hence (F qua Function).x = x by A4,A6,PARTFUN1:def 6; end; hence thesis by A4,FUNCT_1:17; end; theorem d in dom F /\ SD implies F/.d = (F*id SD)/.d proof assume A1: d in dom F /\ SD; then A2: d in dom F by XBOOLE_0:def 4; (F qua Function).d = ((F*(id SD)) qua Function).d by A1,FUNCT_1:20; then A3: F/.d = ((F*(id SD)) qua Function).d by A2,PARTFUN1:def 6; A4: d in SD by A1,XBOOLE_0:def 4; then A5: d in dom id SD by RELAT_1:45; (id SD)/.d in dom F by A2,A4,Th6; then d in dom (F*(id SD)) by A5,Th3; hence thesis by A3,PARTFUN1:def 6; end; theorem d in dom((id SD)*F) iff d in dom F & F/.d in SD proof thus d in dom((id SD)*F) implies d in dom F & F/.d in SD proof assume A1: d in dom((id SD)*F); then F/.d in dom (id SD) by Th3; hence thesis by A1,Th3,RELAT_1:45; end; assume that A2: d in dom F and A3: F/.d in SD; F/.d in dom (id SD) by A3,RELAT_1:45; hence thesis by A2,Th3; end; theorem (for c1,c2 st c1 in dom f & c2 in dom f & f/.c1 = f/.c2 holds c1 = c2) implies f is one-to-one proof assume A1: for c1,c2 st c1 in dom f & c2 in dom f & f/.c1 = f/.c2 holds c1 = c2; now let x,y be object; assume that A2: x in dom f and A3: y in dom f and A4: (f qua Function).x = (f qua Function).y; reconsider y1 = y as Element of C by A3; reconsider x1 = x as Element of C by A2; f/.x1 = (f qua Function).y1 by A2,A4,PARTFUN1:def 6; then f/.x1 = f/.y1 by A3,PARTFUN1:def 6; hence x=y by A1,A2,A3; end; hence thesis; end; theorem f is one-to-one & x in dom f & y in dom f & f/.x = f/.y implies x = y proof assume that A1: f is one-to-one and A2: x in dom f and A3: y in dom f; assume f/.x = f/.y; then f.x = f/.y by A2,PARTFUN1:def 6 .= f.y by A3,PARTFUN1:def 6; hence thesis by A1,A2,A3; end; definition let X,Y; let f be one-to-one PartFunc of X,Y; redefine func f" -> PartFunc of Y,X; coherence by PARTFUN1:9; end; theorem Th11: for f being one-to-one PartFunc of C,D holds for g be PartFunc of D,C holds g = f" iff dom g = rng f & for d,c holds d in rng f & c = g/.d iff c in dom f & d = f/.c proof let f be one-to-one PartFunc of C,D; let g be PartFunc of D,C; thus g = f" implies dom g = rng f & for d,c holds d in rng f & c = g/.d iff c in dom f & d = f/.c proof assume A1: g = f"; hence dom g = rng f by FUNCT_1:32; let d,c; A2: dom g = rng f by A1,FUNCT_1:32; thus d in rng f & c = g/.d implies c in dom f & d = f/.c proof assume that A3: d in rng f and A4: c = g/.d; c = (g qua Function).d by A2,A3,A4,PARTFUN1:def 6; then c in dom f & d = (f qua Function).c by A1,A3,FUNCT_1:32; hence thesis by PARTFUN1:def 6; end; assume that A5: c in dom f and A6: d = f/.c; d = (f qua Function).c by A5,A6,PARTFUN1:def 6; then d in rng f & c = (g qua Function).d by A1,A5,FUNCT_1:32; hence thesis by A2,PARTFUN1:def 6; end; assume that A7: dom g = rng f and A8: for d,c holds d in rng f & c = g/.d iff c in dom f & d = f/.c and A9: g <> f"; now per cases by A9,Th1; suppose dom (f") <> dom g; hence contradiction by A7,FUNCT_1:33; end; suppose ex d st d in dom (f") & f"/.d <> g/.d; then consider d such that A10: d in dom (f") and A11: f"/.d <> g/.d; f"/.d in rng (f") by A10,Th2; then A12: f"/.d in dom f by FUNCT_1:33; d in rng f by A10,FUNCT_1:33; then d = (f qua Function).(((f") qua Function).d) by FUNCT_1:35; then d = (f qua Function).(f"/.d) by A10,PARTFUN1:def 6; then d = f/.(f"/.d) by A12,PARTFUN1:def 6; hence contradiction by A8,A11,A12; end; end; hence contradiction; end; theorem for f being one-to-one PartFunc of C,D st c in dom f holds c = f"/.(f /.c) & c = (f"*f)/.c proof let f be one-to-one PartFunc of C,D; assume A1: c in dom f; hence A2: c = f"/.(f/.c) by Th11; f" = f"; then f/.c in rng f by A1,Th11; then f/.c in dom (f") by FUNCT_1:33; hence thesis by A1,A2,Th4; end; theorem for f being one-to-one PartFunc of C,D st d in rng f holds d = f/.(f" /.d) & d = (f*(f"))/.d proof let f be one-to-one PartFunc of C,D; assume A1: d in rng f; then d = ((f*f") qua Function).d & d in dom (f*f") by FUNCT_1:35,37; hence thesis by A1,Th11,PARTFUN1:def 6; end; theorem f is one-to-one & dom f = rng t & rng f = dom t & (for c,d st c in dom f & d in dom t holds f/.c = d iff t/.d = c) implies t = f" proof assume that A1: f is one-to-one & dom f = rng t & rng f = dom t and A2: for c,d st c in dom f & d in dom t holds f/.c = d iff t/.d = c; now let x,y be object; assume that A3: x in dom f and A4: y in dom t; reconsider y1=y as Element of D by A4; reconsider x1=x as Element of C by A3; thus (f qua Function).x = y implies (t qua Function).y = x proof assume (f qua Function).x = y; then f/.x1 = y1 by A3,PARTFUN1:def 6; then t/.y1 = x1 by A2,A3,A4; hence thesis by A4,PARTFUN1:def 6; end; assume (t qua Function).y = x; then t/.y1 = x1 by A4,PARTFUN1:def 6; then f/.x1 = y1 by A2,A3,A4; hence (f qua Function).x = y by A3,PARTFUN1:def 6; end; hence thesis by A1,FUNCT_1:38; end; theorem Th15: g = f|X iff dom g = dom f /\ X & for c st c in dom g holds g/.c = f/.c proof thus g = f|X implies dom g = dom f /\ X & for c st c in dom g holds g/.c = f /.c proof assume A1: g = f|X; hence dom g = dom f /\ X by RELAT_1:61; let c; assume A2: c in dom g; then (g qua Function).c = (f qua Function).c by A1,FUNCT_1:47; then A3: g/.c = (f qua Function).c by A2,PARTFUN1:def 6; dom g = dom f /\ X by A1,RELAT_1:61; then c in dom f by A2,XBOOLE_0:def 4; hence thesis by A3,PARTFUN1:def 6; end; assume that A4: dom g = dom f /\ X and A5: for c st c in dom g holds g/.c = f/.c; now let x be object; assume A6: x in dom g; then reconsider y=x as Element of C; g/.y = f/.y by A5,A6; then A7: (g qua Function).y = f/.y by A6,PARTFUN1:def 6; x in dom f by A4,A6,XBOOLE_0:def 4; hence (g qua Function).x = (f qua Function).x by A7,PARTFUN1:def 6; end; hence thesis by A4,FUNCT_1:46; end; theorem Th16: c in dom f /\ X implies f|X/.c = f/.c proof assume c in dom f /\ X; then c in dom (f|X) by RELAT_1:61; hence thesis by Th15; end; theorem c in dom f & c in X implies f|X/.c = f/.c proof assume c in dom f & c in X; then c in dom f /\ X by XBOOLE_0:def 4; hence thesis by Th16; end; theorem c in dom f & c in X implies f/.c in rng (f|X) proof assume that A1: c in dom f and A2: c in X; (f qua Function).c in rng (f|X) by A1,A2,FUNCT_1:50; hence thesis by A1,PARTFUN1:def 6; end; definition let C,D; let X,f; redefine func X|`f -> PartFunc of C,D; coherence by PARTFUN1:13; end; theorem Th19: g = X|`f iff (for c holds c in dom g iff c in dom f & f/.c in X) & for c st c in dom g holds g/.c = f/.c proof thus g = X|`f implies (for c holds c in dom g iff c in dom f & f/.c in X) & for c st c in dom g holds g/.c = f/.c proof assume A1: g = X|`f; now let c; thus c in dom g implies c in dom f & f/.c in X proof assume c in dom g; then c in dom f & (f qua Function).c in X by A1,FUNCT_1:54; hence thesis by PARTFUN1:def 6; end; assume that A2: c in dom f and A3: f/.c in X; (f qua Function).c in X by A2,A3,PARTFUN1:def 6; hence c in dom g by A1,A2,FUNCT_1:54; end; hence for c holds c in dom g iff c in dom f & f/.c in X; let c; assume A4: c in dom g; then (g qua Function).c = (f qua Function).c by A1,FUNCT_1:55; then A5: g/.c = (f qua Function).c by A4,PARTFUN1:def 6; c in dom f by A1,A4,FUNCT_1:54; hence thesis by A5,PARTFUN1:def 6; end; assume that A6: for c holds c in dom g iff c in dom f & f/.c in X and A7: for c st c in dom g holds g/.c = f/.c; A8: now let x be object; thus x in dom g implies x in dom f & (f qua Function).x in X proof assume A9: x in dom g; then reconsider x1=x as Element of C; x1 in dom f & f/.x1 in X by A6,A9; hence thesis by PARTFUN1:def 6; end; assume that A10: x in dom f and A11: (f qua Function).x in X; reconsider x1=x as Element of C by A10; f/.x1 in X by A10,A11,PARTFUN1:def 6; hence x in dom g by A6,A10; end; now let x be object; assume A12: x in dom g; then reconsider x1=x as Element of C; g/.x1 = f/.x1 by A7,A12; then A13: (g qua Function).x1 = f/.x1 by A12,PARTFUN1:def 6; x1 in dom f by A6,A12; hence (g qua Function).x = (f qua Function).x by A13,PARTFUN1:def 6; end; hence thesis by A8,FUNCT_1:53; end; theorem c in dom (X|`f) iff c in dom f & f/.c in X by Th19; theorem c in dom (X|`f) implies X|`f/.c = f/.c by Th19; theorem Th22: SD = f.: X iff for d holds d in SD iff ex c st c in dom f & c in X & d = f/.c proof thus SD = f.:X implies for d holds d in SD iff ex c st c in dom f & c in X & d = f/.c proof assume A1: SD = f.:X; let d; thus d in SD implies ex c st c in dom f & c in X & d = f/.c proof assume d in SD; then consider x being object such that A2: x in dom f and A3: x in X and A4: d = (f qua Function).x by A1,FUNCT_1:def 6; reconsider x as Element of C by A2; take x; thus x in dom f & x in X by A2,A3; thus thesis by A2,A4,PARTFUN1:def 6; end; given c such that A5: c in dom f and A6: c in X & d = f/.c; f/.c = (f qua Function).c by A5,PARTFUN1:def 6; hence thesis by A1,A5,A6,FUNCT_1:def 6; end; assume that A7: for d holds d in SD iff ex c st c in dom f & c in X & d = f/.c and A8: SD <> f.:X; consider x being object such that A9: not (x in SD iff x in f.:X) by A8,TARSKI:2; now per cases by A9; suppose A10: x in SD & not x in f.:X; then reconsider x as Element of D; consider c such that A11: c in dom f and A12: c in X and A13: x = f/.c by A7,A10; x = (f qua Function).c by A11,A13,PARTFUN1:def 6; hence contradiction by A10,A11,A12,FUNCT_1:def 6; end; suppose A14: x in f.:X & not x in SD; then consider y being object such that A15: y in dom f and A16: y in X and A17: x = (f qua Function).y by FUNCT_1:def 6; reconsider y as Element of C by A15; x = f/.y by A15,A17,PARTFUN1:def 6; hence contradiction by A7,A14,A15,A16; end; end; hence contradiction; end; theorem d in (f qua Relation of C,D).:X iff ex c st c in dom f & c in X & d = f/.c by Th22; theorem c in dom f implies Im(f,c) = {f/.c} proof assume A1: c in dom f; hence Im(f,c) = {(f qua Function).c} by FUNCT_1:59 .= {f/.c} by A1,PARTFUN1:def 6; end; theorem c1 in dom f & c2 in dom f implies f.:{c1,c2} = {f/.c1,f/.c2} proof assume that A1: c1 in dom f and A2: c2 in dom f; thus f.:{c1,c2} = {(f qua Function).c1,(f qua Function).c2} by A1,A2, FUNCT_1:60 .= {f/.c1,(f qua Function).c2} by A1,PARTFUN1:def 6 .= {f/.c1,f/.c2} by A2,PARTFUN1:def 6; end; theorem Th26: SC = f"X iff for c holds c in SC iff c in dom f & f/.c in X proof thus SC = f"X implies for c holds c in SC iff c in dom f & f/.c in X proof assume A1: SC = f"X; let c; thus c in SC implies c in dom f & f/.c in X proof assume c in SC; then c in dom f & (f qua Function).c in X by A1,FUNCT_1:def 7; hence thesis by PARTFUN1:def 6; end; assume that A2: c in dom f and A3: f/.c in X; (f qua Function).c in X by A2,A3,PARTFUN1:def 6; hence thesis by A1,A2,FUNCT_1:def 7; end; assume A4: for c holds c in SC iff c in dom f & f/.c in X; now let x be object; thus x in SC implies x in dom f & (f qua Function).x in X proof assume A5: x in SC; then reconsider x1=x as Element of C; x1 in dom f & f/.x1 in X by A4,A5; hence thesis by PARTFUN1:def 6; end; assume that A6: x in dom f and A7: (f qua Function).x in X; reconsider x1=x as Element of C by A6; f/.x1 in X by A6,A7,PARTFUN1:def 6; hence x in SC by A4,A6; end; hence thesis by FUNCT_1:def 7; end; theorem for f ex g being Function of C,D st for c st c in dom f holds g.c = f /.c proof let f; consider g being Function of C,D such that A1: for x being object st x in dom f holds g.x = (f qua Function).x by FUNCT_2:71; take g; let c; assume A2: c in dom f; then g.c = (f qua Function).c by A1; hence thesis by A2,PARTFUN1:def 6; end; theorem f tolerates g iff for c st c in dom f /\ dom g holds f/.c = g/.c proof thus f tolerates g implies for c st c in dom f /\ dom g holds f/.c = g/.c proof assume A1: f tolerates g; let c; assume A2: c in dom f /\ dom g; then A3: c in dom f by XBOOLE_0:def 4; (f qua Function).c = (g qua Function).c by A1,A2,PARTFUN1:def 4; then A4: f/.c = (g qua Function).c by A3,PARTFUN1:def 6; c in dom g by A2,XBOOLE_0:def 4; hence thesis by A4,PARTFUN1:def 6; end; assume A5: for c st c in dom f /\ dom g holds f/.c = g/.c; now let x be object; assume A6: x in dom f /\ dom g; then reconsider x1=x as Element of C; x in dom f & f/.x1 = g/.x1 by A5,A6,XBOOLE_0:def 4; then A7: (f qua Function).x = g/.x1 by PARTFUN1:def 6; x in dom g by A6,XBOOLE_0:def 4; hence (f qua Function).x = (g qua Function).x by A7,PARTFUN1:def 6; end; hence thesis by PARTFUN1:def 4; end; scheme PartFuncExD{D,C()->non empty set, P[object,object]}: ex f being PartFunc of D(),C( ) st (for d be Element of D() holds d in dom f iff (ex c be Element of C() st P [d,c])) & for d be Element of D() st d in dom f holds P[d,f/.d] proof defpred R[object] means ex c be Element of C() st P[\$1,c]; set x = the Element of C(); defpred Q[object,object] means ((ex c be Element of C() st P[\$1,c]) implies P[\$1, \$2]) & ((for c be Element of C() holds not P[\$1,c]) implies \$2=x); consider X be set such that A1: for x being object holds x in X iff x in D() & R[x] from XBOOLE_0:sch 1; for x being object holds x in X implies x in D() by A1; then reconsider X as Subset of D() by TARSKI:def 3; A2: for d be Element of D() ex z be Element of C() st Q[d,z] proof let d be Element of D(); (for c be Element of C() holds not P[d,c]) implies ex z be Element of C() st ((ex c be Element of C() st P[d,c]) implies P[d,z]) & ((for c be Element of C() holds not P[d,c]) implies z=x); hence thesis; end; consider g being Function of D(),C() such that A3: for d be Element of D() holds Q[d,g.d] from FUNCT_2:sch 3(A2); reconsider f=g|X as PartFunc of D(),C(); take f; A4: dom g = D() by FUNCT_2:def 1; thus for d be Element of D() holds d in dom f iff ex c be Element of C() st P[d,c] proof let d be Element of D(); dom f c= X by RELAT_1:58; hence d in dom f implies ex c be Element of C() st P[d,c] by A1; assume ex c be Element of C() st P[d,c]; then d in X by A1; then d in dom g /\ X by A4,XBOOLE_0:def 4; hence thesis by RELAT_1:61; end; let d be Element of D(); assume A5: d in dom f; dom f c= X by RELAT_1:58; then ex c be Element of C() st P[d,c] by A1,A5; then P[d,g.d] by A3; then P[d,(f qua Function).d] by A5,FUNCT_1:47; hence thesis by A5,PARTFUN1:def 6; end; scheme LambdaPFD{D,C()->non empty set, F(set)->Element of C(), P[set]}: ex f being PartFunc of D(),C() st (for d be Element of D() holds d in dom f iff P[d]) & for d be Element of D() st d in dom f holds f/.d = F(d) proof defpred Q[set,set] means P[\$1] & \$2 = F(\$1); consider f being PartFunc of D(),C() such that A1: for d be Element of D() holds d in dom f iff ex c be Element of C() st Q[d,c] and A2: for d be Element of D() st d in dom f holds Q[d,f/.d] from PartFuncExD; take f; thus for d be Element of D() holds d in dom f iff P[d] proof let d be Element of D(); thus d in dom f implies P[d] proof assume d in dom f; then ex c be Element of C() st P[d] & c = F(d) by A1; hence thesis; end; assume P[d]; then ex c be Element of C() st P[d] & c = F(d); hence thesis by A1; end; thus thesis by A2; end; scheme UnPartFuncD{C,D()->non empty set, X()->set, F(set)->Element of D()}: for f,g being PartFunc of C(),D() st (dom f=X() & for c be Element of C() st c in dom f holds f/.c = F(c)) & (dom g=X() & for c be Element of C() st c in dom g holds g /.c = F(c)) holds f = g proof let f,g be PartFunc of C(),D(); assume that A1: dom f=X() and A2: for c be Element of C() st c in dom f holds f/.c = F(c) and A3: dom g=X() and A4: for c be Element of C() st c in dom g holds g/.c = F(c); now let c be Element of C(); assume A5: c in dom f; hence f/.c = F(c) by A2 .= g/.c by A1,A3,A4,A5; end; hence thesis by A1,A3,Th1; end; definition let C,D; let SC,d; redefine func SC --> d -> PartFunc of C,D; coherence proof dom (SC --> d) = SC by FUNCOP_1:13; hence thesis by RELSET_1:7; end; end; theorem Th29: c in SC implies (SC --> d)/.c = d proof assume A1: c in SC; then dom (SC --> d) = SC & ((SC --> d) qua Function).c = d by FUNCOP_1:7,13; hence thesis by A1,PARTFUN1:def 6; end; theorem (for c st c in dom f holds f/.c = d) implies f = dom f --> d proof assume A1: for c st c in dom f holds f/.c = d; now let x be object; assume A2: x in dom f; then reconsider x1=x as Element of C; f/.x1 = d by A1,A2; hence ( f qua Function).x = d by A2,PARTFUN1:def 6; end; hence thesis by FUNCOP_1:11; end; theorem c in dom f implies f*(SE --> c) = SE --> f/.c proof assume A1: c in dom f; then f*(SE --> c) = SE --> (f qua Function).c by FUNCOP_1:17; hence thesis by A1,PARTFUN1:def 6; end; theorem (id SC) is total iff SC = C proof thus (id SC) is total implies SC = C proof assume (id SC) is total; then dom (id SC) = C by PARTFUN1:def 2; hence thesis by RELAT_1:45; end; assume SC = C; then dom (id SC) = C by RELAT_1:45; hence thesis by PARTFUN1:def 2; end; theorem (SC --> d) is total implies SC <> {} proof assume that A1: (SC --> d) is total and A2: SC = {}; dom (SC --> d) = C by A1,PARTFUN1:def 2; hence contradiction by A2,FUNCOP_1:10; end; theorem (SC --> d) is total iff SC = C proof thus (SC --> d) is total implies SC = C proof assume (SC --> d) is total; then dom (SC --> d) = C by PARTFUN1:def 2; hence thesis by FUNCOP_1:13; end; assume SC = C; then dom (SC --> d) = C by FUNCOP_1:13; hence thesis by PARTFUN1:def 2; end; :: :: PARTIAL FUNCTION CONSTANT ON SET :: definition let C,D,f; redefine attr f is constant means ex d st for c st c in dom f holds f.c = d; compatibility proof thus f is constant implies ex d st for c st c in dom f holds f.c = d proof assume A1: f is constant; per cases; suppose A2: dom f = {}; set d = the Element of D; take d; thus thesis by A2; end; suppose dom f <> {}; then consider c0 being object such that A3: c0 in dom f by XBOOLE_0:def 1; reconsider c0 as Element of C by A3; take d = f/.c0; let c; assume c in dom f; hence f.c = f.c0 by A1,A3 .= d by A3,PARTFUN1:def 6; end; end; given d such that A4: for c st c in dom f holds f.c = d; let x,y be object such that A5: x in dom f and A6: y in dom f; thus f.x = d by A4,A5 .=f.y by A4,A6; end; end; theorem Th35: f|X is constant iff ex d st for c st c in X /\ dom f holds f/.c = d proof thus f|X is constant implies ex d st for c st c in X /\ dom f holds f/.c = d proof given d such that A1: for c st c in dom(f|X) holds (f|X).c = d; take d; let c; assume A2: c in X /\ dom f; then A3: c in dom(f|X) by RELAT_1:61; c in dom f by A2,XBOOLE_0:def 4; hence f/.c = f.c by PARTFUN1:def 6 .= (f|X).c by A3,FUNCT_1:47 .= d by A1,A3; end; given d such that A4: for c st c in X /\ dom f holds f/.c = d; take d; let c; assume A5: c in dom(f|X); then A6: c in X /\ dom f by RELAT_1:61; then A7: c in dom f by XBOOLE_0:def 4; thus (f|X).c = f.c by A5,FUNCT_1:47 .= f/.c by A7,PARTFUN1:def 6 .= d by A4,A6; end; theorem f|X is constant iff for c1,c2 st c1 in X /\ dom f & c2 in X /\ dom f holds f/.c1=f/.c2 proof thus f|X is constant implies for c1,c2 st c1 in X /\ dom f & c2 in X /\ dom f holds f/.c1=f/.c2 proof assume f|X is constant; then consider d such that A1: for c st c in X /\ dom f holds f/.c = d by Th35; let c1,c2; assume that A2: c1 in X /\ dom f and A3: c2 in X /\ dom f; f/.c1 = d by A1,A2; hence thesis by A1,A3; end; assume A4: for c1,c2 st c1 in X /\ dom f & c2 in X /\ dom f holds f/.c1=f/.c2; now per cases; suppose A5: X /\ dom f = {}; now set d = the Element of D; take d; let c; thus c in X /\ dom f implies f/.c = d by A5; end; hence thesis by Th35; end; suppose A6: X /\ dom f <> {}; set x = the Element of X /\ dom f; x in dom f by A6,XBOOLE_0:def 4; then reconsider x as Element of C; for c holds c in X /\ dom f implies f/.c = f/.x by A4; hence thesis by Th35; end; end; hence thesis; end; theorem X meets dom f implies (f|X is constant iff ex d st rng (f|X) = {d}) proof assume A1: X /\ dom f <> {}; thus f|X is constant implies ex d st rng (f|X) = {d} proof assume f|X is constant; then consider d such that A2: for c st c in X /\ dom f holds f/.c = d by Th35; take d; thus rng (f|X) c= {d} proof let x be object; assume x in rng (f|X); then consider y being object such that A3: y in dom (f|X) and A4: ((f|X) qua Function).y = x by FUNCT_1:def 3; reconsider y as Element of C by A3; dom (f|X) = X /\ dom f by RELAT_1:61; then d = f/.y by A2,A3 .= f|X/.y by A3,Th15 .= x by A3,A4,PARTFUN1:def 6; hence thesis by TARSKI:def 1; end; thus {d} c= rng (f|X) proof set y = the Element of X /\ dom f; y in dom f by A1,XBOOLE_0:def 4; then reconsider y as Element of C; let x be object such that A5: x in {d}; A6: dom (f|X) = X /\ dom f by RELAT_1:61; then f|X/.y = f/.y by A1,Th15 .= d by A1,A2 .= x by A5,TARSKI:def 1; hence thesis by A1,A6,Th2; end; end; given d such that A7: rng (f|X) = {d}; take d; let c; assume A8: c in dom (f|X); then f|X/.c in {d} by A7,Th2; then (f|X).c in {d} by A8,PARTFUN1:def 6; hence thesis by TARSKI:def 1; end; theorem f|X is constant & Y c= X implies f|Y is constant proof assume that A1: f|X is constant and A2: Y c= X; consider d such that A3: for c st c in X /\ dom f holds f/.c = d by A1,Th35; now let c; assume c in Y /\ dom f; then c in Y & c in dom f by XBOOLE_0:def 4; then c in X /\ dom f by A2,XBOOLE_0:def 4; hence f/.c = d by A3; end; hence thesis by Th35; end; theorem Th39: X misses dom f implies f|X is constant proof assume A1: X /\ dom f = {}; now set d = the Element of D; take d; let c; thus c in X /\ dom f implies f/.c = d by A1; end; hence thesis by Th35; end; theorem f|SC = dom (f|SC) --> d implies f|SC is constant proof assume A1: f|SC = dom (f|SC) --> d; now let c; assume c in SC /\ dom f; then A2: c in dom (f|SC) by RELAT_1:61; then f|SC/.c = d by A1,Th29; hence f/.c = d by A2,Th15; end; hence thesis by Th35; end; theorem f|{x} is constant proof now per cases; suppose {x} /\ dom f = {}; then {x} misses dom f; hence thesis by Th39; end; suppose A1: {x} /\ dom f <> {}; set y = the Element of {x} /\ dom f; y in {x} & y in dom f by A1,XBOOLE_0:def 4; then reconsider x1=x as Element of C by TARSKI:def 1; now take d = f/.x1; let c; assume c in {x} /\ dom f; then c in {x} by XBOOLE_0:def 4; hence f/.c = f/.x1 by TARSKI:def 1; end; hence thesis by Th35; end; end; hence thesis; end; theorem f|X is constant & f|Y is constant & X /\ Y meets dom f implies f|(X \/ Y) is constant proof assume that A1: f|X is constant and A2: f|Y is constant and A3: X /\ Y /\ dom f <> {}; consider d1 such that A4: for c st c in X /\ dom f holds f/.c = d1 by A1,Th35; set x = the Element of X /\ Y /\ dom f; A5: x in X /\ Y by A3,XBOOLE_0:def 4; A6: x in dom f by A3,XBOOLE_0:def 4; then reconsider x as Element of C; x in Y by A5,XBOOLE_0:def 4; then A7: x in Y /\ dom f by A6,XBOOLE_0:def 4; consider d2 such that A8: for c st c in Y /\ dom f holds f/.c = d2 by A2,Th35; x in X by A5,XBOOLE_0:def 4; then x in X /\ dom f by A6,XBOOLE_0:def 4; then f/.x = d1 by A4; then A9: d1 = d2 by A8,A7; take d1; let c; assume A10: c in dom(f|(X \/ Y)); then A11: c in (X \/ Y) /\ dom f by RELAT_1:61; then A12: c in dom f by XBOOLE_0:def 4; A13: c in X \/ Y by A11,XBOOLE_0:def 4; now per cases by A13,XBOOLE_0:def 3; suppose c in X; then c in X /\ dom f by A12,XBOOLE_0:def 4; hence f/.c = d1 by A4; end; suppose c in Y; then c in Y /\ dom f by A12,XBOOLE_0:def 4; hence f/.c = d1 by A8,A9; end; end; then (f|(X \/ Y))/.c = d1 by A11,Th16; hence thesis by A10,PARTFUN1:def 6; end; theorem f|Y is constant implies f|X|Y is constant proof assume f|Y is constant; then consider d such that A1: for c st c in Y /\ dom f holds f/.c = d by Th35; take d; let c; assume A2: c in dom (f|X|Y); then A3: c in Y /\ dom (f|X) by RELAT_1:61; then A4: c in Y by XBOOLE_0:def 4; A5: c in dom (f|X) by A3,XBOOLE_0:def 4; then c in dom f /\ X by RELAT_1:61; then c in dom f by XBOOLE_0:def 4; then c in Y /\ dom f by A4,XBOOLE_0:def 4; then f/.c = d by A1; then (f|X)/.c = d by A5,Th15; then (f|X|Y)/.c = d by A3,Th16; hence thesis by A2,PARTFUN1:def 6; end; theorem (SC --> d)|SC is constant proof take d; let c; assume A1: c in dom((SC --> d)|SC); then A2: c in SC /\ dom (SC --> d) by RELAT_1:61; then c in SC by XBOOLE_0:def 4; then (SC --> d)/.c = d by Th29; then ((SC --> d)|SC)/.c = d by A2,Th16; hence thesis by A1,PARTFUN1:def 6; end; :: :: OF PARTIAL FUNCTION FROM A DOMAIN TO A DOMAIN :: theorem dom f c= dom g & (for c st c in dom f holds f/.c = g/.c) implies f c= g proof assume that A1: dom f c= dom g and A2: for c st c in dom f holds f/.c = g/.c; now let x be object; assume A3: x in dom f; then reconsider x1=x as Element of C; f/.x1 = g/.x1 by A2,A3; then (f qua Function).x = g/.x1 by A3,PARTFUN1:def 6; hence (f qua Function).x = (g qua Function).x by A1,A3,PARTFUN1:def 6; end; hence thesis by A1,GRFUNC_1:2; end; theorem Th46: c in dom f & d = f/.c iff [c,d] in f proof thus c in dom f & d = f/.c implies [c,d] in f proof assume that A1: c in dom f and A2: d = f/.c; d = (f qua Function).c by A1,A2,PARTFUN1:def 6; hence thesis by A1,FUNCT_1:1; end; assume [c,d] in f; then c in dom f & d = (f qua Function).c by FUNCT_1:1; hence thesis by PARTFUN1:def 6; end; theorem [c,e] in (s*f) implies [c,f/.c] in f & [f/.c,e] in s proof assume A1: [c,e] in (s*f); then A2: [(f qua Function).c,e] in s by GRFUNC_1:4; A3: [c,(f qua Function).c] in f by A1,GRFUNC_1:4; then c in dom f by FUNCT_1:1; hence thesis by A3,A2,PARTFUN1:def 6; end; theorem f = {[c,d]} implies f/.c = d proof assume A1: f = {[c,d]}; then [c,d] in f by TARSKI:def 1; then A2: c in dom f by FUNCT_1:1; (f qua Function).c = d by A1,GRFUNC_1:6; hence thesis by A2,PARTFUN1:def 6; end; theorem dom f = {c} implies f = {[c,f/.c]} proof assume dom f = {c}; then c in dom f & f = {[c,(f qua Function).c]} by GRFUNC_1:7,TARSKI:def 1; hence thesis by PARTFUN1:def 6; end; theorem f1 = f /\ g & c in dom f1 implies f1/.c = f/.c & f1/.c = g/.c proof assume that A1: f1 = f /\ g and A2: c in dom f1; (f1 qua Function).c = (g qua Function).c by A1,A2,GRFUNC_1:11; then A3: f1/.c = (g qua Function).c by A2,PARTFUN1:def 6; A4: [c,(f1 qua Function).c] in f1 by A2,FUNCT_1:1; then [c,(f1 qua Function).c] in f by A1,XBOOLE_0:def 4; then A5: c in dom f by FUNCT_1:1; [c,(f1 qua Function).c] in g by A1,A4,XBOOLE_0:def 4; then A6: c in dom g by FUNCT_1:1; (f1 qua Function).c = (f qua Function).c by A1,A2,GRFUNC_1:11; then f1/.c = (f qua Function).c by A2,PARTFUN1:def 6; hence thesis by A5,A6,A3,PARTFUN1:def 6; end; theorem c in dom f & f1 = f \/ g implies f1/.c = f/.c proof assume that A1: c in dom f and A2: f1 = f \/ g; [c,(f qua Function).c] in f by A1,FUNCT_1:1; then [c,(f qua Function).c] in f1 by A2,XBOOLE_0:def 3; then A3: c in dom f1 by FUNCT_1:1; (f1 qua Function).c = (f qua Function).c by A1,A2,GRFUNC_1:15; then f1/.c = (f qua Function).c by A3,PARTFUN1:def 6; hence thesis by A1,PARTFUN1:def 6; end; theorem c in dom g & f1 = f \/ g implies f1/.c = g/.c proof assume that A1: c in dom g and A2: f1 = f \/ g; [c,(g qua Function).c] in g by A1,FUNCT_1:1; then [c,(g qua Function).c] in f1 by A2,XBOOLE_0:def 3; then A3: c in dom f1 by FUNCT_1:1; (f1 qua Function).c = (g qua Function).c by A1,A2,GRFUNC_1:15; then f1/.c = (g qua Function).c by A3,PARTFUN1:def 6; hence thesis by A1,PARTFUN1:def 6; end; theorem c in dom f1 & f1 = f \/ g implies f1/.c = f/.c or f1/.c = g/.c proof assume that A1: c in dom f1 and A2: f1 = f \/ g; [c,f1/.c] in f1 by A1,Th46; then A3: [c,f1/.c] in f or [c,f1/.c] in g by A2,XBOOLE_0:def 3; now per cases by A3,FUNCT_1:1; suppose c in dom f; then [c,f/.c] in f by Th46; then [c,f/.c] in f1 by A2,XBOOLE_0:def 3; hence thesis by Th46; end; suppose c in dom g; then [c,g/.c] in g by Th46; then [c,g/.c] in f1 by A2,XBOOLE_0:def 3; hence thesis by Th46; end; end; hence thesis; end; theorem c in dom f & c in SC iff [c,f/.c] in (f|SC) proof thus c in dom f & c in SC implies [c,f/.c] in (f|SC) proof assume that A1: c in dom f and A2: c in SC; [c,(f qua Function).c] in (f|SC) by A1,A2,GRFUNC_1:22; hence thesis by A1,PARTFUN1:def 6; end; assume [c,f/.c] in (f|SC); then c in dom (f|SC) by FUNCT_1:1; then c in dom f /\ SC by RELAT_1:61; hence thesis by XBOOLE_0:def 4; end; theorem c in dom f & f/.c in SD iff [c,f/.c] in (SD|`f) proof thus c in dom f & f/.c in SD implies [c,f/.c] in (SD|`f) proof assume that A1: c in dom f and A2: f/.c in SD; (f qua Function).c in SD by A1,A2,PARTFUN1:def 6; then [c,(f qua Function).c] in (SD|`f) by A1,GRFUNC_1:24; hence thesis by A1,PARTFUN1:def 6; end; assume [c,f/.c] in (SD|`f); then c in dom (SD|`f) by FUNCT_1:1; then c in dom f & (f qua Function).c in SD by FUNCT_1:54; hence thesis by PARTFUN1:def 6; end; theorem c in f"SD iff [c,f/.c] in f & f/.c in SD proof thus c in f"SD implies [c,f/.c] in f & f/.c in SD proof assume A1: c in f"SD; then A2: (f qua Function).c in SD by GRFUNC_1:26; A3: [c,(f qua Function).c] in f by A1,GRFUNC_1:26; then c in dom f by FUNCT_1:1; hence thesis by A3,A2,PARTFUN1:def 6; end; assume that A4: [c,f/.c] in f and A5: f/.c in SD; c in dom f by A4,Th46; hence thesis by A5,Th26; end; theorem Th57: f|X is constant iff ex d st for c st c in X /\ dom f holds f.c = d proof hereby assume f|X is constant; then consider d such that A1: for c st c in X /\ dom f holds f/.c = d by Th35; take d; let c; assume A2: c in X /\ dom f; then c in dom f by XBOOLE_0:def 4; hence f.c = f/.c by PARTFUN1:def 6 .= d by A1,A2; end; given d such that A3: for c st c in X /\ dom f holds f.c = d; take d; let c; assume A4: c in dom(f|X); then A5: c in X /\ dom f by RELAT_1:61; then A6: c in dom f by XBOOLE_0:def 4; thus (f|X).c = (f|X)/.c by A4,PARTFUN1:def 6 .= f/.c by A5,Th16 .= f.c by A6,PARTFUN1:def 6 .= d by A3,A5; end; theorem f|X is constant iff for c1,c2 st c1 in X /\ dom f & c2 in X /\ dom f holds f.c1=f.c2 proof thus f|X is constant implies for c1,c2 st c1 in X /\ dom f & c2 in X /\ dom f holds f.c1=f.c2 proof assume f|X is constant; then consider d such that A1: for c st c in X /\ dom f holds f.c = d by Th57; let c1,c2; assume that A2: c1 in X /\ dom f and A3: c2 in X /\ dom f; f.c1 = d by A1,A2; hence thesis by A1,A3; end; assume A4: for c1,c2 st c1 in X /\ dom f & c2 in X /\ dom f holds f.c1=f.c2; now per cases; suppose A5: X /\ dom f = {}; now set d = the Element of D; take d; let c; thus c in X /\ dom f implies f.c = d by A5; end; hence thesis by Th57; end; suppose A6: X /\ dom f <> {}; set x = the Element of X /\ dom f; now let c; A7: x in dom f by A6,XBOOLE_0:def 4; assume c in X /\ dom f; hence f.c = f.x by A4,A7 .= f/.x by A7,PARTFUN1:def 6; end; hence thesis by Th57; end; end; hence thesis; end; theorem d in f.:X implies ex c st c in dom f & c in X & d = f.c proof assume d in f.:X; then consider x being object such that A1: x in dom f and A2: x in X & d = (f qua Function).x by FUNCT_1:def 6; reconsider x as Element of C by A1; take x; thus thesis by A1,A2; end; theorem f is one-to-one implies (d in rng f & c = (f").d iff c in dom f & d = f.c) proof A1: f" = (f qua Function)"; assume f is one-to-one; hence thesis by A1,FUNCT_1:32; end; theorem for Y for f,g be Y-valued Function st f c= g for x st x in dom f holds f/.x = g/.x proof let Y; let f,g be Y-valued Function; assume A1: f c= g; then A2: dom f c= dom g by GRFUNC_1:2; let x; assume A3: x in dom f; then f.x = g.x by A1,GRFUNC_1:2; then f/.x = (g qua Function).x by A3,PARTFUN1:def 6; hence thesis by A2,A3,PARTFUN1:def 6; end;