environ
 vocabularies
   RELAT_1, BOOLE, XREAL_0, FUNCT_1, FUNCT_4, PARTFUN1, CAT_1, CAT_4,
   PBOOLE, PRALG_1, MSUALG_3, MSPF_1;
 notations
   TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, RELAT_1, FUNCT_1,FUNCT_2, RELSET_1,
   FUNCT_4, CQC_LANG, FUNCOP_1,PARTFUN1, PBOOLE, PRALG_1, MSUALG_1, MSUALG_3,
   PRE_CIRC;
 constructors
   ZFMISC_1, DOMAIN_1, FUNCT_4, CQC_LANG, MSUALG_1, MSUALG_3, PRE_CIRC,
   PRALG_1;
 registrations
   SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, PBOOLE, CQC_LANG, PRALG_1,
   MSUALG_3;
 requirements
   BOOLE, SUBSET;
 theorems
   TARSKI, XBOOLE_0, XBOOLE_1,
   BOOLE, SUBSET_1, ZFMISC_1, RELAT_1, FUNCT_1, GRFUNC_1,
   FUNCT_2,
   RELSET_1, TOPMETR2, FUNCOP_1, PARTFUN1, FUNCT_4, CQC_LANG, PBOOLE, MSUALG_1,
   MSUALG_3;
 definitions
   FUNCT_1, PRALG_1, MSUALG_3, FUNCOP_1;
 schemes
   PBOOLE;

begin

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

reserve i, j, x, y, X, Y for set;

:::::::::::: Auxiliary ::::::::::::::::::::::::::::::::::::::::::::::::::::::

:::::::::::: Functions ::::::::::::::::::::::::::::::::::::::::::::::::::::::

reserve f, F for Function;

theorem :: MSPF_1:1
 x in dom (x .--> y) & (for i st i in dom (x .--> y) holds i = x);

theorem :: MSPF_1:2
 y in rng (x .--> y) & (for i st i in rng (x .--> y) holds i = y);

theorem :: MSPF_1:3
 x in dom (f +* (x .--> y));

theorem :: MSPF_1:4
 (f +* (x .--> y)).x = y;

theorem :: MSPF_1:5
 i in dom f & i <> x implies f.i = (f +* (x .--> y)).i;

theorem :: MSPF_1:6
 F is "1-1" & f is one-to-one implies F +* (i .--> f) is "1-1";

theorem :: MSPF_1:7
 x .--> y is one-to-one;

theorem :: MSPF_1:8
 f is one-to-one & not y in rng f implies f +* (x .--> y) is one-to-one;

theorem :: MSPF_1:9
 x in dom f implies f = f +* (x .--> f.x);

theorem :: MSPF_1:10
 x in dom f implies dom (f +* (x .--> y)) = dom f;

theorem :: MSPF_1:11
 i in dom f & not x in dom f implies (f +* (x .--> y)).i = f.i;

:::::::::::: Partial functions ::::::::::::::::::::::::::::::::::::::::::::::

theorem :: MSPF_1:12   :: In PARTFUN1:111 Y must be non empty
 for X, Y being set, f being Function of X, Y holds f is PartFunc of X, Y;

theorem :: MSPF_1:13
 for X, Y being set, f being Function of X, Y holds f is Relation of X, Y;

definition let X, Y be non empty set;
  let x be Element of X, y be Element of Y;
 redefine func x .--> y -> PartFunc of X, Y;
end;


:::::::::::: Many Sorted partial Functions ::::::::::::::::::::::::::::::::::

reserve I for set,
        A, B for ManySortedSet of I;

definition
  let I, A, B;
 mode MSPartFunc of A, B -> ManySortedSet of I means
:: MSPF_1:def 1

 for i being set st i in I holds it.i is PartFunc of A.i, B.i;
end;

registration
  let I, A, B;
 cluster -> Function-yielding MSPartFunc of A,B;
end;

theorem :: MSPF_1:14
 for f being ManySortedFunction of A, B holds f is MSPartFunc of A, B;

definition
  let I, A, B;
 func [0](A, B) -> MSPartFunc of A, B means
:: MSPF_1:def 2
 it = [0]I;
end;

theorem :: MSPF_1:15
i in I implies [0](A, B).i = {};

theorem :: MSPF_1:16
[0](A, B) is "1-1";

registration
  let I, A, B;
 cluster "1-1" MSPartFunc of A, B;
end;

reserve I for non empty set,
        A, B for ManySortedSet of I,
        P for MSPartFunc of A, B,
        i for Element of I;

definition
  let I, A, B, P, i;
 redefine func P.i -> PartFunc of A.i, B.i;
end;

theorem :: MSPF_1:17
 for p being PartFunc of A.i, B.i
  holds P +* (i .--> p) is MSPartFunc of A, B;