:: Schemes of Existence of some Types of Functions
::  by Jaros{\l}aw Kotowicz
::
:: Received September 21, 1990
:: Copyright (c) 1990-2012 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 NUMBERS, SUBSET_1, REAL_1, RELAT_1, ARYTM_3, INT_1, CARD_1,
      XXREAL_0, SEQ_1, VALUED_0, FUNCT_1, NAT_1, TARSKI, ORDINAL2, ARYTM_1,
      XBOOLE_0, PARTFUN1, ZFMISC_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XCMPLX_0, REAL_1,
      ORDINAL1, NAT_1, NAT_D, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
      VALUED_0, SEQ_1, XXREAL_0, RECDEF_1;
 constructors PARTFUN1, XXREAL_0, NAT_1, NAT_D, SEQ_1, SEQM_3, RECDEF_1,
      MEMBERED, RELSET_1;
 registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, SEQM_3,
      VALUED_0;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
 definitions TARSKI, XBOOLE_0;
 theorems ZFMISC_1, NAT_1, FUNCT_1, FUNCT_2, SEQM_3, PARTFUN1, RELSET_1,
      XBOOLE_1, NAT_D, ORDINAL1, XXREAL_0, XTUPLE_0;
 schemes NAT_1, FUNCT_2, RECDEF_1, SUBSET_1, CLASSES1, XBOOLE_0;

begin

reserve x,y,z for set;
reserve n,m,k for Element of NAT;
reserve r for Real;

theorem
  for n ex m st n = 2*m or n = 2*m+1
proof
  let n;
  take n div 2;
  set k = n mod 2;
A1: k = 0 or k = 1
  proof
    k < 1 + 1 by NAT_D:1;
    then
A2: k <= 0 + 1 by NAT_1:13;
    now
      per cases by A2,NAT_1:8;
      suppose
        k <= 0;
        hence thesis by NAT_1:2;
      end;
      suppose
        k = 0 + 1;
        hence thesis;
      end;
    end;
    hence thesis;
  end;
  n = 2*(n div 2) + (n mod 2) by NAT_D:2;
  hence thesis by A1;
end;

theorem Th2:
  for n ex m st n = 3*m or n = 3*m+1 or n = 3*m+2
proof
  let n;
  take n div 3;
  set w = n mod 3;
A1: w = 0 or w = 1 or w = 2
  proof
    w < 2 + 1 by NAT_D:1;
    then
A2: w <= 1 + 1 by NAT_1:13;
    now
      per cases by A2,NAT_1:8;
      suppose
A3:     w <= 1;
        now
          per cases by A3,NAT_1:8;
          suppose
            w <= 0;
            hence thesis by NAT_1:2;
          end;
          suppose
            w = 0 + 1;
            hence thesis;
          end;
        end;
        hence thesis;
      end;
      suppose
        w = 1 + 1;
        hence thesis;
      end;
    end;
    hence thesis;
  end;
A4: n = 3*(n div 3) + (n mod 3) by NAT_D:2;
  now
    per cases by A1;
    suppose
      w = 0;
      hence thesis by A4;
    end;
    suppose
      w = 1;
      hence thesis by NAT_D:2;
    end;
    suppose
      w = 2;
      hence thesis by NAT_D:2;
    end;
  end;
  hence thesis;
end;

theorem Th3:
  for n ex m st n = 4*m or n = 4*m+1 or n = 4*m+2 or n = 4*m+3
proof
  let n;
  take n div 4;
  set o = n mod 4;
A1: o = 0 or o = 1 or o = 2 or o = 3
  proof
    o < 3 + 1 by NAT_D:1;
    then
A2: o <= 2 + 1 by NAT_1:13;
    now
      per cases by A2,NAT_1:8;
      suppose
A3:     o <= 2;
        now
          per cases by A3,NAT_1:8;
          suppose
A4:         o <= 1;
            now
              per cases by A4,NAT_1:8;
              suppose
                o <= 0;
                hence thesis by NAT_1:2;
              end;
              suppose
                o = 0 + 1;
                hence thesis;
              end;
            end;
            hence thesis;
          end;
          suppose
            o = 1 + 1;
            hence thesis;
          end;
        end;
        hence thesis;
      end;
      suppose
        o = 2 + 1;
        hence thesis;
      end;
    end;
    hence thesis;
  end;
  n = 4*(n div 4) + (n mod 4) by NAT_D:2;
  hence thesis by A1;
end;

theorem Th4:
  for n ex m st n = 5*m or n = 5*m+1 or n = 5*m+2 or n = 5*m+3 or n = 5*m+4
proof
  let n;
  take n div 5;
  set l = n mod 5;
A1: l = 0 or l = 1 or l = 2 or l = 3 or l = 4
  proof
    l < 4 + 1 by NAT_D:1;
    then
A2: l <= 3 + 1 by NAT_1:13;
    now
      per cases by A2,NAT_1:8;
      suppose
A3:     l <= 3;
        now
          per cases by A3,NAT_1:8;
          suppose
A4:         l <= 2;
            now
              per cases by A4,NAT_1:8;
              suppose
A5:             l <= 1;
                now
                  per cases by A5,NAT_1:8;
                  suppose
                    l <= 0;
                    hence thesis by NAT_1:2;
                  end;
                  suppose
                    l = 0 + 1;
                    hence thesis;
                  end;
                end;
                hence thesis;
              end;
              suppose
                l = 1 + 1;
                hence thesis;
              end;
            end;
            hence thesis;
          end;
          suppose
            l = 2 + 1;
            hence thesis;
          end;
        end;
        hence thesis;
      end;
      suppose
        l = 3 + 1;
        hence thesis;
      end;
    end;
    hence thesis;
  end;
  n = 5*(n div 5) + (n mod 5) by NAT_D:2;
  hence thesis by A1;
end;

scheme
  ExRealSubseq{s()->Real_Sequence,P[set]}: ex q being Real_Sequence st q is
subsequence of s() & (for n holds P[q.n]) & for n st (for r st r = s().n holds
  P[r]) ex m st s().n = q.m
provided
A1: for n ex m st n <= m & P[s().m]
proof
  defpred P[set,set] means for n,m st $1 = n & $2 = m holds n < m & P[s().m] &
  for k st n < k & P[s().k] holds m <= k;
  defpred X[set,set,set] means P[$2,$3];
  defpred X[set] means P[s().$1];
  ex m1 be Element of NAT st 0 <= m1 & P[s().m1] by A1;
  then
A2: ex m be Nat st X[m];
  consider M be Nat such that
A3: X[M] & for n be Nat st X[n] holds M <= n from NAT_1:sch 5(A2);
  reconsider M9 = M as Element of NAT by ORDINAL1:def 12;
A4: now
    let n;
    consider m such that
A5: n + 1 <= m & P[s().m] by A1;
    take m;
    thus n < m & P[s().m] by A5,NAT_1:13;
  end;
A6: for n for x be Element of NAT ex y be Element of NAT st X[n,x,y]
  proof
    let n;
    let x be Element of NAT;
    defpred X[Nat] means x < $1 & P[s().$1];
    ex m be Element of NAT st X[m] by A4;
    then
A7: ex m be Nat st X[m];
    consider l be Nat such that
A8: X[l] & for k be Nat st X[k] holds l <= k from NAT_1:sch 5(A7);
    reconsider l as Element of NAT by ORDINAL1:def 12;
    take l;
    thus thesis by A8;
  end;
  consider F be Function of NAT,NAT such that
A9: F.0 = M9 & for n be Element of NAT holds X[n,F.n,F.(n+1)] from
  RECDEF_1:sch 2(A6);
  dom F = NAT & rng F c= REAL by FUNCT_2:def 1,XBOOLE_1:1;
  then reconsider F as natural-valued Real_Sequence by FUNCT_2:def 1,RELSET_1:4
;
  for n holds F.n < F.(n+1) by A9;
  then reconsider F as increasing sequence of NAT by SEQM_3:def 6;
A10: for n st P[s().n] ex m st F.m = n
  proof
    defpred X[set] means P[s().$1] & for m holds F.m <> $1;
    assume ex n st X[n];
    then
A11: ex n be Nat st X[n];
    consider M1 be Nat such that
A12: X[M1] & for n be Nat st X[n] holds M1 <= n from NAT_1:sch 5(A11);
    defpred X[Nat] means $1 < M1 & P[s().$1] & ex m st F.m = $1;
A13: ex n be Nat st X[n]
    proof
      take M;
      M <= M1 & M <> M1 by A3,A9,A12;
      hence M < M1 by XXREAL_0:1;
      thus P[s().M] by A3;
      take 0;
      thus thesis by A9;
    end;
A14: for n be Nat st X[n] holds n <= M1;
    consider X be Nat such that
A15: X[X] & for n be Nat st X[n] holds n <= X from NAT_1:sch 6(A14,A13
    );
A16: for k st X < k & k < M1 holds not P[s().k]
    proof
      given k such that
A17:  X < k and
A18:  k < M1 & P[s().k];
      now
        per cases;
        suppose
          ex m st F.m = k;
          hence contradiction by A15,A17,A18;
        end;
        suppose
          for m holds F.m <> k;
          hence contradiction by A12,A18;
        end;
      end;
      hence contradiction;
    end;
    consider m such that
A19: F.m = X by A15;
A20: X < F.(m+1) & P[s().(F.(m+1))] by A9,A19;
    M1 in NAT by ORDINAL1:def 12;
    then
A21: F.(m+1) <= M1 by A9,A12,A15,A19;
    now
      assume F.(m+1) <> M1;
      then F.(m+1) < M1 by A21,XXREAL_0:1;
      hence contradiction by A16,A20;
    end;
    hence contradiction by A12;
  end;
  take q = s()*F;
  defpred X[set] means P[q.$1];
A22: for k st X[k] holds X[k+1]
  proof
    let k such that
    P[q.k];
    P[F.k,F.(k+1)] by A9;
    then P[s().(F.(k+1) ) ];
    hence thesis by FUNCT_2:15;
  end;
  thus q is subsequence of s();
A23: X[0] by A3,A9,FUNCT_2:15;
  thus for n holds X[n] from NAT_1:sch 1(A23,A22);
  let n;
  assume for r st r = s().n holds P[r];
  then consider m such that
A24: F.m = n by A10;
  take m;
  thus thesis by A24,FUNCT_2:15;
end;

scheme
  ExRealSeq2{F,G(set)->Real}: ex s being Real_Sequence st for n holds s.(2*n)
  = F(n) & s.(2*n+1) = G(n) proof
  defpred X[set] means ex m st $1 = 2*m;
  consider N be Subset of NAT such that
A1: for n holds n in N iff X[n] from SUBSET_1:sch 3;
  defpred X[set] means ex m st $1 = 2*m+1;
  consider M be Subset of NAT such that
A2: for n holds n in M iff X[n] from SUBSET_1:sch 3;
  defpred X[Element of NAT, set] means ($1 in N implies $2 = F($1/2)) & ($1 in
  M implies $2 = G(($1-1)/2));
A3: for n ex r st X[n,r]
  proof
    let n;
    now
      assume
A4:   n in N;
      take r = F(n/2);
      now
        assume n in M;
        then
A5:     ex k st n = 2*k + 1 by A2;
        consider m such that
A6:     n = 2*m by A1,A4;
        n = 2*m + 0 by A6;
        hence contradiction by A5,NAT_1:18;
      end;
      hence thesis;
    end;
    hence thesis;
  end;
  consider f being Function of NAT,REAL such that
A7: for n holds X[n,f.n] from FUNCT_2:sch 3(A3);
  reconsider f as Real_Sequence;
  take f;
  let n;
  2*n in N by A1;
  hence f.(2*n) = F(2*n/2) by A7
    .= F(n);
  2*n + 1 in M by A2;
  hence f.(2*n + 1) = G((2*n + 1 - 1)/2) by A7
    .= G(n);
end;

scheme
  ExRealSeq3{F,G,H(set)->Real}: ex s being Real_Sequence st for n holds s.(3*n
  ) = F(n) & s.(3*n+1) = G(n) & s.(3*n+2) = H(n) proof
  defpred X[set] means ex m st $1 = 3*m;
  consider E be Subset of NAT such that
A1: for n holds n in E iff X[n] from SUBSET_1:sch 3;
  defpred X[set] means ex m st $1 = 3*m+1;
  consider G be Subset of NAT such that
A2: for n holds n in G iff X[n] from SUBSET_1:sch 3;
  defpred X[set] means ex m st $1 = 3*m+2;
  consider K be Subset of NAT such that
A3: for n holds n in K iff X[n] from SUBSET_1:sch 3;
  defpred X[Element of NAT, set] means ($1 in E implies $2 = F($1/3)) & ($1 in
  G implies $2 = G(($1-1)/3)) & ( $1 in K implies $2 = H(($1-2)/3));
A4: for n ex r st X[n,r]
  proof
    let n;
    consider m such that
A5: n = 3*m or n = 3*m + 1 or n = 3*m + 2 by Th2;
    now
      per cases by A5;
      suppose
A6:     n = 3*m;
        take r = F(n/3);
A7:     n = 3*m + 0 by A6;
A8:     now
          assume n in K;
          then ex k st n = 3*k + 2 by A3;
          hence contradiction by A7,NAT_1:18;
        end;
        now
          assume n in G;
          then ex k st n = 3*k + 1 by A2;
          hence contradiction by A7,NAT_1:18;
        end;
        hence thesis by A8;
      end;
      suppose
A9:     n = 3*m + 1;
        take r = G((n-1)/3);
A10:    now
          assume n in E;
          then consider k such that
A11:      n = 3*k by A1;
          n = 3*k + 0 by A11;
          hence contradiction by A9,NAT_1:18;
        end;
        now
          assume n in K;
          then ex k st n = 3*k + 2 by A3;
          hence contradiction by A9,NAT_1:18;
        end;
        hence thesis by A10;
      end;
      suppose
A12:    n = 3*m + 2;
        take r = H((n-2)/3);
A13:    now
          assume n in E;
          then consider k such that
A14:      n = 3*k by A1;
          n = 3*k + 0 by A14;
          hence contradiction by A12,NAT_1:18;
        end;
        now
          assume n in G;
          then ex k st n = 3*k + 1 by A2;
          hence contradiction by A12,NAT_1:18;
        end;
        hence thesis by A13;
      end;
    end;
    hence thesis;
  end;
  consider f being Function of NAT,REAL such that
A15: for n holds X[n,f.n] from FUNCT_2:sch 3(A4);
  reconsider f as Real_Sequence;
  take f;
  let n;
  3*n in E by A1;
  hence f.(3*n) = F(3*n/3) by A15
    .= F(n);
  3*n+1 in G by A2;
  hence f.(3*n+1) = G((3*n + 1 - 1)/3) by A15
    .= G(n);
  3*n+2 in K by A3;
  hence f.(3*n+2) = H((3*n + 2 - 2)/3) by A15
    .= H(n);
end;

scheme
  ExRealSeq4{F,G,H,I(set)->Real}: ex s being Real_Sequence st for n holds s.(4
  *n) = F(n) & s.(4*n+1) = G(n) & s.(4*n+2) = H(n) & s.(4*n+3) = I(n) proof
  defpred X[set] means ex m st $1 = 4*m;
  consider Q be Subset of NAT such that
A1: for n holds n in Q iff X[n] from SUBSET_1:sch 3;
  defpred X[set] means ex m st $1 = 4*m+1;
  consider R be Subset of NAT such that
A2: for n holds n in R iff X[n] from SUBSET_1:sch 3;
  defpred X[set] means ex m st $1 = 4*m+2;
  consider P be Subset of NAT such that
A3: for n holds n in P iff X[n] from SUBSET_1:sch 3;
  defpred X[set] means ex m st $1 = 4*m+3;
  consider L be Subset of NAT such that
A4: for n holds n in L iff X[n] from SUBSET_1:sch 3;
  defpred X[Element of NAT, set] means ($1 in Q implies $2 = F($1/4)) & ($1 in
  R implies $2 = G(($1-1)/4)) & ( $1 in P implies $2 = H(($1-2)/4)) & ($1 in L
  implies $2 = I(($1-3)/4));
A5: for n ex r st X[n,r]
  proof
    let n;
    consider m such that
A6: n = 4*m or n = 4*m + 1 or n = 4*m + 2 or n = 4*m + 3 by Th3;
    now
      per cases by A6;
      suppose
A7:     n = 4*m;
        take r=F(n/4);
A8:     n=4*m+0 by A7;
A9:     now
          assume n in P;
          then ex k st n=4*k+2 by A3;
          hence contradiction by A8,NAT_1:18;
        end;
A10:    now
          assume n in L;
          then ex k st n=4*k+3 by A4;
          hence contradiction by A8,NAT_1:18;
        end;
        now
          assume n in R;
          then ex k st n=4*k+1 by A2;
          hence contradiction by A8,NAT_1:18;
        end;
        hence thesis by A9,A10;
      end;
      suppose
A11:    n = 4*m + 1;
        take r=G((n-1)/4);
A12:    now
          assume n in Q;
          then consider k such that
A13:      n=4*k by A1;
          n=4*k+0 by A13;
          hence contradiction by A11,NAT_1:18;
        end;
A14:    now
          assume n in L;
          then ex k st n=4*k+3 by A4;
          hence contradiction by A11,NAT_1:18;
        end;
        now
          assume n in P;
          then ex k st n=4*k+2 by A3;
          hence contradiction by A11,NAT_1:18;
        end;
        hence thesis by A12,A14;
      end;
      suppose
A15:    n=4*m+2;
        take r=H((n-2)/4);
A16:    now
          assume n in Q;
          then consider k such that
A17:      n=4*k by A1;
          n=4*k+0 by A17;
          hence contradiction by A15,NAT_1:18;
        end;
A18:    now
          assume n in L;
          then ex k st n=4*k+3 by A4;
          hence contradiction by A15,NAT_1:18;
        end;
        now
          assume n in R;
          then ex k st n=4*k+1 by A2;
          hence contradiction by A15,NAT_1:18;
        end;
        hence thesis by A16,A18;
      end;
      suppose
A19:    n=4*m+3;
        take r=I((n-3)/4);
A20:    now
          assume n in Q;
          then consider k such that
A21:      n=4*k by A1;
          n=4*k+0 by A21;
          hence contradiction by A19,NAT_1:18;
        end;
A22:    now
          assume n in P;
          then ex k st n=4*k+2 by A3;
          hence contradiction by A19,NAT_1:18;
        end;
        now
          assume n in R;
          then ex k st n=4*k+1 by A2;
          hence contradiction by A19,NAT_1:18;
        end;
        hence thesis by A20,A22;
      end;
    end;
    hence thesis;
  end;
  consider f being Function of NAT,REAL such that
A23: for n holds X[n,f.n] from FUNCT_2:sch 3(A5);
  reconsider f as Real_Sequence;
  take f;
  let n;
  4*n in Q by A1;
  hence f.(4*n)=F(4*n/4) by A23
    .= F(n);
  4*n+1 in R by A2;
  hence f.(4*n+1)=G((4*n+1-1)/4) by A23
    .= G(n);
  4*n+2 in P by A3;
  hence f.(4*n+2)=H((4*n+2-2)/4) by A23
    .= H(n);
  4*n+3 in L by A4;
  hence f.(4*n+3)=I((4*n+3-3)/4) by A23
    .= I(n);
end;

scheme
  ExRealSeq5{F,G,H,I,J(set)->Real}: ex s being Real_Sequence st for n holds s.
(5*n) = F(n) & s.(5*n+1) = G(n) & s.(5*n+2) = H(n) & s.(5*n+3) = I(n) & s.(5*n+
  4) = J(n) proof
  defpred X[set] means ex m st $1 = 5*m;
  consider N be Subset of NAT such that
A1: for n holds n in N iff X[n] from SUBSET_1:sch 3;
  defpred X[set] means ex m st $1 = 5*m+1;
  consider M be Subset of NAT such that
A2: for n holds n in M iff X[n] from SUBSET_1:sch 3;
  defpred X[set] means ex m st $1 = 5*m+2;
  consider K be Subset of NAT such that
A3: for n holds n in K iff X[n] from SUBSET_1:sch 3;
  defpred X[set] means ex m st $1 = 5*m+3;
  consider L be Subset of NAT such that
A4: for n holds n in L iff X[n] from SUBSET_1:sch 3;
  defpred X[set] means ex m st $1 = 5*m+4;
  consider O be Subset of NAT such that
A5: for n holds n in O iff X[n] from SUBSET_1:sch 3;
  defpred X[Element of NAT, set] means ($1 in N implies $2 = F($1/5)) & ($1 in
  M implies $2 = G(($1-1)/5)) & ( $1 in K implies $2 = H(($1-2)/5)) & ($1 in L
  implies $2 = I(($1-3)/5)) & ($1 in O implies $2=J(($1-4)/5));
A6: for n ex r st X[n,r]
  proof
    let n;
    consider m such that
A7: n=5*m or n=5*m+1 or n=5*m+2 or n=5*m+3 or n=5*m+4 by Th4;
    now
      per cases by A7;
      suppose
A8:     n=5*m;
        take r=F(n/5);
A9:     n=5*m+0 by A8;
A10:    now
          assume n in K;
          then ex k st n=5*k+2 by A3;
          hence contradiction by A9,NAT_1:18;
        end;
A11:    now
          assume n in O;
          then ex k st n=5*k+4 by A5;
          hence contradiction by A9,NAT_1:18;
        end;
A12:    now
          assume n in L;
          then ex k st n=5*k+3 by A4;
          hence contradiction by A9,NAT_1:18;
        end;
        now
          assume n in M;
          then ex k st n=5*k+1 by A2;
          hence contradiction by A9,NAT_1:18;
        end;
        hence thesis by A10,A12,A11;
      end;
      suppose
A13:    n=5*m+1;
A14:    now
          assume n in O;
          then ex k st n=5*k+4 by A5;
          hence contradiction by A13,NAT_1:18;
        end;
A15:    now
          assume n in L;
          then ex k st n=5*k+3 by A4;
          hence contradiction by A13,NAT_1:18;
        end;
        take r=G((n-1)/5);
A16:    now
          assume n in N;
          then consider k such that
A17:      n=5*k by A1;
          n=5*k+0 by A17;
          hence contradiction by A13,NAT_1:18;
        end;
        now
          assume n in K;
          then ex k st n=5*k+2 by A3;
          hence contradiction by A13,NAT_1:18;
        end;
        hence thesis by A16,A15,A14;
      end;
      suppose
A18:    n=5*m+2;
A19:    now
          assume n in O;
          then ex k st n=5*k+4 by A5;
          hence contradiction by A18,NAT_1:18;
        end;
A20:    now
          assume n in L;
          then ex k st n=5*k+3 by A4;
          hence contradiction by A18,NAT_1:18;
        end;
        take r=H((n-2)/5);
A21:    now
          assume n in N;
          then consider k such that
A22:      n=5*k by A1;
          n=5*k+0 by A22;
          hence contradiction by A18,NAT_1:18;
        end;
        now
          assume n in M;
          then ex k st n=5*k+1 by A2;
          hence contradiction by A18,NAT_1:18;
        end;
        hence thesis by A21,A20,A19;
      end;
      suppose
A23:    n=5*m+3;
A24:    now
          assume n in O;
          then ex k st n=5*k+4 by A5;
          hence contradiction by A23,NAT_1:18;
        end;
A25:    now
          assume n in K;
          then ex k st n=5*k+2 by A3;
          hence contradiction by A23,NAT_1:18;
        end;
        take r=I((n-3)/5);
A26:    now
          assume n in N;
          then consider k such that
A27:      n=5*k by A1;
          n=5*k+0 by A27;
          hence contradiction by A23,NAT_1:18;
        end;
        now
          assume n in M;
          then ex k st n=5*k+1 by A2;
          hence contradiction by A23,NAT_1:18;
        end;
        hence thesis by A26,A25,A24;
      end;
      suppose
A28:    n=5*m+4;
A29:    now
          assume n in L;
          then ex k st n=5*k+3 by A4;
          hence contradiction by A28,NAT_1:18;
        end;
A30:    now
          assume n in K;
          then ex k st n=5*k+2 by A3;
          hence contradiction by A28,NAT_1:18;
        end;
        take r=J((n-4)/5);
A31:    now
          assume n in N;
          then consider k such that
A32:      n=5*k by A1;
          n=5*k+0 by A32;
          hence contradiction by A28,NAT_1:18;
        end;
        now
          assume n in M;
          then ex k st n=5*k+1 by A2;
          hence contradiction by A28,NAT_1:18;
        end;
        hence thesis by A31,A30,A29;
      end;
    end;
    hence thesis;
  end;
  consider f being Function of NAT,REAL such that
A33: for n holds X[n,f.n] from FUNCT_2:sch 3(A6);
  reconsider f as Real_Sequence;
  take f;
  let n;
  5*n in N by A1;
  hence f.(5*n) = F(5*n/5) by A33
    .= F(n);
  5*n+1 in M by A2;
  hence f.(5*n+1) = G((5*n+1-1)/5) by A33
    .= G(n);
  5*n+2 in K by A3;
  hence f.(5*n+2) = H((5*n+2-2)/5) by A33
    .= H(n);
  5*n+3 in L by A4;
  hence f.(5*n+3) = I((5*n+3-3)/5) by A33
    .= I(n);
  5*n+4 in O by A5;
  hence f.(5*n+4) = J((5*n+4-4)/5) by A33
    .= J(n);
end;

scheme
  PartFuncExD2{C, D()->non empty set, P,Q[set], F,G(set)->Element of D()}: ex
f being PartFunc of C(),D() st (for c be Element of C() holds c in dom f iff P[
c] or Q[c]) & for c be Element of C() st c in dom f holds (P[c] implies f.c = F
  (c)) & (Q[c] implies f.c = G(c))
provided
A1: for c be Element of C() st P[c] holds not Q[c]
proof
  defpred X[set,set] means (P[$1] implies $2 = F($1)) & (Q[$1] implies $2 = G(
  $1));
  defpred X[set] means P[$1] or Q[$1];
  consider X be set such that
A2: for x holds x in X iff x in C() & X[x] from XBOOLE_0:sch 1;
A3: for x st x in X ex y st X[x,y]
  proof
    let x;
    assume
A4: x in X;
    then reconsider x9 = x as Element of C() by A2;
    now
      per cases by A2,A4;
      suppose
A5:     P[x];
        take y = F(x);
        not Q[x9] by A1,A5;
        hence thesis;
      end;
      suppose
A6:     Q[x];
        take y = G(x);
        not P[x9] by A1,A6;
        hence thesis;
      end;
    end;
    hence thesis;
  end;
  consider f being Function such that
A7: dom f = X & for x st x in X holds X[x,f.x] from CLASSES1:sch 1(A3);
A8: X c= C()
  proof
    let x;
    assume x in X;
    hence thesis by A2;
  end;
  rng f c= D()
  proof
    let x;
    assume x in rng f;
    then consider y such that
A9: y in dom f and
A10: x = f.y by FUNCT_1:def 3;
    now
      per cases by A2,A7,A9;
      suppose
        P[y];
        then f.y = F(y) by A7,A9;
        hence thesis by A10;
      end;
      suppose
        Q[y];
        then f.y = G(y) by A7,A9;
        hence thesis by A10;
      end;
    end;
    hence thesis;
  end;
  then reconsider q = f as PartFunc of C(),D() by A8,A7,RELSET_1:4;
  take q;
  thus for c be Element of C() holds c in dom q iff P[c] or Q[c] by A2,A7;
  let b be Element of C();
  assume b in dom q;
  hence thesis by A7;
end;

scheme
  PartFuncExD29{C, D()->non empty set,P,Q[set], F,G(set)->Element of D()}: ex
f being PartFunc of C(),D() st (for c be Element of C() holds c in dom f iff P[
c] or Q[c]) & for c be Element of C() st c in dom f holds (P[c] implies f.c = F
  (c)) & (Q[c] implies f.c = G(c))
provided
A1: for c be Element of C() st P[c] & Q[c] holds F(c)=G(c)
proof
  defpred X[set,set] means (P[$1] implies $2 = F($1)) & (Q[$1] implies $2 = G(
  $1));
  defpred X[set] means P[$1] or Q[$1];
  consider Y be set such that
A2: for x holds x in Y iff x in C() & X[x] from XBOOLE_0:sch 1;
A3: for x st x in Y ex y st X[x,y]
  proof
    let x;
    assume
A4: x in Y;
    then reconsider a9 = x as Element of C() by A2;
    now
      per cases by A2,A4;
      suppose
A5:     P[a9];
        take y = F(a9);
        now
          per cases;
          suppose
            Q[a9];
            then F(a9) = G(a9) by A1,A5;
            hence thesis;
          end;
          suppose
            not Q[a9];
            hence thesis;
          end;
        end;
        hence thesis;
      end;
      suppose
A6:     Q[a9];
        take y = G(a9);
        now
          per cases;
          suppose
            P[a9];
            then F(a9) = G(a9) by A1,A6;
            hence thesis;
          end;
          suppose
            not P[a9];
            hence thesis;
          end;
        end;
        hence thesis;
      end;
    end;
    hence thesis;
  end;
  consider f being Function such that
A7: dom f = Y & for x st x in Y holds X[x,f.x] from CLASSES1:sch 1(A3);
A8: Y c= C()
  proof
    let x;
    assume x in Y;
    hence thesis by A2;
  end;
  rng f c= D()
  proof
    let x;
    assume x in rng f;
    then consider y such that
A9: y in dom f and
A10: x = f.y by FUNCT_1:def 3;
    now
      per cases by A2,A7,A9;
      suppose
        P[y];
        then f.y = F(y) by A7,A9;
        hence thesis by A10;
      end;
      suppose
        Q[y];
        then f.y = G(y) by A7,A9;
        hence thesis by A10;
      end;
    end;
    hence thesis;
  end;
  then reconsider q = f as PartFunc of C(),D() by A8,A7,RELSET_1:4;
  take q;
  thus for c be Element of C() holds c in dom q iff P[c] or Q[c] by A2,A7;
  let e be Element of C();
  assume e in dom q;
  hence thesis by A7;
end;

scheme
  PartFuncExD299{C, D()->non empty set,P[set], F,G(set)->Element of D()}: ex f
being PartFunc of C(),D() st f is total & for c be Element of C() st c in dom f
  holds (P[c] implies f.c = F(c)) & (not P[c] implies f.c = G(c)) proof
  defpred Y[set] means not P[$1];
A1: for c be Element of C() st P[c] holds not Y[c];
  consider f being PartFunc of C(),D() such that
A2: (for c be Element of C() holds c in dom f iff P[c] or Y[c]) & for c
be Element of C() st c in dom f holds (P[c] implies f.c = F(c)) & (Y[c] implies
  f.c = G(c)) from PartFuncExD2(A1);
  take f;
  dom f = C()
  proof
    thus dom f c= C();
    let x;
    assume x in C();
    then reconsider b9 = x as Element of C();
    P[b9] or not P[b9];
    hence thesis by A2;
  end;
  hence f is total by PARTFUN1:def 2;
  thus thesis by A2;
end;

scheme
  PartFuncExD3{C, D()->non empty set,P,Q,R[set], F,G,H(set)->Element of D()}:
ex f being PartFunc of C(),D() st (for c be Element of C() holds c in dom f iff
  P[c] or Q[c] or R[c]) & for c be Element of C() st c in dom f holds (P[c]
  implies f.c = F(c)) & (Q[c] implies f.c = G(c)) & (R[c] implies f.c = H(c))
provided
A1: for c be Element of C() holds (P[c] implies not Q[c]) & (P[c]
implies not R[c]) & (Q[c] implies not R[c])
proof
  defpred X[set,set] means (P[$1] implies $2 = F($1)) & (Q[$1] implies $2 = G(
  $1)) & (R[$1] implies $2 = H($1));
  defpred X[set] means P[$1] or Q[$1] or R[$1];
  consider Z be set such that
A2: for x holds x in Z iff x in C() & X[x] from XBOOLE_0:sch 1;
A3: for x st x in Z ex y st X[x,y]
  proof
    let x;
    assume
A4: x in Z;
    then reconsider c9 = x as Element of C() by A2;
    now
      per cases by A2,A4;
      suppose
A5:     P[x];
        take y = F(x);
        ( not Q[c9])& not R[c9] by A1,A5;
        hence thesis;
      end;
      suppose
A6:     Q[x];
        take y = G(x);
        ( not P[c9])& not R[c9] by A1,A6;
        hence thesis;
      end;
      suppose
A7:     R[x];
        take y = H(x);
        ( not P[c9])& not Q[c9] by A1,A7;
        hence thesis;
      end;
    end;
    hence thesis;
  end;
  consider f being Function such that
A8: dom f = Z & for x st x in Z holds X[x,f.x] from CLASSES1:sch 1(A3);
A9: rng f c= D()
  proof
    let x;
    assume x in rng f;
    then consider y such that
A10: y in dom f and
A11: x = f.y by FUNCT_1:def 3;
    now
      per cases by A2,A8,A10;
      suppose
        P[y];
        then f.y = F(y) by A8,A10;
        hence thesis by A11;
      end;
      suppose
        Q[y];
        then f.y = G(y) by A8,A10;
        hence thesis by A11;
      end;
      suppose
        R[y];
        then f.y = H(y) by A8,A10;
        hence thesis by A11;
      end;
    end;
    hence thesis;
  end;
  Z c= C()
  proof
    let x;
    assume x in Z;
    hence thesis by A2;
  end;
  then reconsider q = f as PartFunc of C(),D() by A8,A9,RELSET_1:4;
  take q;
  thus for c be Element of C() holds c in dom q iff P[c] or Q[c] or R[c] by A2
,A8;
  let g be Element of C();
  assume g in dom q;
  hence thesis by A8;
end;

scheme
  PartFuncExD39{C, D()->non empty set,P,Q,R[set], F,G,H(set)->Element of D()}:
ex f being PartFunc of C(),D() st (for c be Element of C() holds c in dom f iff
  P[c] or Q[c] or R[c]) & for c be Element of C() st c in dom f holds (P[c]
  implies f.c = F(c)) & (Q[c] implies f.c = G(c)) & (R[c] implies f.c = H(c))
provided
A1: for c be Element of C() holds (P[c] & Q[c] implies F(c)=G(c)) & (P[c
] & R[c] implies F(c)=H(c)) & (Q[c] & R[c] implies G(c)=H(c))
proof
  defpred X[set,set] means (P[$1] implies $2 = F($1)) & (Q[$1] implies $2 = G(
  $1)) & (R[$1] implies $2 = H($1));
  defpred X[set] means P[$1] or Q[$1] or R[$1];
  consider V be set such that
A2: for x holds x in V iff x in C() & X[x] from XBOOLE_0:sch 1;
A3: for x st x in V ex y st X[x,y]
  proof
    let x;
    assume
A4: x in V;
    then reconsider d9 = x as Element of C() by A2;
    now
      per cases by A2,A4;
      suppose
A5:     P[d9];
        take y = F(d9);
        now
          per cases;
          suppose
A6:         Q[d9];
            then
A7:         F(d9) = G(d9) by A1,A5;
            now
              per cases;
              suppose
                R[d9];
                then G(d9) = H(d9) by A1,A6;
                hence thesis by A7;
              end;
              suppose
                not R[d9];
                hence thesis by A7;
              end;
            end;
            hence thesis;
          end;
          suppose
A8:         not Q[d9];
            now
              per cases;
              suppose
                R[d9];
                then F(d9) = H(d9) by A1,A5;
                hence thesis by A8;
              end;
              suppose
                not R[d9];
                hence thesis by A8;
              end;
            end;
            hence thesis;
          end;
        end;
        hence thesis;
      end;
      suppose
A9:     Q[d9];
        take y = G(x);
        now
          per cases;
          suppose
            P[d9];
            then
A10:        F(d9) = G(d9) by A1,A9;
            now
              per cases;
              suppose
                R[d9];
                then G(d9) = H(d9) by A1,A9;
                hence thesis by A10;
              end;
              suppose
                not R[d9];
                hence thesis by A10;
              end;
            end;
            hence thesis;
          end;
          suppose
A11:        not P[d9];
            now
              per cases;
              suppose
                R[d9];
                then G(d9) = H(d9) by A1,A9;
                hence thesis by A11;
              end;
              suppose
                not R[d9];
                hence thesis by A11;
              end;
            end;
            hence thesis;
          end;
        end;
        hence thesis;
      end;
      suppose
A12:    R[d9];
        take y = H(x);
        now
          per cases;
          suppose
            P[d9];
            then
A13:        F(d9) = H(d9) by A1,A12;
            now
              per cases;
              suppose
                Q[d9];
                then G(d9) = H(d9) by A1,A12;
                hence thesis by A13;
              end;
              suppose
                not Q[d9];
                hence thesis by A13;
              end;
            end;
            hence thesis;
          end;
          suppose
A14:        not P[d9];
            now
              per cases;
              suppose
                Q[d9];
                then G(d9) = H(d9) by A1,A12;
                hence thesis by A14;
              end;
              suppose
                not Q[d9];
                hence thesis by A14;
              end;
            end;
            hence thesis;
          end;
        end;
        hence thesis;
      end;
    end;
    hence thesis;
  end;
  consider f being Function such that
A15: dom f = V & for x st x in V holds X[x,f.x] from CLASSES1:sch 1(A3);
A16: rng f c= D()
  proof
    let x;
    assume x in rng f;
    then consider y such that
A17: y in dom f and
A18: x = f.y by FUNCT_1:def 3;
    now
      per cases by A2,A15,A17;
      suppose
        P[y];
        then f.y = F(y) by A15,A17;
        hence thesis by A18;
      end;
      suppose
        Q[y];
        then f.y = G(y) by A15,A17;
        hence thesis by A18;
      end;
      suppose
        R[y];
        then f.y = H(y) by A15,A17;
        hence thesis by A18;
      end;
    end;
    hence thesis;
  end;
  V c= C()
  proof
    let x;
    assume x in V;
    hence thesis by A2;
  end;
  then reconsider q = f as PartFunc of C(),D() by A15,A16,RELSET_1:4;
  take q;
  thus for c be Element of C() holds c in dom q iff P[c] or Q[c] or R[c] by A2
,A15;
  let i be Element of C();
  assume i in dom q;
  hence thesis by A15;
end;

scheme
  PartFuncExD4{C, D()->non empty set,P,Q,R,S[set], F,G,H,I(set)->Element of D(
)}: ex f being PartFunc of C(),D() st (for c be Element of C() holds c in dom f
iff P[c] or Q[c] or R[c] or S[c]) & for c be Element of C() st c in dom f holds
(P[c] implies f.c = F(c)) & (Q[c] implies f.c = G(c)) & (R[c] implies f.c = H(c
  )) & (S[c] implies f.c = I(c))
provided
A1: for c be Element of C() holds (P[c] implies not Q[c]) & (P[c]
implies not R[c]) & (P[c] implies not S[c]) & (Q[c] implies not R[c]) & (Q[c]
implies not S[c]) & (R[c] implies not S[c])
proof
  defpred X[set,set] means (P[$1] implies $2 = F($1)) & (Q[$1] implies $2 = G(
  $1)) & (R[$1] implies $2 = H($1)) & (S[$1] implies $2 = I($1));
  defpred X[set] means P[$1] or Q[$1] or R[$1] or S[$1];
  consider B be set such that
A2: for x holds x in B iff x in C() & X[x] from XBOOLE_0:sch 1;
A3: for x st x in B ex y st X[x,y]
  proof
    let x;
    assume
A4: x in B;
    then reconsider e9 = x as Element of C() by A2;
    now
      per cases by A2,A4;
      suppose
A5:     P[x];
        take y = F(x);
A6:     not S[e9] by A1,A5;
        ( not Q[e9])& not R[e9] by A1,A5;
        hence thesis by A6;
      end;
      suppose
A7:     Q[x];
        take y = G(x);
A8:     not S[e9] by A1,A7;
        ( not P[e9])& not R[e9] by A1,A7;
        hence thesis by A8;
      end;
      suppose
A9:     R[x];
        take y = H(x);
A10:    not S[e9] by A1,A9;
        ( not P[e9])& not Q[e9] by A1,A9;
        hence thesis by A10;
      end;
      suppose
A11:    S[x];
        take y = I(x);
A12:    not R[e9] by A1,A11;
        ( not P[e9])& not Q[e9] by A1,A11;
        hence thesis by A12;
      end;
    end;
    hence thesis;
  end;
  consider f being Function such that
A13: dom f = B & for y st y in B holds X[y,f.y] from CLASSES1:sch 1(A3);
A14: rng f c= D()
  proof
    let x;
    assume x in rng f;
    then consider y such that
A15: y in dom f and
A16: x = f.y by FUNCT_1:def 3;
    now
      per cases by A2,A13,A15;
      suppose
        P[y];
        then f.y = F(y) by A13,A15;
        hence thesis by A16;
      end;
      suppose
        Q[y];
        then f.y = G(y) by A13,A15;
        hence thesis by A16;
      end;
      suppose
        R[y];
        then f.y = H(y) by A13,A15;
        hence thesis by A16;
      end;
      suppose
        S[y];
        then f.y = I(y) by A13,A15;
        hence thesis by A16;
      end;
    end;
    hence thesis;
  end;
  B c= C()
  proof
    let x;
    assume x in B;
    hence thesis by A2;
  end;
  then reconsider q = f as PartFunc of C(),D() by A13,A14,RELSET_1:4;
  take q;
  thus for c be Element of C() holds c in dom q iff P[c] or Q[c] or R[c] or S[
  c ] by A2,A13;
  let o be Element of C();
  assume o in dom q;
  hence thesis by A13;
end;

scheme
  PartFuncExS2{X, Y()->set,P,Q[set],F,G(set)->set}: ex f being PartFunc of X()
,Y() st (for x holds x in dom f iff x in X() & (P[x] or Q[x])) & for x st x in
  dom f holds (P[x] implies f.x=F(x)) & (Q[x] implies f.x=G(x))
provided
A1: for x st x in X() holds P[x] implies not Q[x] and
A2: for x st x in X() & P[x] holds F(x) in Y() and
A3: for x st x in X() & Q[x] holds G(x) in Y()
proof
  defpred X[set,set] means (P[$1] implies $2 = F($1)) & (Q[$1] implies $2 = G(
  $1));
  defpred X[set] means P[$1] or Q[$1];
  consider A be set such that
A4: for x holds x in A iff x in X() & X[x] from XBOOLE_0:sch 1;
A5: for x st x in A ex y st X[x,y]
  proof
    let x;
    assume
A6: x in A;
    then
A7: x in X() by A4;
    now
      per cases by A4,A6;
      suppose
A8:     P[x];
        take y = F(x);
        not Q[x] by A1,A7,A8;
        hence thesis;
      end;
      suppose
A9:     Q[x];
        take y = G(x);
        not P[x] by A1,A7,A9;
        hence thesis;
      end;
    end;
    hence thesis;
  end;
  consider f being Function such that
A10: dom f = A & for x st x in A holds X[x,f.x] from CLASSES1:sch 1(A5);
A11: A c= X()
  proof
    let x;
    assume x in A;
    hence thesis by A4;
  end;
  rng f c= Y()
  proof
    let x;
    assume x in rng f;
    then consider y such that
A12: y in dom f and
A13: x = f.y by FUNCT_1:def 3;
    now
      per cases by A4,A10,A12;
      suppose
A14:    P[y];
        then f.y = F(y) by A10,A12;
        hence thesis by A2,A11,A10,A12,A13,A14;
      end;
      suppose
A15:    Q[y];
        then f.y = G(y) by A10,A12;
        hence thesis by A3,A11,A10,A12,A13,A15;
      end;
    end;
    hence thesis;
  end;
  then reconsider f as PartFunc of X(),Y() by A11,A10,RELSET_1:4;
  take f;
  thus for x holds x in dom f iff x in X() & (P[x] or Q[x]) by A4,A10;
  let x;
  assume x in dom f;
  hence thesis by A10;
end;

scheme
  PartFuncExS3{X, Y()->set,P,Q,R[set], F,G,H(set)->set}: ex f being PartFunc
of X(),Y() st (for x holds x in dom f iff x in X() & (P[x] or Q[x] or R[x])) &
for x st x in dom f holds (P[x] implies f.x=F(x)) & (Q[x] implies f.x=G(x)) & (
  R[x] implies f.x=H(x))
provided
A1: for x st x in X() holds (P[x] implies not Q[x]) & (P[x] implies not
R[x]) & (Q[x] implies not R[x]) and
A2: for x st x in X() & P[x] holds F(x) in Y() and
A3: for x st x in X() & Q[x] holds G(x) in Y() and
A4: for x st x in X() & R[x] holds H(x) in Y()
proof
  defpred X[set,set] means (P[$1] implies $2 = F($1)) & (Q[$1] implies $2 = G(
  $1)) & (R[$1] implies $2 = H($1));
  defpred X[set] means P[$1] or Q[$1] or R[$1];
  consider S be set such that
A5: for x holds x in S iff x in X() & X[x] from XBOOLE_0:sch 1;
A6: for x st x in S ex y st X[x,y]
  proof
    let x;
    assume
A7: x in S;
    then
A8: x in X() by A5;
    now
      per cases by A5,A7;
      suppose
A9:     P[x];
        take y = F(x);
        ( not Q[x])& not R[x] by A1,A8,A9;
        hence thesis;
      end;
      suppose
A10:    Q[x];
        take y = G(x);
        ( not P[x])& not R[x] by A1,A8,A10;
        hence thesis;
      end;
      suppose
A11:    R[x];
        take y = H(x);
        ( not P[x])& not Q[x] by A1,A8,A11;
        hence thesis;
      end;
    end;
    hence thesis;
  end;
  consider f being Function such that
A12: dom f = S & for x st x in S holds X[x,f.x] from CLASSES1:sch 1(A6);
A13: S c= X()
  proof
    let x;
    assume x in S;
    hence thesis by A5;
  end;
  rng f c= Y()
  proof
    let x;
    assume x in rng f;
    then consider y such that
A14: y in dom f and
A15: x = f.y by FUNCT_1:def 3;
    now
      per cases by A5,A12,A14;
      suppose
A16:    P[y];
        then f.y = F(y) by A12,A14;
        hence thesis by A2,A13,A12,A14,A15,A16;
      end;
      suppose
A17:    Q[y];
        then f.y = G(y) by A12,A14;
        hence thesis by A3,A13,A12,A14,A15,A17;
      end;
      suppose
A18:    R[y];
        then f.y = H(y) by A12,A14;
        hence thesis by A4,A13,A12,A14,A15,A18;
      end;
    end;
    hence thesis;
  end;
  then reconsider f as PartFunc of X(),Y() by A13,A12,RELSET_1:4;
  take f;
  thus for x holds x in dom f iff x in X() & (P[x] or Q[x] or R[x]) by A5,A12;
  let x;
  assume x in dom f;
  hence thesis by A12;
end;

scheme
  PartFuncExS4{X, Y()->set,P,Q,R,S[set], F,G,H,I(set)->set}: ex f being
PartFunc of X(),Y() st (for x holds x in dom f iff x in X() & (P[x] or Q[x] or
  R[x] or S[x])) & for x st x in dom f holds (P[x] implies f.x=F(x)) & (Q[x]
  implies f.x=G(x)) & (R[x] implies f.x=H(x)) & (S[x] implies f.x=I(x))
provided
A1: for x st x in X() holds (P[x] implies not Q[x]) & (P[x] implies not
R[x]) & (P[x] implies not S[x]) & (Q[x] implies not R[x]) & (Q[x] implies not S
[x]) & (R[x] implies not S[x]) and
A2: for x st x in X() & P[x] holds F(x) in Y() and
A3: for x st x in X() & Q[x] holds G(x) in Y() and
A4: for x st x in X() & R[x] holds H(x) in Y() and
A5: for x st x in X() & S[x] holds I(x) in Y()
proof
  defpred X[set,set] means (P[$1] implies $2 = F($1)) & (Q[$1] implies $2 = G(
  $1)) & (R[$1] implies $2 = H($1)) & (S[$1] implies $2 = I($1));
  defpred X[set] means P[$1] or Q[$1] or R[$1] or S[$1];
  consider D be set such that
A6: for x holds x in D iff x in X() & X[x] from XBOOLE_0:sch 1;
A7: for x st x in D ex y st X[x,y]
  proof
    let x;
    assume
A8: x in D;
    then
A9: x in X() by A6;
    now
      per cases by A6,A8;
      suppose
A10:    P[x];
        take y = F(x);
A11:    not S[x] by A1,A9,A10;
        ( not Q[x])& not R[x] by A1,A9,A10;
        hence thesis by A11;
      end;
      suppose
A12:    Q[x];
        take y = G(x);
A13:    not S[x] by A1,A9,A12;
        ( not P[x])& not R[x] by A1,A9,A12;
        hence thesis by A13;
      end;
      suppose
A14:    R[x];
        take y = H(x);
A15:    not S[x] by A1,A9,A14;
        ( not P[x])& not Q[x] by A1,A9,A14;
        hence thesis by A15;
      end;
      suppose
A16:    S[x];
        take y = I(x);
A17:    not R[x] by A1,A9,A16;
        ( not P[x])& not Q[x] by A1,A9,A16;
        hence thesis by A17;
      end;
    end;
    hence thesis;
  end;
  consider f being Function such that
A18: dom f = D & for x st x in D holds X[x,f.x] from CLASSES1:sch 1(A7);
A19: D c= X()
  proof
    let x;
    assume x in D;
    hence thesis by A6;
  end;
  rng f c= Y()
  proof
    let x;
    assume x in rng f;
    then consider y such that
A20: y in dom f and
A21: x = f.y by FUNCT_1:def 3;
    now
      per cases by A6,A18,A20;
      suppose
A22:    P[y];
        then f.y = F(y) by A18,A20;
        hence thesis by A2,A19,A18,A20,A21,A22;
      end;
      suppose
A23:    Q[y];
        then f.y = G(y) by A18,A20;
        hence thesis by A3,A19,A18,A20,A21,A23;
      end;
      suppose
A24:    R[y];
        then f.y = H(y) by A18,A20;
        hence thesis by A4,A19,A18,A20,A21,A24;
      end;
      suppose
A25:    S[y];
        then f.y = I(y) by A18,A20;
        hence thesis by A5,A19,A18,A20,A21,A25;
      end;
    end;
    hence thesis;
  end;
  then reconsider f as PartFunc of X(),Y() by A19,A18,RELSET_1:4;
  take f;
  thus for x holds x in dom f iff x in X() & (P[x] or Q[x] or R[x] or S[x]) by
A6,A18;
  let x;
  assume x in dom f;
  hence thesis by A18;
end;

scheme
  PartFuncExCD2{C, D, E()->non empty set, P,Q[set,set], F,G(set,set)->Element
of E()}: ex f being PartFunc of [:C(),D():],E() st (for c be Element of C() ,d
be Element of D() holds [c,d] in dom f iff P[c,d] or Q[c,d]) & for c be Element
of C() ,d be Element of D() st [c,d] in dom f holds (P[c,d] implies f.[c,d]=F(c
  ,d)) & (Q[c,d] implies f.[c,d]=G(c,d))
provided
A1: for c be Element of C() ,d be Element of D() st P[c,d] holds not Q[c ,d]
proof
  defpred X[set,set] means for c be Element of C() ,t be Element of D() st $1
  = [c,t] holds (P[c,t] implies $2 = F(c,t)) & (Q[c,t] implies $2 = G(c,t));
  defpred X[set] means for c be Element of C() ,d be Element of D() st $1 = [c
  ,d] holds P[c,d] or Q[c,d];
  consider F be set such that
A2: for z holds z in F iff z in [:C(),D():] & X[z] from XBOOLE_0:sch 1;
A3: for x1 be set st x1 in F ex z st X[x1,z]
  proof
    let x1 be set;
    assume
A4: x1 in F;
    then x1 in [:C(),D():] by A2;
    then consider f9,g9 be set such that
A5: f9 in C() and
A6: g9 in D() and
A7: x1 = [f9,g9] by ZFMISC_1:def 2;
    reconsider g9 as Element of D() by A6;
    reconsider f9 as Element of C() by A5;
    now
      per cases by A2,A4,A7;
      suppose
A8:     P[f9,g9];
        take z = F(f9,g9);
        let p be Element of C() ,d be Element of D();
        assume x1 = [p,d];
        then f9 = p & g9 = d by A7,XTUPLE_0:1;
        hence (P[p,d] implies z = F(p,d)) & (Q[p,d] implies z = G(p,d)) by A1
,A8;
      end;
      suppose
A9:     Q[f9,g9];
        take z = G(f9,g9);
        let r be Element of C() ,d be Element of D();
        assume x1 = [r,d];
        then f9 = r & g9 = d by A7,XTUPLE_0:1;
        hence (P[r,d] implies z = F(r,d)) & (Q[r,d] implies z = G(r,d)) by A1
,A9;
      end;
    end;
    hence thesis;
  end;
  consider f being Function such that
A10: dom f = F & for z st z in F holds X[z,f.z] from CLASSES1:sch 1(A3);
A11: rng f c= E()
  proof
    let z;
    assume z in rng f;
    then consider x1 be set such that
A12: x1 in dom f and
A13: z = f.x1 by FUNCT_1:def 3;
    x1 in [:C(),D():] by A2,A10,A12;
    then consider x,y such that
A14: x in C() and
A15: y in D() and
A16: x1 = [x,y] by ZFMISC_1:def 2;
    reconsider y as Element of D() by A15;
    reconsider x as Element of C() by A14;
    now
      per cases by A2,A10,A12,A16;
      suppose
        P[x,y];
        then f.[x,y] = F(x,y) by A10,A12,A16;
        hence thesis by A13,A16;
      end;
      suppose
        Q[x,y];
        then f.[x,y] = G(x,y) by A10,A12,A16;
        hence thesis by A13,A16;
      end;
    end;
    hence thesis;
  end;
  F c= [:C(),D():]
  proof
    let z;
    assume z in F;
    hence thesis by A2;
  end;
  then reconsider f as PartFunc of [:C(),D():],E() by A10,A11,RELSET_1:4;
  take f;
  thus for c be Element of C() ,h be Element of D() holds [c,h] in dom f iff P
  [c,h] or Q[c,h]
  proof
    let c be Element of C() ,g be Element of D();
    thus [c,g] in dom f implies P[c,g] or Q[c,g] by A2,A10;
    assume
A17: P[c,g] or Q[c,g];
A18: now
      let h9 be Element of C() ,j9 be Element of D();
      assume
A19:  [c,g] = [h9, j9 ];
      then c = h9 by XTUPLE_0:1;
      hence P[h9,j9] or Q[h9,j9] by A17,A19,XTUPLE_0:1;
    end;
    [c,g] in [:C(),D():] by ZFMISC_1:87;
    hence thesis by A2,A10,A18;
  end;
  let c be Element of C() ,d be Element of D();
  assume [c,d] in dom f;
  hence thesis by A10;
end;

scheme
  PartFuncExCD3{C, D, E()->non empty set, P,Q,R[set,set], F,G,H(set,set)->
Element of E()}: ex f being PartFunc of [:C(),D():],E() st (for c be Element of
C() ,d be Element of D() holds [c,d] in dom f iff P[c,d] or Q[c,d] or R[c,d]) &
  for c be Element of C() ,r be Element of D() st [c,r] in dom f holds (P[c,r]
implies f.[c,r]=F(c,r)) & (Q[c,r] implies f.[c,r]=G(c,r)) & (R[c,r] implies f.[
  c,r]=H(c,r))
provided
A1: for c be Element of C() ,s be Element of D() holds (P[c,s] implies
not Q[c,s]) & (P[c,s] implies not R[c,s]) & (Q[c,s] implies not R[c,s])
proof
  defpred X[set,set] means for c be Element of C() ,t be Element of D() st $1
= [c,t] holds (P[c,t] implies $2 = F(c,t)) & (Q[c,t] implies $2 = G(c,t)) & (R[
  c,t] implies $2 = H(c,t));
  defpred X[set] means for c be Element of C() ,d be Element of D() st $1 = [c
  ,d] holds P[c,d] or Q[c,d] or R[c,d];
  consider T be set such that
A2: for z holds z in T iff z in [:C(),D():] & X[z] from XBOOLE_0:sch 1;
A3: for x1 be set st x1 in T ex z st X[x1,z]
  proof
    let x1 be set;
    assume
A4: x1 in T;
    then x1 in [:C(),D():] by A2;
    then consider q9,w9 be set such that
A5: q9 in C() and
A6: w9 in D() and
A7: x1 = [q9,w9] by ZFMISC_1:def 2;
    reconsider w9 as Element of D() by A6;
    reconsider q9 as Element of C() by A5;
    now
      per cases by A2,A4,A7;
      suppose
A8:     P[q9,w9];
        take z = F(q9,w9);
        let c be Element of C() ,d be Element of D();
        assume x1 = [c,d];
        then q9 = c & w9 = d by A7,XTUPLE_0:1;
        hence
        (P[c,d] implies z = F(c,d)) & (Q[c,d] implies z = G(c,d)) & (R[c,
        d] implies z = H(c,d)) by A1,A8;
      end;
      suppose
A9:     Q[q9,w9];
        take z = G(q9,w9);
        let c be Element of C() ,d be Element of D();
        assume x1 = [c,d];
        then q9 = c & w9 = d by A7,XTUPLE_0:1;
        hence
        (P[c,d] implies z = F(c,d)) & (Q[c,d] implies z = G(c,d)) & (R[c,
        d] implies z = H(c,d)) by A1,A9;
      end;
      suppose
A10:    R[q9,w9];
        take z = H(q9,w9);
        let c be Element of C() ,d be Element of D();
        assume x1 = [c,d];
        then q9 = c & w9 = d by A7,XTUPLE_0:1;
        hence
        (P[c,d] implies z = F(c,d)) & (Q[c,d] implies z = G(c,d)) & (R[c,
        d] implies z = H(c,d)) by A1,A10;
      end;
    end;
    hence thesis;
  end;
  consider f being Function such that
A11: dom f = T & for z st z in T holds X[z,f.z] from CLASSES1:sch 1(A3);
A12: rng f c= E()
  proof
    let z;
    assume z in rng f;
    then consider x1 be set such that
A13: x1 in dom f and
A14: z = f.x1 by FUNCT_1:def 3;
    x1 in [:C(),D():] by A2,A11,A13;
    then consider x,y such that
A15: x in C() and
A16: y in D() and
A17: x1 = [x,y] by ZFMISC_1:def 2;
    reconsider y as Element of D() by A16;
    reconsider x as Element of C() by A15;
    now
      per cases by A2,A11,A13,A17;
      suppose
        P[x,y];
        then f.[x,y] = F(x,y) by A11,A13,A17;
        hence thesis by A14,A17;
      end;
      suppose
        Q[x,y];
        then f.[x,y] = G(x,y) by A11,A13,A17;
        hence thesis by A14,A17;
      end;
      suppose
        R[x,y];
        then f.[x,y] = H(x,y) by A11,A13,A17;
        hence thesis by A14,A17;
      end;
    end;
    hence thesis;
  end;
  T c= [:C(),D():]
  proof
    let z;
    assume z in T;
    hence thesis by A2;
  end;
  then reconsider f as PartFunc of [:C(),D():],E() by A11,A12,RELSET_1:4;
  take f;
  thus for c be Element of C() ,d be Element of D() holds [c,d] in dom f iff P
  [c,d] or Q[c,d] or R[c,d]
  proof
    let c be Element of C() ,d be Element of D();
    thus [c,d] in dom f implies P[c,d] or Q[c,d] or R[c,d] by A2,A11;
    assume
A18: P[c,d] or Q[c,d] or R[c,d];
A19: now
      let i9 be Element of C() ,o9 be Element of D();
      assume
A20:  [c,d] = [i9, o9 ];
      then c = i9 by XTUPLE_0:1;
      hence P[i9,o9] or Q[i9,o9] or R[i9,o9] by A18,A20,XTUPLE_0:1;
    end;
    [c,d] in [:C(),D():] by ZFMISC_1:87;
    hence thesis by A2,A11,A19;
  end;
  let c be Element of C() ,d be Element of D();
  assume [c,d] in dom f;
  hence thesis by A11;
end;

scheme
  PartFuncExCS2{X, Y, Z()->set,P,Q[set,set], F,G(set,set)->set}: ex f being
  PartFunc of [:X(),Y():],Z() st (for x,y holds [x,y] in dom f iff x in X() & y
in Y() & (P[x,y] or Q[x,y])) & for x,y st [x,y] in dom f holds (P[x,y] implies
  f.[x,y]=F(x,y)) & (Q[x,y] implies f.[x,y]=G(x,y))
provided
A1: for x,y st x in X() & y in Y() holds P[x,y] implies not Q[x,y] and
A2: for x,y st x in X() & y in Y() & P[x,y] holds F(x,y) in Z() and
A3: for x,y st x in X() & y in Y() & Q[x,y] holds G(x,y) in Z()
proof
  defpred X[set,set] means for x,y st $1 = [x,y] holds (P[x,y] implies $2 = F(
  x,y)) & (Q[x,y] implies $2 = G(x,y));
  defpred X[set] means for x,y st $1 = [x,y] holds P[x,y] or Q[x,y];
  consider K be set such that
A4: for z holds z in K iff z in [:X(),Y():] & X[z] from XBOOLE_0:sch 1;
A5: for x1 be set st x1 in K ex z st X[x1,z]
  proof
    let x1 be set;
    assume
A6: x1 in K;
    then x1 in [:X(),Y():] by A4;
    then consider n9,m9 be set such that
A7: n9 in X() & m9 in Y() and
A8: x1 = [n9,m9] by ZFMISC_1:def 2;
    now
      per cases by A4,A6,A8;
      suppose
A9:     P[n9,m9];
        take z = F(n9,m9);
        let x,y;
        assume x1 = [x,y];
        then n9 = x & m9 = y by A8,XTUPLE_0:1;
        hence (P[x,y] implies z = F(x,y)) & (Q[x,y] implies z = G(x,y)) by A1
,A7,A9;
      end;
      suppose
A10:    Q[n9,m9];
        take z = G(n9,m9);
        let x,y;
        assume x1 = [x,y];
        then n9 = x & m9 = y by A8,XTUPLE_0:1;
        hence (P[x,y] implies z = F(x,y)) & (Q[x,y] implies z = G(x,y)) by A1
,A7,A10;
      end;
    end;
    hence thesis;
  end;
  consider f being Function such that
A11: dom f = K & for z st z in K holds X[z,f.z] from CLASSES1:sch 1(A5);
A12: rng f c= Z()
  proof
    let z;
    assume z in rng f;
    then consider x1 be set such that
A13: x1 in dom f and
A14: z = f.x1 by FUNCT_1:def 3;
    x1 in [:X(),Y():] by A4,A11,A13;
    then consider x,y such that
A15: x in X() & y in Y() and
A16: x1 = [x,y] by ZFMISC_1:def 2;
    now
      per cases by A4,A11,A13,A16;
      suppose
A17:    P[x,y];
        then f.[x,y] = F(x,y) by A11,A13,A16;
        hence thesis by A2,A14,A15,A16,A17;
      end;
      suppose
A18:    Q[x,y];
        then f.[x,y] = G(x,y) by A11,A13,A16;
        hence thesis by A3,A14,A15,A16,A18;
      end;
    end;
    hence thesis;
  end;
  K c= [:X(),Y():]
  proof
    let z;
    assume z in K;
    hence thesis by A4;
  end;
  then reconsider f as PartFunc of [:X(),Y():],Z() by A11,A12,RELSET_1:4;
  take f;
  thus for x,y holds [x,y] in dom f iff x in X() & y in Y() & (P[x,y] or Q[x,y
  ] )
  proof
    let x,y;
    thus [x,y] in dom f implies x in X() & y in Y() & (P[x,y] or Q[x,y]) by A4
,A11,ZFMISC_1:87;
    assume that
A19: x in X() & y in Y() and
A20: P[x,y] or Q[x,y];
A21: now
      let z9,q9 be set;
      assume
A22:  [x,y] = [z9,q9];
      then x = z9 by XTUPLE_0:1;
      hence P[z9,q9] or Q[z9,q9] by A20,A22,XTUPLE_0:1;
    end;
    [x,y] in [:X(),Y():] by A19,ZFMISC_1:87;
    hence thesis by A4,A11,A21;
  end;
  let x,y;
  assume [x,y] in dom f;
  hence thesis by A11;
end;

scheme
  PartFuncExCS3{X, Y, Z()->set, P,Q,R[set,set], F,G,H(set,set)->set}: ex f
being PartFunc of [:X(),Y():],Z() st (for x,y holds [x,y] in dom f iff x in X()
& y in Y() & (P[x,y] or Q[x,y] or R[x,y])) & for x,y st [x,y] in dom f holds (P
  [x,y] implies f.[x,y]=F(x,y)) & (Q[x,y] implies f.[x,y]=G(x,y)) & (R[x,y]
  implies f.[x,y]=H(x,y))
provided
A1: for x,y st x in X() & y in Y() holds (P[x,y] implies not Q[x,y]) & (
P[x,y] implies not R[x,y]) & (Q[x,y] implies not R[x,y]) and
A2: for x,y st x in X() & y in Y() holds P[x,y] implies F(x,y) in Z() and
A3: for x,y st x in X() & y in Y() holds Q[x,y] implies G(x,y) in Z() and
A4: for x,y st x in X() & y in Y() holds R[x,y] implies H(x,y) in Z()
proof
  defpred X[set,set] means for x,y st $1 = [x,y] holds (P[x,y] implies $2 = F(
  x,y)) & (Q[x,y] implies $2 = G(x,y)) & (R[x,y] implies $2 = H(x,y));
  defpred X[set] means for x,y st $1 = [x,y] holds P[x,y] or Q[x,y] or R[x,y];
  consider L be set such that
A5: for z holds z in L iff z in [:X(),Y():] & X[z] from XBOOLE_0:sch 1;
A6: for x1 be set st x1 in L ex z st X[x1,z]
  proof
    let x1 be set;
    assume
A7: x1 in L;
    then x1 in [:X(),Y():] by A5;
    then consider z9,a9 be set such that
A8: z9 in X() & a9 in Y() and
A9: x1 = [z9,a9] by ZFMISC_1:def 2;
    now
      per cases by A5,A7,A9;
      suppose
A10:    P[z9,a9];
        take z = F(z9,a9);
        let x,y;
        assume x1 = [x,y];
        then z9 = x & a9 = y by A9,XTUPLE_0:1;
        hence
        (P[x,y] implies z = F(x,y)) & (Q[x,y] implies z = G(x,y)) & (R[x,
        y] implies z = H(x,y)) by A1,A8,A10;
      end;
      suppose
A11:    Q[z9,a9];
        take z = G(z9,a9);
        let x,y;
        assume x1 = [x,y];
        then z9 = x & a9 = y by A9,XTUPLE_0:1;
        hence
        (P[x,y] implies z = F(x,y)) & (Q[x,y] implies z = G(x,y)) & (R[x,
        y] implies z = H(x,y)) by A1,A8,A11;
      end;
      suppose
A12:    R[z9,a9];
        take z=H(z9,a9);
        let x,y;
        assume x1 = [x,y];
        then z9 = x & a9 = y by A9,XTUPLE_0:1;
        hence
        (P[x,y] implies z = F(x,y)) & (Q[x,y] implies z = G(x,y)) & (R[x,
        y] implies z = H(x,y)) by A1,A8,A12;
      end;
    end;
    hence thesis;
  end;
  consider f being Function such that
A13: dom f = L & for z st z in L holds X[z,f.z] from CLASSES1:sch 1(A6);
A14: rng f c= Z()
  proof
    let z;
    assume z in rng f;
    then consider x1 be set such that
A15: x1 in dom f and
A16: z = f.x1 by FUNCT_1:def 3;
    x1 in [:X(),Y():] by A5,A13,A15;
    then consider x,y such that
A17: x in X() & y in Y() and
A18: x1 = [x,y] by ZFMISC_1:def 2;
    now
      per cases by A5,A13,A15,A18;
      suppose
A19:    P[x,y];
        then f.[x,y] = F(x,y) by A13,A15,A18;
        hence thesis by A2,A16,A17,A18,A19;
      end;
      suppose
A20:    Q[x,y];
        then f.[x,y] = G(x,y) by A13,A15,A18;
        hence thesis by A3,A16,A17,A18,A20;
      end;
      suppose
A21:    R[x,y];
        then f.[x,y] = H(x,y) by A13,A15,A18;
        hence thesis by A4,A16,A17,A18,A21;
      end;
    end;
    hence thesis;
  end;
  L c= [:X(),Y():]
  proof
    let z;
    assume z in L;
    hence thesis by A5;
  end;
  then reconsider f as PartFunc of [:X(),Y():],Z() by A13,A14,RELSET_1:4;
  take f;
  thus for x,y holds [x,y] in dom f iff x in X() & y in Y() & (P[x,y] or Q[x,y
  ] or R[x,y])
  proof
    let x,y;
    thus [x,y] in dom f implies x in X() & y in Y() & (P[x,y] or Q[x,y] or R[x
    ,y]) by A5,A13,ZFMISC_1:87;
    assume that
A22: x in X() & y in Y() and
A23: P[x,y] or Q[x,y] or R[x,y];
A24: now
      let f9,r9 be set;
      assume
A25:  [x,y]=[f9,r9];
      then x = f9 by XTUPLE_0:1;
      hence P[f9,r9] or Q[f9,r9] or R[f9,r9] by A23,A25,XTUPLE_0:1;
    end;
    [x,y] in [:X(),Y():] by A22,ZFMISC_1:87;
    hence thesis by A5,A13,A24;
  end;
  let x,y;
  assume [x,y] in dom f;
  hence thesis by A13;
end;

scheme
  ExFuncD3{C, D()->non empty set,P,Q,R[set], F,G,H(set)->Element of D()}: ex f
being Function of C(),D() st for c be Element of C() holds (P[c] implies f.c =
  F(c)) & (Q[c] implies f.c = G(c)) & (R[c] implies f.c = H(c))
provided
A1: for c be Element of C() holds (P[c] implies not Q[c]) & (P[c]
implies not R[c]) & (Q[c] implies not R[c]) and
A2: for c be Element of C() holds P[c] or Q[c] or R[c]
proof
A3: for c be Element of C() holds (P[c] implies not Q[c]) & (P[c] implies
  not R[c]) & (Q[c] implies not R[c]) by A1;
  consider f being PartFunc of C(),D() such that
A4: for w be Element of C() holds w in dom f iff P[w] or Q[w] or R[w] and
A5: for q be Element of C() st q in dom f holds (P[q] implies f.q = F(q)
) & (Q[q] implies f.q = G(q)) & (R[q] implies f.q = H(q)) from PartFuncExD3(A3
  );
  set q = f;
A6: dom q = C()
  proof
    thus dom q c= C();
    let x;
    assume x in C();
    then reconsider t9 = x as Element of C();
    P[t9] or Q[t9] or R[t9] by A2;
    hence thesis by A4;
  end;
  then reconsider q as Function of C(),D() by FUNCT_2:def 1;
  take q;
  let t be Element of C();
  thus thesis by A5,A6;
end;

scheme
  ExFuncD4{C, D()->non empty set, P,Q,R,S[set], F,G,H,I(set)->Element of D()}:
ex f being Function of C(),D() st for c be Element of C() holds (P[c] implies f
  .c = F(c)) & (Q[c] implies f.c = G(c)) & (R[c] implies f.c = H(c)) & (S[c]
  implies f.c = I(c))
provided
A1: for c be Element of C() holds (P[c] implies not Q[c]) & (P[c]
implies not R[c]) & (P[c] implies not S[c]) & (Q[c] implies not R[c]) & (Q[c]
implies not S[c]) & (R[c] implies not S[c]) and
A2: for c be Element of C() holds P[c] or Q[c] or R[c] or S[c]
proof
A3: for c be Element of C() holds (P[c] implies not Q[c]) & (P[c] implies
  not R[c]) & (P[c] implies not S[c]) & (Q[c] implies not R[c]) & (Q[c] implies
  not S[c]) & (R[c] implies not S[c]) by A1;
  consider f being PartFunc of C(),D() such that
A4: for r be Element of C() holds r in dom f iff P[r] or Q[r] or R[r] or
  S[r] and
A5: for o be Element of C() st o in dom f holds (P[o] implies f.o = F(o)
) & (Q[o] implies f.o = G(o)) & (R[o] implies f.o = H(o)) & (S[o] implies f.o =
  I(o)) from PartFuncExD4(A3);
  set q=f;
A6: dom q = C()
  proof
    thus dom q c= C();
    let x;
    assume x in C();
    then reconsider w9 = x as Element of C();
    P[w9] or Q[w9] or R[w9] or S[w9] by A2;
    hence thesis by A4;
  end;
  then reconsider q as Function of C(),D() by FUNCT_2:def 1;
  take q;
  let e be Element of C();
  thus thesis by A5,A6;
end;

scheme
  FuncExCD2{C, D, E()->non empty set,P[set,set], F,G(set,set)->Element of E()}
  : ex f being Function of [:C(),D():],E() st for c be Element of C() ,d be
Element of D() st [c,d] in dom f holds (P[c,d] implies f.[c,d]=F(c,d)) & (not P
  [c,d] implies f.[c,d]=G(c,d)) proof
  defpred Y[set,set] means not P[$1,$2];
A1: for c be Element of C() ,f being Element of D() st P[c,f] holds not Y[c,
  f];
  consider f being PartFunc of [:C(),D():],E() such that
A2: (for c be Element of C() ,e be Element of D() holds [c,e] in dom f
iff P[c,e] or Y[c,e]) & for c be Element of C() ,g being Element of D() st [c,g
] in dom f holds (P[c,g] implies f.[c,g] = F(c,g)) & (Y[c,g] implies f.[c,g] =
  G(c,g)) from PartFuncExCD2(A1);
  consider g be Function such that
A3: g=f;
  dom f = [:C(),D():]
  proof
    thus dom f c= [:C(),D():];
    let x;
    assume x in [:C(),D():];
    then consider y,z such that
A4: y in C() and
A5: z in D() and
A6: x = [y,z] by ZFMISC_1:def 2;
    reconsider z as Element of D() by A5;
    reconsider y as Element of C() by A4;
    P[y,z] or not P[y,z];
    hence thesis by A2,A6;
  end;
  then reconsider g as Function of [:C(),D():],E() by A3,FUNCT_2:def 1;
  take g;
  thus thesis by A2,A3;
end;

scheme
  FuncExCD3{C, D, E()->non empty set, P,Q,R[set,set], F,G,H(set,set)->Element
of E()}: ex f being Function of [:C(),D():],E() st (for c be Element of C() ,d
be Element of D() holds [c,d] in dom f iff P[c,d] or Q[c,d] or R[c,d]) & for c
be Element of C() ,d be Element of D() st [c,d] in dom f holds (P[c,d] implies
f.[c,d]=F(c,d)) & (Q[c,d] implies f.[c,d]=G(c,d)) & (R[c,d] implies f.[c,d]=H(c
  ,d))
provided
A1: for c be Element of C() ,d be Element of D() holds (P[c,d] implies
not Q[c,d]) & (P[c,d] implies not R[c,d]) & (Q[c,d] implies not R[c,d]) and
A2: for c be Element of C() ,d be Element of D() holds P[c,d] or Q[c,d]
or R[c,d]
proof
A3: for c be Element of C() ,d be Element of D() holds (P[c,d] implies not Q
  [c,d]) & (P[c,d] implies not R[c,d]) & (Q[c,d] implies not R[c,d]) by A1;
  consider f being PartFunc of [:C(),D():],E() such that
A4: (for c be Element of C() ,b be Element of D() holds [c,b] in dom f
iff P[c,b] or Q[c,b] or R[c,b]) & for a being Element of C() ,b be Element of D
() st [a,b] in dom f holds (P[a,b] implies f.[a,b] = F(a,b)) & (Q[a,b] implies
  f.[a,b] = G(a,b)) & (R[a,b] implies f.[a,b] = H(a,b)) from PartFuncExCD3(A3);
  consider v be Function such that
A5: v = f;
  dom f = [:C(),D():]
  proof
    thus dom f c= [:C(),D():];
    let x;
    assume x in [:C(),D():];
    then consider y,z such that
A6: y in C() and
A7: z in D() and
A8: x = [y,z] by ZFMISC_1:def 2;
    reconsider z as Element of D() by A7;
    reconsider y as Element of C() by A6;
    P[y,z] or Q[y,z] or R[y,z] by A2;
    hence thesis by A4,A8;
  end;
  then reconsider v as Function of [:C(),D():],E() by A5,FUNCT_2:def 1;
  take v;
  thus thesis by A4,A5;
end;