scheme1.miz



    begin

    reserve x,y,z for object;

    reserve n,m,k for Element of NAT ;

    reserve r for Real;

    theorem :: SCHEME1:1

    for n be Nat holds ex m st n = (2 * m) or n = ((2 * m) + 1)

    proof

      let n be Nat;

      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 :: SCHEME1:2

    

     Th2: for n holds 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 :: SCHEME1:3

    

     Th3: for n holds 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 :: SCHEME1:4

    

     Th4: for n holds 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 :: SCHEME1:sch1

    ExRealSubseq { s() -> Real_Sequence , P[ object] } :

ex q be Real_Sequence st q is subsequence of s() & (for n be Nat holds P[(q . n)]) & for n st (for r st r = (s() . n) holds P[r]) holds ex m st (s() . n) = (q . m)

      provided

       A1: for n holds ex m st n <= m & P[(s() . m)];

      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 be Nat holds for x be Element of NAT holds ex y be Element of NAT st X[n, x, y]

      proof

        let n be Nat;

        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 sequence of NAT such that

       A9: (F . 0 ) = M9 & for n be 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, NUMBERS: 19;

      then

      reconsider F as natural-valued Real_Sequence by FUNCT_2:def 1, RELSET_1: 4;

      for n be Nat 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)] holds 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 be Nat st X[k] holds X[(k + 1)]

      proof

        let k be Nat 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 be Nat holds X[n] from NAT_1:sch 2( 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 :: SCHEME1:sch2

    ExRealSeq2 { F,G( set) -> Element of REAL } :

ex s be Real_Sequence st for n holds (s . (2 * n)) = F(n) & (s . ((2 * n) + 1)) = G(n);

      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 in M implies $2 = G(/));

      

       A3: for n holds ex r be Element of REAL st X[n, r]

      proof

        let n;

        now

          assume

           A4: n in N;

          reconsider r = F(/) as Element of REAL ;

          take r;

          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 be sequence of 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(/) by A7

      .= F(n);

      ((2 * n) + 1) in M by A2;

      

      hence (f . ((2 * n) + 1)) = G(/) by A7

      .= G(n);

    end;

    scheme :: SCHEME1:sch3

    ExRealSeq3 { F,G,H( set) -> Element of REAL } :

ex s be Real_Sequence st for n holds (s . (3 * n)) = F(n) & (s . ((3 * n) + 1)) = G(n) & (s . ((3 * n) + 2)) = H(n);

      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 in G implies $2 = G(/)) & ($1 in K implies $2 = H(/));

      

       A4: for n holds ex r be Element of REAL 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(/);

            

             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(/);

             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(/);

             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 be sequence of 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(/) by A15

      .= F(n);

      ((3 * n) + 1) in G by A2;

      

      hence (f . ((3 * n) + 1)) = G(/) by A15

      .= G(n);

      ((3 * n) + 2) in K by A3;

      

      hence (f . ((3 * n) + 2)) = H(/) by A15

      .= H(n);

    end;

    scheme :: SCHEME1:sch4

    ExRealSeq4 { F,G,H,I( set) -> Element of REAL } :

ex s be 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);

      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 in R implies $2 = G(/)) & ($1 in P implies $2 = H(/)) & ($1 in L implies $2 = I(/));

      

       A5: for n holds ex r be Element of REAL 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(/);

            

             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(/);

             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(/);

             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(/);

             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 be sequence of 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(/) by A23

      .= F(n);

      ((4 * n) + 1) in R by A2;

      

      hence (f . ((4 * n) + 1)) = G(/) by A23

      .= G(n);

      ((4 * n) + 2) in P by A3;

      

      hence (f . ((4 * n) + 2)) = H(/) by A23

      .= H(n);

      ((4 * n) + 3) in L by A4;

      

      hence (f . ((4 * n) + 3)) = I(/) by A23

      .= I(n);

    end;

    scheme :: SCHEME1:sch5

    ExRealSeq5 { F,G,H,I,J( set) -> Element of REAL } :

ex s be 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);

      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 in M implies $2 = G(/)) & ($1 in K implies $2 = H(/)) & ($1 in L implies $2 = I(/)) & ($1 in O implies $2 = J(/));

      

       A6: for n holds ex r be Element of REAL 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(/);

            

             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(/);

             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(/);

             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(/);

             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(/);

             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 be sequence of 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(/) by A33

      .= F(n);

      ((5 * n) + 1) in M by A2;

      

      hence (f . ((5 * n) + 1)) = G(/) by A33

      .= G(n);

      ((5 * n) + 2) in K by A3;

      

      hence (f . ((5 * n) + 2)) = H(/) by A33

      .= H(n);

      ((5 * n) + 3) in L by A4;

      

      hence (f . ((5 * n) + 3)) = I(/) by A33

      .= I(n);

      ((5 * n) + 4) in O by A5;

      

      hence (f . ((5 * n) + 4)) = J(/) by A33

      .= J(n);

    end;

    scheme :: SCHEME1:sch6

    PartFuncExD2 { C,D() -> non empty set , P,Q[ object], F,G( object) -> Element of D() } :

ex f be 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];

      defpred X[ object, object] means (P[$1] implies $2 = F($1)) & (Q[$1] implies $2 = G($1));

      defpred X[ object] means P[$1] or Q[$1];

      consider X be set such that

       A2: for x be object holds x in X iff x in C() & X[x] from XBOOLE_0:sch 1;

      

       A3: for x be object st x in X holds ex y be object st X[x, y]

      proof

        let x be object;

        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 be Function such that

       A7: ( dom f) = X & for x be object st x in X holds X[x, (f . x)] from CLASSES1:sch 1( A3);

      

       A8: X c= C() by A2;

      ( rng f) c= D()

      proof

        let x be object;

        assume x in ( rng f);

        then

        consider y be object 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 :: SCHEME1:sch7

    PartFuncExD29 { C,D() -> non empty set , P,Q[ object], F,G( object) -> Element of D() } :

ex f be 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);

      defpred X[ object, object] means (P[$1] implies $2 = F($1)) & (Q[$1] implies $2 = G($1));

      defpred X[ object] means P[$1] or Q[$1];

      consider Y be set such that

       A2: for x be object holds x in Y iff x in C() & X[x] from XBOOLE_0:sch 1;

      

       A3: for x be object st x in Y holds ex y be object st X[x, y]

      proof

        let x be object;

        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 be Function such that

       A7: ( dom f) = Y & for x be object st x in Y holds X[x, (f . x)] from CLASSES1:sch 1( A3);

      

       A8: Y c= C() by A2;

      ( rng f) c= D()

      proof

        let x be object;

        assume x in ( rng f);

        then

        consider y be object 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 :: SCHEME1:sch8

    PartFuncExD299 { C,D() -> non empty set , P[ set], F,G( set) -> Element of D() } :

ex f be 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));

      defpred Y[ set] means not P[$1];

      

       A1: for c be Element of C() st P[c] holds not Y[c];

      consider f be 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 be object;

        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 :: SCHEME1:sch9

    PartFuncExD3 { C,D() -> non empty set , P,Q,R[ object], F,G,H( object) -> Element of D() } :

ex f be 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]);

      defpred X[ object, object] means (P[$1] implies $2 = F($1)) & (Q[$1] implies $2 = G($1)) & (R[$1] implies $2 = H($1));

      defpred X[ object] means P[$1] or Q[$1] or R[$1];

      consider Z be set such that

       A2: for x be object holds x in Z iff x in C() & X[x] from XBOOLE_0:sch 1;

      

       A3: for x be object st x in Z holds ex y be object st X[x, y]

      proof

        let x be object;

        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 be Function such that

       A8: ( dom f) = Z & for x be object st x in Z holds X[x, (f . x)] from CLASSES1:sch 1( A3);

      

       A9: ( rng f) c= D()

      proof

        let x be object;

        assume x in ( rng f);

        then

        consider y be object 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() by A2;

      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 :: SCHEME1:sch10

    PartFuncExD39 { C,D() -> non empty set , P,Q,R[ object], F,G,H( object) -> Element of D() } :

ex f be 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));

      defpred X[ object, object] means (P[$1] implies $2 = F($1)) & (Q[$1] implies $2 = G($1)) & (R[$1] implies $2 = H($1));

      defpred X[ object] means P[$1] or Q[$1] or R[$1];

      consider V be set such that

       A2: for x be object holds x in V iff x in C() & X[x] from XBOOLE_0:sch 1;

      

       A3: for x be object st x in V holds ex y be object st X[x, y]

      proof

        let x be object;

        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 be Function such that

       A15: ( dom f) = V & for x be object st x in V holds X[x, (f . x)] from CLASSES1:sch 1( A3);

      

       A16: ( rng f) c= D()

      proof

        let x be object;

        assume x in ( rng f);

        then

        consider y be object 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() by A2;

      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 :: SCHEME1:sch11

    PartFuncExD4 { C,D() -> non empty set , P,Q,R,S[ object], F,G,H,I( object) -> Element of D() } :

ex f be 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]);

      defpred X[ object, object] 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[ object] means P[$1] or Q[$1] or R[$1] or S[$1];

      consider B be set such that

       A2: for x be object holds x in B iff x in C() & X[x] from XBOOLE_0:sch 1;

      

       A3: for x be object st x in B holds ex y be object st X[x, y]

      proof

        let x be object;

        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 be Function such that

       A13: ( dom f) = B & for y be object st y in B holds X[y, (f . y)] from CLASSES1:sch 1( A3);

      

       A14: ( rng f) c= D()

      proof

        let x be object;

        assume x in ( rng f);

        then

        consider y be object 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() by A2;

      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 :: SCHEME1:sch12

    PartFuncExS2 { X,Y() -> set , P,Q[ object], F,G( object) -> set } :

ex f be 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();

      defpred X[ object, object] means (P[$1] implies $2 = F($1)) & (Q[$1] implies $2 = G($1));

      defpred X[ object] means P[$1] or Q[$1];

      consider A be set such that

       A4: for x be object holds x in A iff x in X() & X[x] from XBOOLE_0:sch 1;

      

       A5: for x be object st x in A holds ex y be object st X[x, y]

      proof

        let x be object;

        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 be Function such that

       A10: ( dom f) = A & for x be object st x in A holds X[x, (f . x)] from CLASSES1:sch 1( A5);

      

       A11: A c= X() by A4;

      ( rng f) c= Y()

      proof

        let x be object;

        assume x in ( rng f);

        then

        consider y be object 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 :: SCHEME1:sch13

    PartFuncExS3 { X,Y() -> set , P,Q,R[ object], F,G,H( object) -> set } :

ex f be 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();

      defpred X[ object, object] means (P[$1] implies $2 = F($1)) & (Q[$1] implies $2 = G($1)) & (R[$1] implies $2 = H($1));

      defpred X[ object] means P[$1] or Q[$1] or R[$1];

      consider S be set such that

       A5: for x be object holds x in S iff x in X() & X[x] from XBOOLE_0:sch 1;

      

       A6: for x be object st x in S holds ex y be object st X[x, y]

      proof

        let x be object;

        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 be Function such that

       A12: ( dom f) = S & for x be object st x in S holds X[x, (f . x)] from CLASSES1:sch 1( A6);

      

       A13: S c= X() by A5;

      ( rng f) c= Y()

      proof

        let x be object;

        assume x in ( rng f);

        then

        consider y be object 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 :: SCHEME1:sch14

    PartFuncExS4 { X,Y() -> set , P,Q,R,S[ object], F,G,H,I( object) -> set } :

ex f be 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();

      defpred X[ object, object] 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[ object] means P[$1] or Q[$1] or R[$1] or S[$1];

      consider D be set such that

       A6: for x be object holds x in D iff x in X() & X[x] from XBOOLE_0:sch 1;

      

       A7: for x be object st x in D holds ex y be object st X[x, y]

      proof

        let x be object;

        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 be Function such that

       A18: ( dom f) = D & for x be object st x in D holds X[x, (f . x)] from CLASSES1:sch 1( A7);

      

       A19: D c= X() by A6;

      ( rng f) c= Y()

      proof

        let x be object;

        assume x in ( rng f);

        then

        consider y be object 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 :: SCHEME1:sch15

    PartFuncExCD2 { C,D,E() -> non empty set , P,Q[ set, set], F,G( set, set) -> Element of E() } :

ex f be 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];

      defpred X[ object, object] 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[ object] 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 be object holds z in F iff z in [:C(), D():] & X[z] from XBOOLE_0:sch 1;

      

       A3: for x1 be object st x1 in F holds ex z be object st X[x1, z]

      proof

        let x1 be object;

        assume

         A4: x1 in F;

        then x1 in [:C(), D():] by A2;

        then

        consider f9,g9 be object 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 be Function such that

       A10: ( dom f) = F & for z be object st z in F holds X[z, (f . z)] from CLASSES1:sch 1( A3);

      

       A11: ( rng f) c= E()

      proof

        let z be object;

        assume z in ( rng f);

        then

        consider x1 be object 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 be object 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():] by A2;

      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 :: SCHEME1:sch16

    PartFuncExCD3 { C,D,E() -> non empty set , P,Q,R[ set, set], F,G,H( set, set) -> Element of E() } :

ex f be 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]);

      defpred X[ object, object] 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[ object] 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 be object holds z in T iff z in [:C(), D():] & X[z] from XBOOLE_0:sch 1;

      

       A3: for x1 be object st x1 in T holds ex z be object st X[x1, z]

      proof

        let x1 be object;

        assume

         A4: x1 in T;

        then x1 in [:C(), D():] by A2;

        then

        consider q9,w9 be object 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 be Function such that

       A11: ( dom f) = T & for z be object st z in T holds X[z, (f . z)] from CLASSES1:sch 1( A3);

      

       A12: ( rng f) c= E()

      proof

        let z be object;

        assume z in ( rng f);

        then

        consider x1 be object 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 be object 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():] by A2;

      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 :: SCHEME1:sch17

    PartFuncExCS2 { X,Y,Z() -> set , P,Q[ object, object], F,G( object, object) -> object } :

ex f be 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();

      defpred X[ object, object] 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[ object] 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 be object holds z in K iff z in [:X(), Y():] & X[z] from XBOOLE_0:sch 1;

      

       A5: for x1 be object st x1 in K holds ex z be object st X[x1, z]

      proof

        let x1 be object;

        assume

         A6: x1 in K;

        then x1 in [:X(), Y():] by A4;

        then

        consider n9,m9 be object 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 be Function such that

       A11: ( dom f) = K & for z be object st z in K holds X[z, (f . z)] from CLASSES1:sch 1( A5);

      

       A12: ( rng f) c= Z()

      proof

        let z be object;

        assume z in ( rng f);

        then

        consider x1 be object 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 be object 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():] by A4;

      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 object;

          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 :: SCHEME1:sch18

    PartFuncExCS3 { X,Y,Z() -> set , P,Q,R[ object, object], F,G,H( object, object) -> object } :

ex f be 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();

      defpred X[ object, object] 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[ object] 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 be object holds z in L iff z in [:X(), Y():] & X[z] from XBOOLE_0:sch 1;

      

       A6: for x1 be object st x1 in L holds ex z be object st X[x1, z]

      proof

        let x1 be object;

        assume

         A7: x1 in L;

        then x1 in [:X(), Y():] by A5;

        then

        consider z9,a9 be object 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 be Function such that

       A13: ( dom f) = L & for z be object st z in L holds X[z, (f . z)] from CLASSES1:sch 1( A6);

      

       A14: ( rng f) c= Z()

      proof

        let z be object;

        assume z in ( rng f);

        then

        consider x1 be object 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 be object 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():] by A5;

      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 object;

          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 :: SCHEME1:sch19

    ExFuncD3 { C,D() -> non empty set , P,Q,R[ set], F,G,H( set) -> Element of D() } :

ex f be 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];

      

       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 be 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 be object;

        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 :: SCHEME1:sch20

    ExFuncD4 { C,D() -> non empty set , P,Q,R,S[ set], F,G,H,I( set) -> Element of D() } :

ex f be 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];

      

       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 be 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 be object;

        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 :: SCHEME1:sch21

    FuncExCD2 { C,D,E() -> non empty set , P[ set, set], F,G( set, set) -> Element of E() } :

ex f be 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));

      defpred Y[ set, set] means not P[$1, $2];

      

       A1: for c be Element of C(), f be Element of D() st P[c, f] holds not Y[c, f];

      consider f be 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 be 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 be object;

        assume x in [:C(), D():];

        then

        consider y,z be object 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 :: SCHEME1:sch22

    FuncExCD3 { C,D,E() -> non empty set , P,Q,R[ set, set], F,G,H( set, set) -> Element of E() } :

ex f be 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];

      

       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 be 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 be 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 be object;

        assume x in [:C(), D():];

        then

        consider y,z be object 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;