:: Schemes of Existence of some Types of Functions
:: by Jaros{\l}aw Kotowicz
::
:: Received September 21, 1990
:: Copyright (c) 1990-2026 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, ORDINAL1, NUMBERS, XCMPLX_0,
XREAL_0, 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, SEQM_3, RECDEF_1, MEMBERED,
RELSET_1, NUMBERS;
registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, SEQM_3,
VALUED_0;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions TARSKI, XBOOLE_0;
equalities XBOOLE_0;
expansions TARSKI;
theorems ZFMISC_1, NAT_1, FUNCT_1, FUNCT_2, SEQM_3, PARTFUN1, RELSET_1, NAT_D,
ORDINAL1, XXREAL_0, XTUPLE_0, NUMBERS;
schemes NAT_1, FUNCT_2, RECDEF_1, SUBSET_1, CLASSES1, XBOOLE_0;
begin
reserve x,y,z for object;
reserve n,m,k for Element of NAT;
reserve r for Real;
theorem
for n being Nat 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 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[object]}:
ex q being Real_Sequence st q is
subsequence of s() & (for n being Nat 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 being Nat
for x be Element of NAT 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 being 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] 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 being 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 being 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
ExRealSeq2{F,G(set)->Element of REAL}:
ex s being 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/2)) & ($1 in
M implies $2 = G(($1-1)/2));
A3: for n ex r being Element of REAL st X[n,r]
proof
let n;
now
assume
A4: n in N;
reconsider r = F(n/2) 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 being 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(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)-> Element of 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 being 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(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 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(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)->Element of 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 being 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(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 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(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)->Element of 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 being 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(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 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(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[object],
F,G(object)->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[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 being object holds x in X iff x in C() & X[x] from XBOOLE_0:sch 1;
A3: for x being object st x in X ex y being 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 being Function such that
A7: dom f = X &
for x being 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 being 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
PartFuncExD29{C, D()->non empty set,P,Q[object],
F,G(object)->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[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 being object holds x in Y iff x in C() & X[x] from XBOOLE_0:sch 1;
A3: for x being object st x in Y ex y being 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 being Function such that
A7: dom f = Y &
for x being 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 being 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
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 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
PartFuncExD3{C, D()->non empty set,P,Q,R[object],
F,G,H(object)->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[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 being object holds x in Z iff x in C() & X[x] from XBOOLE_0:sch 1;
A3: for x being object st x in Z ex y being 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 being Function such that
A8: dom f = Z &
for x being 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 being 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
PartFuncExD39{C, D()->non empty set,P,Q,R[object],
F,G,H(object)->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[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 being object holds x in V iff x in C() & X[x] from XBOOLE_0:sch 1;
A3: for x being object st x in V ex y being 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 being Function such that
A15: dom f = V &
for x being 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 being 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
PartFuncExD4{C, D()->non empty set,P,Q,R,S[object],
F,G,H,I(object)->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[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 being object holds x in B iff x in C() & X[x] from XBOOLE_0:sch 1;
A3: for x being object st x in B ex y being 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 being Function such that
A13: dom f = B &
for y being 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 being 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
PartFuncExS2{X, Y()->set,P,Q[object],F,G(object)->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[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 being object holds x in A iff x in X() & X[x] from XBOOLE_0:sch 1;
A5: for x being object st x in A ex y being 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 being Function such that
A10: dom f = A &
for x being 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 being 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
PartFuncExS3{X, Y()->set,P,Q,R[object], F,G,H(object)->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[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 being object holds x in S iff x in X() & X[x] from XBOOLE_0:sch 1;
A6: for x being object st x in S ex y being 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 being Function such that
A12: dom f = S &
for x being 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 being 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
PartFuncExS4{X, Y()->set,P,Q,R,S[object], F,G,H,I(object)->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[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 being object holds x in D iff x in X() & X[x] from XBOOLE_0:sch 1;
A7: for x being object st x in D ex y being 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 being Function such that
A18: dom f = D &
for x being 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 being 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
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[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 being 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 ex z being 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 being Function such that
A10: dom f = F &
for z being 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 being 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
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[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 being 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 ex z being 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 being Function such that
A11: dom f = T &
for z being 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 being 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
PartFuncExCS2{X, Y, Z()->set,P,Q[object,object],
F,G(object,object)->object}:
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[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 being 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 ex z being 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 being Function such that
A11: dom f = K &
for z being 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 being 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
PartFuncExCS3{X, Y, Z()->set, P,Q,R[object,object],
F,G,H(object,object)->object}:
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[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 being 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 ex z being 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 being Function such that
A13: dom f = L &
for z being 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 being 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
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 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
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 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
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 be object;
assume x in [:C(),D():];
then consider y,z being 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
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 be object;
assume x in [:C(),D():];
then consider y,z being 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;