:: Partial Functions from a Domain to a Domain
::  by Jaros{\l}aw Kotowicz
::
:: Received May 31, 1990
:: Copyright (c) 1990-2019 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;