:: SCHEME1 semantic presentation begin theorem :: SCHEME1:1 for n being Element of NAT ex m being Element of NAT st ( n = 2 * m or n = (2 * m) + 1 ) proof let n be Element of NAT ; ::_thesis: ex m being Element of NAT st ( n = 2 * m or n = (2 * m) + 1 ) take n div 2 ; ::_thesis: ( n = 2 * (n div 2) or n = (2 * (n div 2)) + 1 ) set k = n mod 2; A1: ( n mod 2 = 0 or n mod 2 = 1 ) proof n mod 2 < 1 + 1 by NAT_D:1; then A2: n mod 2 <= 0 + 1 by NAT_1:13; now__::_thesis:_(_n_mod_2_=_0_or_n_mod_2_=_1_) percases ( n mod 2 <= 0 or n mod 2 = 0 + 1 ) by A2, NAT_1:8; suppose n mod 2 <= 0 ; ::_thesis: ( n mod 2 = 0 or n mod 2 = 1 ) hence ( n mod 2 = 0 or n mod 2 = 1 ) by NAT_1:2; ::_thesis: verum end; suppose n mod 2 = 0 + 1 ; ::_thesis: ( n mod 2 = 0 or n mod 2 = 1 ) hence ( n mod 2 = 0 or n mod 2 = 1 ) ; ::_thesis: verum end; end; end; hence ( n mod 2 = 0 or n mod 2 = 1 ) ; ::_thesis: verum end; n = (2 * (n div 2)) + (n mod 2) by NAT_D:2; hence ( n = 2 * (n div 2) or n = (2 * (n div 2)) + 1 ) by A1; ::_thesis: verum end; theorem Th2: :: SCHEME1:2 for n being Element of NAT ex m being Element of NAT st ( n = 3 * m or n = (3 * m) + 1 or n = (3 * m) + 2 ) proof let n be Element of NAT ; ::_thesis: ex m being Element of NAT st ( n = 3 * m or n = (3 * m) + 1 or n = (3 * m) + 2 ) take n div 3 ; ::_thesis: ( n = 3 * (n div 3) or n = (3 * (n div 3)) + 1 or n = (3 * (n div 3)) + 2 ) set w = n mod 3; A1: ( n mod 3 = 0 or n mod 3 = 1 or n mod 3 = 2 ) proof n mod 3 < 2 + 1 by NAT_D:1; then A2: n mod 3 <= 1 + 1 by NAT_1:13; now__::_thesis:_(_n_mod_3_=_0_or_n_mod_3_=_1_or_n_mod_3_=_2_) percases ( n mod 3 <= 1 or n mod 3 = 1 + 1 ) by A2, NAT_1:8; supposeA3: n mod 3 <= 1 ; ::_thesis: ( n mod 3 = 0 or n mod 3 = 1 or n mod 3 = 2 ) now__::_thesis:_(_n_mod_3_=_0_or_n_mod_3_=_1_or_n_mod_3_=_2_) percases ( n mod 3 <= 0 or n mod 3 = 0 + 1 ) by A3, NAT_1:8; suppose n mod 3 <= 0 ; ::_thesis: ( n mod 3 = 0 or n mod 3 = 1 or n mod 3 = 2 ) hence ( n mod 3 = 0 or n mod 3 = 1 or n mod 3 = 2 ) by NAT_1:2; ::_thesis: verum end; suppose n mod 3 = 0 + 1 ; ::_thesis: ( n mod 3 = 0 or n mod 3 = 1 or n mod 3 = 2 ) hence ( n mod 3 = 0 or n mod 3 = 1 or n mod 3 = 2 ) ; ::_thesis: verum end; end; end; hence ( n mod 3 = 0 or n mod 3 = 1 or n mod 3 = 2 ) ; ::_thesis: verum end; suppose n mod 3 = 1 + 1 ; ::_thesis: ( n mod 3 = 0 or n mod 3 = 1 or n mod 3 = 2 ) hence ( n mod 3 = 0 or n mod 3 = 1 or n mod 3 = 2 ) ; ::_thesis: verum end; end; end; hence ( n mod 3 = 0 or n mod 3 = 1 or n mod 3 = 2 ) ; ::_thesis: verum end; A4: n = (3 * (n div 3)) + (n mod 3) by NAT_D:2; now__::_thesis:_(_n_=_3_*_(n_div_3)_or_n_=_(3_*_(n_div_3))_+_1_or_n_=_(3_*_(n_div_3))_+_2_) percases ( n mod 3 = 0 or n mod 3 = 1 or n mod 3 = 2 ) by A1; suppose n mod 3 = 0 ; ::_thesis: ( n = 3 * (n div 3) or n = (3 * (n div 3)) + 1 or n = (3 * (n div 3)) + 2 ) hence ( n = 3 * (n div 3) or n = (3 * (n div 3)) + 1 or n = (3 * (n div 3)) + 2 ) by A4; ::_thesis: verum end; suppose n mod 3 = 1 ; ::_thesis: ( n = 3 * (n div 3) or n = (3 * (n div 3)) + 1 or n = (3 * (n div 3)) + 2 ) hence ( n = 3 * (n div 3) or n = (3 * (n div 3)) + 1 or n = (3 * (n div 3)) + 2 ) by NAT_D:2; ::_thesis: verum end; suppose n mod 3 = 2 ; ::_thesis: ( n = 3 * (n div 3) or n = (3 * (n div 3)) + 1 or n = (3 * (n div 3)) + 2 ) hence ( n = 3 * (n div 3) or n = (3 * (n div 3)) + 1 or n = (3 * (n div 3)) + 2 ) by NAT_D:2; ::_thesis: verum end; end; end; hence ( n = 3 * (n div 3) or n = (3 * (n div 3)) + 1 or n = (3 * (n div 3)) + 2 ) ; ::_thesis: verum end; theorem Th3: :: SCHEME1:3 for n being Element of NAT ex m being Element of NAT st ( n = 4 * m or n = (4 * m) + 1 or n = (4 * m) + 2 or n = (4 * m) + 3 ) proof let n be Element of NAT ; ::_thesis: ex m being Element of NAT st ( n = 4 * m or n = (4 * m) + 1 or n = (4 * m) + 2 or n = (4 * m) + 3 ) take n div 4 ; ::_thesis: ( n = 4 * (n div 4) or n = (4 * (n div 4)) + 1 or n = (4 * (n div 4)) + 2 or n = (4 * (n div 4)) + 3 ) set o = n mod 4; A1: ( n mod 4 = 0 or n mod 4 = 1 or n mod 4 = 2 or n mod 4 = 3 ) proof n mod 4 < 3 + 1 by NAT_D:1; then A2: n mod 4 <= 2 + 1 by NAT_1:13; now__::_thesis:_(_n_mod_4_=_0_or_n_mod_4_=_1_or_n_mod_4_=_2_or_n_mod_4_=_3_) percases ( n mod 4 <= 2 or n mod 4 = 2 + 1 ) by A2, NAT_1:8; supposeA3: n mod 4 <= 2 ; ::_thesis: ( n mod 4 = 0 or n mod 4 = 1 or n mod 4 = 2 or n mod 4 = 3 ) now__::_thesis:_(_n_mod_4_=_0_or_n_mod_4_=_1_or_n_mod_4_=_2_or_n_mod_4_=_3_) percases ( n mod 4 <= 1 or n mod 4 = 1 + 1 ) by A3, NAT_1:8; supposeA4: n mod 4 <= 1 ; ::_thesis: ( n mod 4 = 0 or n mod 4 = 1 or n mod 4 = 2 or n mod 4 = 3 ) now__::_thesis:_(_n_mod_4_=_0_or_n_mod_4_=_1_or_n_mod_4_=_2_or_n_mod_4_=_3_) percases ( n mod 4 <= 0 or n mod 4 = 0 + 1 ) by A4, NAT_1:8; suppose n mod 4 <= 0 ; ::_thesis: ( n mod 4 = 0 or n mod 4 = 1 or n mod 4 = 2 or n mod 4 = 3 ) hence ( n mod 4 = 0 or n mod 4 = 1 or n mod 4 = 2 or n mod 4 = 3 ) by NAT_1:2; ::_thesis: verum end; suppose n mod 4 = 0 + 1 ; ::_thesis: ( n mod 4 = 0 or n mod 4 = 1 or n mod 4 = 2 or n mod 4 = 3 ) hence ( n mod 4 = 0 or n mod 4 = 1 or n mod 4 = 2 or n mod 4 = 3 ) ; ::_thesis: verum end; end; end; hence ( n mod 4 = 0 or n mod 4 = 1 or n mod 4 = 2 or n mod 4 = 3 ) ; ::_thesis: verum end; suppose n mod 4 = 1 + 1 ; ::_thesis: ( n mod 4 = 0 or n mod 4 = 1 or n mod 4 = 2 or n mod 4 = 3 ) hence ( n mod 4 = 0 or n mod 4 = 1 or n mod 4 = 2 or n mod 4 = 3 ) ; ::_thesis: verum end; end; end; hence ( n mod 4 = 0 or n mod 4 = 1 or n mod 4 = 2 or n mod 4 = 3 ) ; ::_thesis: verum end; suppose n mod 4 = 2 + 1 ; ::_thesis: ( n mod 4 = 0 or n mod 4 = 1 or n mod 4 = 2 or n mod 4 = 3 ) hence ( n mod 4 = 0 or n mod 4 = 1 or n mod 4 = 2 or n mod 4 = 3 ) ; ::_thesis: verum end; end; end; hence ( n mod 4 = 0 or n mod 4 = 1 or n mod 4 = 2 or n mod 4 = 3 ) ; ::_thesis: verum end; n = (4 * (n div 4)) + (n mod 4) by NAT_D:2; hence ( n = 4 * (n div 4) or n = (4 * (n div 4)) + 1 or n = (4 * (n div 4)) + 2 or n = (4 * (n div 4)) + 3 ) by A1; ::_thesis: verum end; theorem Th4: :: SCHEME1:4 for n being Element of NAT ex m being Element of NAT 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 be Element of NAT ; ::_thesis: ex m being Element of NAT st ( n = 5 * m or n = (5 * m) + 1 or n = (5 * m) + 2 or n = (5 * m) + 3 or n = (5 * m) + 4 ) take n div 5 ; ::_thesis: ( n = 5 * (n div 5) or n = (5 * (n div 5)) + 1 or n = (5 * (n div 5)) + 2 or n = (5 * (n div 5)) + 3 or n = (5 * (n div 5)) + 4 ) set l = n mod 5; A1: ( n mod 5 = 0 or n mod 5 = 1 or n mod 5 = 2 or n mod 5 = 3 or n mod 5 = 4 ) proof n mod 5 < 4 + 1 by NAT_D:1; then A2: n mod 5 <= 3 + 1 by NAT_1:13; now__::_thesis:_(_n_mod_5_=_0_or_n_mod_5_=_1_or_n_mod_5_=_2_or_n_mod_5_=_3_or_n_mod_5_=_4_) percases ( n mod 5 <= 3 or n mod 5 = 3 + 1 ) by A2, NAT_1:8; supposeA3: n mod 5 <= 3 ; ::_thesis: ( n mod 5 = 0 or n mod 5 = 1 or n mod 5 = 2 or n mod 5 = 3 or n mod 5 = 4 ) now__::_thesis:_(_n_mod_5_=_0_or_n_mod_5_=_1_or_n_mod_5_=_2_or_n_mod_5_=_3_or_n_mod_5_=_4_) percases ( n mod 5 <= 2 or n mod 5 = 2 + 1 ) by A3, NAT_1:8; supposeA4: n mod 5 <= 2 ; ::_thesis: ( n mod 5 = 0 or n mod 5 = 1 or n mod 5 = 2 or n mod 5 = 3 or n mod 5 = 4 ) now__::_thesis:_(_n_mod_5_=_0_or_n_mod_5_=_1_or_n_mod_5_=_2_or_n_mod_5_=_3_or_n_mod_5_=_4_) percases ( n mod 5 <= 1 or n mod 5 = 1 + 1 ) by A4, NAT_1:8; supposeA5: n mod 5 <= 1 ; ::_thesis: ( n mod 5 = 0 or n mod 5 = 1 or n mod 5 = 2 or n mod 5 = 3 or n mod 5 = 4 ) now__::_thesis:_(_n_mod_5_=_0_or_n_mod_5_=_1_or_n_mod_5_=_2_or_n_mod_5_=_3_or_n_mod_5_=_4_) percases ( n mod 5 <= 0 or n mod 5 = 0 + 1 ) by A5, NAT_1:8; suppose n mod 5 <= 0 ; ::_thesis: ( n mod 5 = 0 or n mod 5 = 1 or n mod 5 = 2 or n mod 5 = 3 or n mod 5 = 4 ) hence ( n mod 5 = 0 or n mod 5 = 1 or n mod 5 = 2 or n mod 5 = 3 or n mod 5 = 4 ) by NAT_1:2; ::_thesis: verum end; suppose n mod 5 = 0 + 1 ; ::_thesis: ( n mod 5 = 0 or n mod 5 = 1 or n mod 5 = 2 or n mod 5 = 3 or n mod 5 = 4 ) hence ( n mod 5 = 0 or n mod 5 = 1 or n mod 5 = 2 or n mod 5 = 3 or n mod 5 = 4 ) ; ::_thesis: verum end; end; end; hence ( n mod 5 = 0 or n mod 5 = 1 or n mod 5 = 2 or n mod 5 = 3 or n mod 5 = 4 ) ; ::_thesis: verum end; suppose n mod 5 = 1 + 1 ; ::_thesis: ( n mod 5 = 0 or n mod 5 = 1 or n mod 5 = 2 or n mod 5 = 3 or n mod 5 = 4 ) hence ( n mod 5 = 0 or n mod 5 = 1 or n mod 5 = 2 or n mod 5 = 3 or n mod 5 = 4 ) ; ::_thesis: verum end; end; end; hence ( n mod 5 = 0 or n mod 5 = 1 or n mod 5 = 2 or n mod 5 = 3 or n mod 5 = 4 ) ; ::_thesis: verum end; suppose n mod 5 = 2 + 1 ; ::_thesis: ( n mod 5 = 0 or n mod 5 = 1 or n mod 5 = 2 or n mod 5 = 3 or n mod 5 = 4 ) hence ( n mod 5 = 0 or n mod 5 = 1 or n mod 5 = 2 or n mod 5 = 3 or n mod 5 = 4 ) ; ::_thesis: verum end; end; end; hence ( n mod 5 = 0 or n mod 5 = 1 or n mod 5 = 2 or n mod 5 = 3 or n mod 5 = 4 ) ; ::_thesis: verum end; suppose n mod 5 = 3 + 1 ; ::_thesis: ( n mod 5 = 0 or n mod 5 = 1 or n mod 5 = 2 or n mod 5 = 3 or n mod 5 = 4 ) hence ( n mod 5 = 0 or n mod 5 = 1 or n mod 5 = 2 or n mod 5 = 3 or n mod 5 = 4 ) ; ::_thesis: verum end; end; end; hence ( n mod 5 = 0 or n mod 5 = 1 or n mod 5 = 2 or n mod 5 = 3 or n mod 5 = 4 ) ; ::_thesis: verum end; n = (5 * (n div 5)) + (n mod 5) by NAT_D:2; hence ( n = 5 * (n div 5) or n = (5 * (n div 5)) + 1 or n = (5 * (n div 5)) + 2 or n = (5 * (n div 5)) + 3 or n = (5 * (n div 5)) + 4 ) by A1; ::_thesis: verum end; scheme :: SCHEME1:sch 1 ExRealSubseq{ F1() -> Real_Sequence, P1[ set ] } : ex q being Real_Sequence st ( q is subsequence of F1() & ( for n being Element of NAT holds P1[q . n] ) & ( for n being Element of NAT st ( for r being Real st r = F1() . n holds P1[r] ) holds ex m being Element of NAT st F1() . n = q . m ) ) provided A1: for n being Element of NAT ex m being Element of NAT st ( n <= m & P1[F1() . m] ) proof defpred S1[ set , set ] means for n, m being Element of NAT st $1 = n & $2 = m holds ( n < m & P1[F1() . m] & ( for k being Element of NAT st n < k & P1[F1() . k] holds m <= k ) ); defpred S2[ set , set , set ] means S1[$2,$3]; defpred S3[ set ] means P1[F1() . $1]; ex m1 being Element of NAT st ( 0 <= m1 & P1[F1() . m1] ) by A1; then A2: ex m being Nat st S3[m] ; consider M being Nat such that A3: ( S3[M] & ( for n being Nat st S3[n] holds M <= n ) ) from NAT_1:sch_5(A2); reconsider M9 = M as Element of NAT by ORDINAL1:def_12; A4: now__::_thesis:_for_n_being_Element_of_NAT_ex_m_being_Element_of_NAT_st_ (_n_<_m_&_P1[F1()_._m]_) let n be Element of NAT ; ::_thesis: ex m being Element of NAT st ( n < m & P1[F1() . m] ) consider m being Element of NAT such that A5: ( n + 1 <= m & P1[F1() . m] ) by A1; take m = m; ::_thesis: ( n < m & P1[F1() . m] ) thus ( n < m & P1[F1() . m] ) by A5, NAT_1:13; ::_thesis: verum end; A6: for n, x being Element of NAT ex y being Element of NAT st S2[n,x,y] proof let n, x be Element of NAT ; ::_thesis: ex y being Element of NAT st S2[n,x,y] defpred S4[ Nat] means ( x < $1 & P1[F1() . $1] ); ex m being Element of NAT st S4[m] by A4; then A7: ex m being Nat st S4[m] ; consider l being Nat such that A8: ( S4[l] & ( for k being Nat st S4[k] holds l <= k ) ) from NAT_1:sch_5(A7); reconsider l = l as Element of NAT by ORDINAL1:def_12; take l ; ::_thesis: S2[n,x,l] thus S2[n,x,l] by A8; ::_thesis: verum end; consider F being Function of NAT,NAT such that A9: ( F . 0 = M9 & ( for n being Element of NAT holds S2[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch_2(A6); ( dom F = NAT & rng F c= REAL ) by FUNCT_2:def_1, XBOOLE_1:1; then reconsider F = F as natural-valued Real_Sequence by FUNCT_2:def_1, RELSET_1:4; for n being Element of NAT holds F . n < F . (n + 1) by A9; then reconsider F = F as increasing sequence of NAT by SEQM_3:def_6; A10: for n being Element of NAT st P1[F1() . n] holds ex m being Element of NAT st F . m = n proof defpred S4[ set ] means ( P1[F1() . $1] & ( for m being Element of NAT holds F . m <> $1 ) ); assume ex n being Element of NAT st S4[n] ; ::_thesis: contradiction then A11: ex n being Nat st S4[n] ; consider M1 being Nat such that A12: ( S4[M1] & ( for n being Nat st S4[n] holds M1 <= n ) ) from NAT_1:sch_5(A11); defpred S5[ Nat] means ( $1 < M1 & P1[F1() . $1] & ex m being Element of NAT st F . m = $1 ); A13: ex n being Nat st S5[n] proof take M ; ::_thesis: S5[M] ( M <= M1 & M <> M1 ) by A3, A9, A12; hence M < M1 by XXREAL_0:1; ::_thesis: ( P1[F1() . M] & ex m being Element of NAT st F . m = M ) thus P1[F1() . M] by A3; ::_thesis: ex m being Element of NAT st F . m = M take 0 ; ::_thesis: F . 0 = M thus F . 0 = M by A9; ::_thesis: verum end; A14: for n being Nat st S5[n] holds n <= M1 ; consider X being Nat such that A15: ( S5[X] & ( for n being Nat st S5[n] holds n <= X ) ) from NAT_1:sch_6(A14, A13); A16: for k being Element of NAT st X < k & k < M1 holds not P1[F1() . k] proof given k being Element of NAT such that A17: X < k and A18: ( k < M1 & P1[F1() . k] ) ; ::_thesis: contradiction now__::_thesis:_contradiction percases ( ex m being Element of NAT st F . m = k or for m being Element of NAT holds F . m <> k ) ; suppose ex m being Element of NAT st F . m = k ; ::_thesis: contradiction hence contradiction by A15, A17, A18; ::_thesis: verum end; suppose for m being Element of NAT holds F . m <> k ; ::_thesis: contradiction hence contradiction by A12, A18; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; consider m being Element of NAT such that A19: F . m = X by A15; A20: ( X < F . (m + 1) & P1[F1() . (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__::_thesis:_not_F_._(m_+_1)_<>_M1 assume F . (m + 1) <> M1 ; ::_thesis: contradiction then F . (m + 1) < M1 by A21, XXREAL_0:1; hence contradiction by A16, A20; ::_thesis: verum end; hence contradiction by A12; ::_thesis: verum end; take q = F1() * F; ::_thesis: ( q is subsequence of F1() & ( for n being Element of NAT holds P1[q . n] ) & ( for n being Element of NAT st ( for r being Real st r = F1() . n holds P1[r] ) holds ex m being Element of NAT st F1() . n = q . m ) ) defpred S4[ set ] means P1[q . $1]; A22: for k being Element of NAT st S4[k] holds S4[k + 1] proof let k be Element of NAT ; ::_thesis: ( S4[k] implies S4[k + 1] ) assume P1[q . k] ; ::_thesis: S4[k + 1] S1[F . k,F . (k + 1)] by A9; then P1[F1() . (F . (k + 1))] ; hence S4[k + 1] by FUNCT_2:15; ::_thesis: verum end; thus q is subsequence of F1() ; ::_thesis: ( ( for n being Element of NAT holds P1[q . n] ) & ( for n being Element of NAT st ( for r being Real st r = F1() . n holds P1[r] ) holds ex m being Element of NAT st F1() . n = q . m ) ) A23: S4[ 0 ] by A3, A9, FUNCT_2:15; thus for n being Element of NAT holds S4[n] from NAT_1:sch_1(A23, A22); ::_thesis: for n being Element of NAT st ( for r being Real st r = F1() . n holds P1[r] ) holds ex m being Element of NAT st F1() . n = q . m let n be Element of NAT ; ::_thesis: ( ( for r being Real st r = F1() . n holds P1[r] ) implies ex m being Element of NAT st F1() . n = q . m ) assume for r being Real st r = F1() . n holds P1[r] ; ::_thesis: ex m being Element of NAT st F1() . n = q . m then consider m being Element of NAT such that A24: F . m = n by A10; take m ; ::_thesis: F1() . n = q . m thus F1() . n = q . m by A24, FUNCT_2:15; ::_thesis: verum end; scheme :: SCHEME1:sch 2 ExRealSeq2{ F1( set ) -> Real, F2( set ) -> Real } : ex s being Real_Sequence st for n being Element of NAT holds ( s . (2 * n) = F1(n) & s . ((2 * n) + 1) = F2(n) ) proof defpred S1[ set ] means ex m being Element of NAT st $1 = 2 * m; consider N being Subset of NAT such that A1: for n being Element of NAT holds ( n in N iff S1[n] ) from SUBSET_1:sch_3(); defpred S2[ set ] means ex m being Element of NAT st $1 = (2 * m) + 1; consider M being Subset of NAT such that A2: for n being Element of NAT holds ( n in M iff S2[n] ) from SUBSET_1:sch_3(); defpred S3[ Element of NAT , set ] means ( ( $1 in N implies $2 = F1(($1 / 2)) ) & ( $1 in M implies $2 = F2((($1 - 1) / 2)) ) ); A3: for n being Element of NAT ex r being Real st S3[n,r] proof let n be Element of NAT ; ::_thesis: ex r being Real st S3[n,r] now__::_thesis:_(_n_in_N_implies_ex_r,_r_being_Real_st_S3[n,r]_) assume A4: n in N ; ::_thesis: ex r, r being Real st S3[n,r] take r = F1((n / 2)); ::_thesis: ex r being Real st S3[n,r] now__::_thesis:_not_n_in_M assume n in M ; ::_thesis: contradiction then A5: ex k being Element of NAT st n = (2 * k) + 1 by A2; consider m being Element of NAT such that A6: n = 2 * m by A1, A4; n = (2 * m) + 0 by A6; hence contradiction by A5, NAT_1:18; ::_thesis: verum end; hence ex r being Real st S3[n,r] ; ::_thesis: verum end; hence ex r being Real st S3[n,r] ; ::_thesis: verum end; consider f being Function of NAT,REAL such that A7: for n being Element of NAT holds S3[n,f . n] from FUNCT_2:sch_3(A3); reconsider f = f as Real_Sequence ; take f ; ::_thesis: for n being Element of NAT holds ( f . (2 * n) = F1(n) & f . ((2 * n) + 1) = F2(n) ) let n be Element of NAT ; ::_thesis: ( f . (2 * n) = F1(n) & f . ((2 * n) + 1) = F2(n) ) 2 * n in N by A1; hence f . (2 * n) = F1(((2 * n) / 2)) by A7 .= F1(n) ; ::_thesis: f . ((2 * n) + 1) = F2(n) (2 * n) + 1 in M by A2; hence f . ((2 * n) + 1) = F2(((((2 * n) + 1) - 1) / 2)) by A7 .= F2(n) ; ::_thesis: verum end; scheme :: SCHEME1:sch 3 ExRealSeq3{ F1( set ) -> Real, F2( set ) -> Real, F3( set ) -> Real } : ex s being Real_Sequence st for n being Element of NAT holds ( s . (3 * n) = F1(n) & s . ((3 * n) + 1) = F2(n) & s . ((3 * n) + 2) = F3(n) ) proof defpred S1[ set ] means ex m being Element of NAT st $1 = 3 * m; consider E being Subset of NAT such that A1: for n being Element of NAT holds ( n in E iff S1[n] ) from SUBSET_1:sch_3(); defpred S2[ set ] means ex m being Element of NAT st $1 = (3 * m) + 1; consider G being Subset of NAT such that A2: for n being Element of NAT holds ( n in G iff S2[n] ) from SUBSET_1:sch_3(); defpred S3[ set ] means ex m being Element of NAT st $1 = (3 * m) + 2; consider K being Subset of NAT such that A3: for n being Element of NAT holds ( n in K iff S3[n] ) from SUBSET_1:sch_3(); defpred S4[ Element of NAT , set ] means ( ( $1 in E implies $2 = F1(($1 / 3)) ) & ( $1 in G implies $2 = F2((($1 - 1) / 3)) ) & ( $1 in K implies $2 = F3((($1 - 2) / 3)) ) ); A4: for n being Element of NAT ex r being Real st S4[n,r] proof let n be Element of NAT ; ::_thesis: ex r being Real st S4[n,r] consider m being Element of NAT such that A5: ( n = 3 * m or n = (3 * m) + 1 or n = (3 * m) + 2 ) by Th2; now__::_thesis:_ex_r,_r_being_Real_st_S4[n,r] percases ( n = 3 * m or n = (3 * m) + 1 or n = (3 * m) + 2 ) by A5; supposeA6: n = 3 * m ; ::_thesis: ex r, r being Real st S4[n,r] take r = F1((n / 3)); ::_thesis: ex r being Real st S4[n,r] A7: n = (3 * m) + 0 by A6; A8: now__::_thesis:_not_n_in_K assume n in K ; ::_thesis: contradiction then ex k being Element of NAT st n = (3 * k) + 2 by A3; hence contradiction by A7, NAT_1:18; ::_thesis: verum end; now__::_thesis:_not_n_in_G assume n in G ; ::_thesis: contradiction then ex k being Element of NAT st n = (3 * k) + 1 by A2; hence contradiction by A7, NAT_1:18; ::_thesis: verum end; hence ex r being Real st S4[n,r] by A8; ::_thesis: verum end; supposeA9: n = (3 * m) + 1 ; ::_thesis: ex r, r being Real st S4[n,r] take r = F2(((n - 1) / 3)); ::_thesis: ex r being Real st S4[n,r] A10: now__::_thesis:_not_n_in_E assume n in E ; ::_thesis: contradiction then consider k being Element of NAT such that A11: n = 3 * k by A1; n = (3 * k) + 0 by A11; hence contradiction by A9, NAT_1:18; ::_thesis: verum end; now__::_thesis:_not_n_in_K assume n in K ; ::_thesis: contradiction then ex k being Element of NAT st n = (3 * k) + 2 by A3; hence contradiction by A9, NAT_1:18; ::_thesis: verum end; hence ex r being Real st S4[n,r] by A10; ::_thesis: verum end; supposeA12: n = (3 * m) + 2 ; ::_thesis: ex r, r being Real st S4[n,r] take r = F3(((n - 2) / 3)); ::_thesis: ex r being Real st S4[n,r] A13: now__::_thesis:_not_n_in_E assume n in E ; ::_thesis: contradiction then consider k being Element of NAT such that A14: n = 3 * k by A1; n = (3 * k) + 0 by A14; hence contradiction by A12, NAT_1:18; ::_thesis: verum end; now__::_thesis:_not_n_in_G assume n in G ; ::_thesis: contradiction then ex k being Element of NAT st n = (3 * k) + 1 by A2; hence contradiction by A12, NAT_1:18; ::_thesis: verum end; hence ex r being Real st S4[n,r] by A13; ::_thesis: verum end; end; end; hence ex r being Real st S4[n,r] ; ::_thesis: verum end; consider f being Function of NAT,REAL such that A15: for n being Element of NAT holds S4[n,f . n] from FUNCT_2:sch_3(A4); reconsider f = f as Real_Sequence ; take f ; ::_thesis: for n being Element of NAT holds ( f . (3 * n) = F1(n) & f . ((3 * n) + 1) = F2(n) & f . ((3 * n) + 2) = F3(n) ) let n be Element of NAT ; ::_thesis: ( f . (3 * n) = F1(n) & f . ((3 * n) + 1) = F2(n) & f . ((3 * n) + 2) = F3(n) ) 3 * n in E by A1; hence f . (3 * n) = F1(((3 * n) / 3)) by A15 .= F1(n) ; ::_thesis: ( f . ((3 * n) + 1) = F2(n) & f . ((3 * n) + 2) = F3(n) ) (3 * n) + 1 in G by A2; hence f . ((3 * n) + 1) = F2(((((3 * n) + 1) - 1) / 3)) by A15 .= F2(n) ; ::_thesis: f . ((3 * n) + 2) = F3(n) (3 * n) + 2 in K by A3; hence f . ((3 * n) + 2) = F3(((((3 * n) + 2) - 2) / 3)) by A15 .= F3(n) ; ::_thesis: verum end; scheme :: SCHEME1:sch 4 ExRealSeq4{ F1( set ) -> Real, F2( set ) -> Real, F3( set ) -> Real, F4( set ) -> Real } : ex s being Real_Sequence st for n being Element of NAT holds ( s . (4 * n) = F1(n) & s . ((4 * n) + 1) = F2(n) & s . ((4 * n) + 2) = F3(n) & s . ((4 * n) + 3) = F4(n) ) proof defpred S1[ set ] means ex m being Element of NAT st $1 = 4 * m; consider Q being Subset of NAT such that A1: for n being Element of NAT holds ( n in Q iff S1[n] ) from SUBSET_1:sch_3(); defpred S2[ set ] means ex m being Element of NAT st $1 = (4 * m) + 1; consider R being Subset of NAT such that A2: for n being Element of NAT holds ( n in R iff S2[n] ) from SUBSET_1:sch_3(); defpred S3[ set ] means ex m being Element of NAT st $1 = (4 * m) + 2; consider P being Subset of NAT such that A3: for n being Element of NAT holds ( n in P iff S3[n] ) from SUBSET_1:sch_3(); defpred S4[ set ] means ex m being Element of NAT st $1 = (4 * m) + 3; consider L being Subset of NAT such that A4: for n being Element of NAT holds ( n in L iff S4[n] ) from SUBSET_1:sch_3(); defpred S5[ Element of NAT , set ] means ( ( $1 in Q implies $2 = F1(($1 / 4)) ) & ( $1 in R implies $2 = F2((($1 - 1) / 4)) ) & ( $1 in P implies $2 = F3((($1 - 2) / 4)) ) & ( $1 in L implies $2 = F4((($1 - 3) / 4)) ) ); A5: for n being Element of NAT ex r being Real st S5[n,r] proof let n be Element of NAT ; ::_thesis: ex r being Real st S5[n,r] consider m being Element of NAT such that A6: ( n = 4 * m or n = (4 * m) + 1 or n = (4 * m) + 2 or n = (4 * m) + 3 ) by Th3; now__::_thesis:_ex_r,_r_being_Real_st_S5[n,r] percases ( n = 4 * m or n = (4 * m) + 1 or n = (4 * m) + 2 or n = (4 * m) + 3 ) by A6; supposeA7: n = 4 * m ; ::_thesis: ex r, r being Real st S5[n,r] take r = F1((n / 4)); ::_thesis: ex r being Real st S5[n,r] A8: n = (4 * m) + 0 by A7; A9: now__::_thesis:_not_n_in_P assume n in P ; ::_thesis: contradiction then ex k being Element of NAT st n = (4 * k) + 2 by A3; hence contradiction by A8, NAT_1:18; ::_thesis: verum end; A10: now__::_thesis:_not_n_in_L assume n in L ; ::_thesis: contradiction then ex k being Element of NAT st n = (4 * k) + 3 by A4; hence contradiction by A8, NAT_1:18; ::_thesis: verum end; now__::_thesis:_not_n_in_R assume n in R ; ::_thesis: contradiction then ex k being Element of NAT st n = (4 * k) + 1 by A2; hence contradiction by A8, NAT_1:18; ::_thesis: verum end; hence ex r being Real st S5[n,r] by A9, A10; ::_thesis: verum end; supposeA11: n = (4 * m) + 1 ; ::_thesis: ex r, r being Real st S5[n,r] take r = F2(((n - 1) / 4)); ::_thesis: ex r being Real st S5[n,r] A12: now__::_thesis:_not_n_in_Q assume n in Q ; ::_thesis: contradiction then consider k being Element of NAT such that A13: n = 4 * k by A1; n = (4 * k) + 0 by A13; hence contradiction by A11, NAT_1:18; ::_thesis: verum end; A14: now__::_thesis:_not_n_in_L assume n in L ; ::_thesis: contradiction then ex k being Element of NAT st n = (4 * k) + 3 by A4; hence contradiction by A11, NAT_1:18; ::_thesis: verum end; now__::_thesis:_not_n_in_P assume n in P ; ::_thesis: contradiction then ex k being Element of NAT st n = (4 * k) + 2 by A3; hence contradiction by A11, NAT_1:18; ::_thesis: verum end; hence ex r being Real st S5[n,r] by A12, A14; ::_thesis: verum end; supposeA15: n = (4 * m) + 2 ; ::_thesis: ex r, r being Real st S5[n,r] take r = F3(((n - 2) / 4)); ::_thesis: ex r being Real st S5[n,r] A16: now__::_thesis:_not_n_in_Q assume n in Q ; ::_thesis: contradiction then consider k being Element of NAT such that A17: n = 4 * k by A1; n = (4 * k) + 0 by A17; hence contradiction by A15, NAT_1:18; ::_thesis: verum end; A18: now__::_thesis:_not_n_in_L assume n in L ; ::_thesis: contradiction then ex k being Element of NAT st n = (4 * k) + 3 by A4; hence contradiction by A15, NAT_1:18; ::_thesis: verum end; now__::_thesis:_not_n_in_R assume n in R ; ::_thesis: contradiction then ex k being Element of NAT st n = (4 * k) + 1 by A2; hence contradiction by A15, NAT_1:18; ::_thesis: verum end; hence ex r being Real st S5[n,r] by A16, A18; ::_thesis: verum end; supposeA19: n = (4 * m) + 3 ; ::_thesis: ex r, r being Real st S5[n,r] take r = F4(((n - 3) / 4)); ::_thesis: ex r being Real st S5[n,r] A20: now__::_thesis:_not_n_in_Q assume n in Q ; ::_thesis: contradiction then consider k being Element of NAT such that A21: n = 4 * k by A1; n = (4 * k) + 0 by A21; hence contradiction by A19, NAT_1:18; ::_thesis: verum end; A22: now__::_thesis:_not_n_in_P assume n in P ; ::_thesis: contradiction then ex k being Element of NAT st n = (4 * k) + 2 by A3; hence contradiction by A19, NAT_1:18; ::_thesis: verum end; now__::_thesis:_not_n_in_R assume n in R ; ::_thesis: contradiction then ex k being Element of NAT st n = (4 * k) + 1 by A2; hence contradiction by A19, NAT_1:18; ::_thesis: verum end; hence ex r being Real st S5[n,r] by A20, A22; ::_thesis: verum end; end; end; hence ex r being Real st S5[n,r] ; ::_thesis: verum end; consider f being Function of NAT,REAL such that A23: for n being Element of NAT holds S5[n,f . n] from FUNCT_2:sch_3(A5); reconsider f = f as Real_Sequence ; take f ; ::_thesis: for n being Element of NAT holds ( f . (4 * n) = F1(n) & f . ((4 * n) + 1) = F2(n) & f . ((4 * n) + 2) = F3(n) & f . ((4 * n) + 3) = F4(n) ) let n be Element of NAT ; ::_thesis: ( f . (4 * n) = F1(n) & f . ((4 * n) + 1) = F2(n) & f . ((4 * n) + 2) = F3(n) & f . ((4 * n) + 3) = F4(n) ) 4 * n in Q by A1; hence f . (4 * n) = F1(((4 * n) / 4)) by A23 .= F1(n) ; ::_thesis: ( f . ((4 * n) + 1) = F2(n) & f . ((4 * n) + 2) = F3(n) & f . ((4 * n) + 3) = F4(n) ) (4 * n) + 1 in R by A2; hence f . ((4 * n) + 1) = F2(((((4 * n) + 1) - 1) / 4)) by A23 .= F2(n) ; ::_thesis: ( f . ((4 * n) + 2) = F3(n) & f . ((4 * n) + 3) = F4(n) ) (4 * n) + 2 in P by A3; hence f . ((4 * n) + 2) = F3(((((4 * n) + 2) - 2) / 4)) by A23 .= F3(n) ; ::_thesis: f . ((4 * n) + 3) = F4(n) (4 * n) + 3 in L by A4; hence f . ((4 * n) + 3) = F4(((((4 * n) + 3) - 3) / 4)) by A23 .= F4(n) ; ::_thesis: verum end; scheme :: SCHEME1:sch 5 ExRealSeq5{ F1( set ) -> Real, F2( set ) -> Real, F3( set ) -> Real, F4( set ) -> Real, F5( set ) -> Real } : ex s being Real_Sequence st for n being Element of NAT holds ( s . (5 * n) = F1(n) & s . ((5 * n) + 1) = F2(n) & s . ((5 * n) + 2) = F3(n) & s . ((5 * n) + 3) = F4(n) & s . ((5 * n) + 4) = F5(n) ) proof defpred S1[ set ] means ex m being Element of NAT st $1 = 5 * m; consider N being Subset of NAT such that A1: for n being Element of NAT holds ( n in N iff S1[n] ) from SUBSET_1:sch_3(); defpred S2[ set ] means ex m being Element of NAT st $1 = (5 * m) + 1; consider M being Subset of NAT such that A2: for n being Element of NAT holds ( n in M iff S2[n] ) from SUBSET_1:sch_3(); defpred S3[ set ] means ex m being Element of NAT st $1 = (5 * m) + 2; consider K being Subset of NAT such that A3: for n being Element of NAT holds ( n in K iff S3[n] ) from SUBSET_1:sch_3(); defpred S4[ set ] means ex m being Element of NAT st $1 = (5 * m) + 3; consider L being Subset of NAT such that A4: for n being Element of NAT holds ( n in L iff S4[n] ) from SUBSET_1:sch_3(); defpred S5[ set ] means ex m being Element of NAT st $1 = (5 * m) + 4; consider O being Subset of NAT such that A5: for n being Element of NAT holds ( n in O iff S5[n] ) from SUBSET_1:sch_3(); defpred S6[ Element of NAT , set ] means ( ( $1 in N implies $2 = F1(($1 / 5)) ) & ( $1 in M implies $2 = F2((($1 - 1) / 5)) ) & ( $1 in K implies $2 = F3((($1 - 2) / 5)) ) & ( $1 in L implies $2 = F4((($1 - 3) / 5)) ) & ( $1 in O implies $2 = F5((($1 - 4) / 5)) ) ); A6: for n being Element of NAT ex r being Real st S6[n,r] proof let n be Element of NAT ; ::_thesis: ex r being Real st S6[n,r] consider m being Element of NAT 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__::_thesis:_ex_r,_r_being_Real_st_S6[n,r] percases ( n = 5 * m or n = (5 * m) + 1 or n = (5 * m) + 2 or n = (5 * m) + 3 or n = (5 * m) + 4 ) by A7; supposeA8: n = 5 * m ; ::_thesis: ex r, r being Real st S6[n,r] take r = F1((n / 5)); ::_thesis: ex r being Real st S6[n,r] A9: n = (5 * m) + 0 by A8; A10: now__::_thesis:_not_n_in_K assume n in K ; ::_thesis: contradiction then ex k being Element of NAT st n = (5 * k) + 2 by A3; hence contradiction by A9, NAT_1:18; ::_thesis: verum end; A11: now__::_thesis:_not_n_in_O assume n in O ; ::_thesis: contradiction then ex k being Element of NAT st n = (5 * k) + 4 by A5; hence contradiction by A9, NAT_1:18; ::_thesis: verum end; A12: now__::_thesis:_not_n_in_L assume n in L ; ::_thesis: contradiction then ex k being Element of NAT st n = (5 * k) + 3 by A4; hence contradiction by A9, NAT_1:18; ::_thesis: verum end; now__::_thesis:_not_n_in_M assume n in M ; ::_thesis: contradiction then ex k being Element of NAT st n = (5 * k) + 1 by A2; hence contradiction by A9, NAT_1:18; ::_thesis: verum end; hence ex r being Real st S6[n,r] by A10, A12, A11; ::_thesis: verum end; supposeA13: n = (5 * m) + 1 ; ::_thesis: ex r, r being Real st S6[n,r] A14: now__::_thesis:_not_n_in_O assume n in O ; ::_thesis: contradiction then ex k being Element of NAT st n = (5 * k) + 4 by A5; hence contradiction by A13, NAT_1:18; ::_thesis: verum end; A15: now__::_thesis:_not_n_in_L assume n in L ; ::_thesis: contradiction then ex k being Element of NAT st n = (5 * k) + 3 by A4; hence contradiction by A13, NAT_1:18; ::_thesis: verum end; take r = F2(((n - 1) / 5)); ::_thesis: ex r being Real st S6[n,r] A16: now__::_thesis:_not_n_in_N assume n in N ; ::_thesis: contradiction then consider k being Element of NAT such that A17: n = 5 * k by A1; n = (5 * k) + 0 by A17; hence contradiction by A13, NAT_1:18; ::_thesis: verum end; now__::_thesis:_not_n_in_K assume n in K ; ::_thesis: contradiction then ex k being Element of NAT st n = (5 * k) + 2 by A3; hence contradiction by A13, NAT_1:18; ::_thesis: verum end; hence ex r being Real st S6[n,r] by A16, A15, A14; ::_thesis: verum end; supposeA18: n = (5 * m) + 2 ; ::_thesis: ex r, r being Real st S6[n,r] A19: now__::_thesis:_not_n_in_O assume n in O ; ::_thesis: contradiction then ex k being Element of NAT st n = (5 * k) + 4 by A5; hence contradiction by A18, NAT_1:18; ::_thesis: verum end; A20: now__::_thesis:_not_n_in_L assume n in L ; ::_thesis: contradiction then ex k being Element of NAT st n = (5 * k) + 3 by A4; hence contradiction by A18, NAT_1:18; ::_thesis: verum end; take r = F3(((n - 2) / 5)); ::_thesis: ex r being Real st S6[n,r] A21: now__::_thesis:_not_n_in_N assume n in N ; ::_thesis: contradiction then consider k being Element of NAT such that A22: n = 5 * k by A1; n = (5 * k) + 0 by A22; hence contradiction by A18, NAT_1:18; ::_thesis: verum end; now__::_thesis:_not_n_in_M assume n in M ; ::_thesis: contradiction then ex k being Element of NAT st n = (5 * k) + 1 by A2; hence contradiction by A18, NAT_1:18; ::_thesis: verum end; hence ex r being Real st S6[n,r] by A21, A20, A19; ::_thesis: verum end; supposeA23: n = (5 * m) + 3 ; ::_thesis: ex r, r being Real st S6[n,r] A24: now__::_thesis:_not_n_in_O assume n in O ; ::_thesis: contradiction then ex k being Element of NAT st n = (5 * k) + 4 by A5; hence contradiction by A23, NAT_1:18; ::_thesis: verum end; A25: now__::_thesis:_not_n_in_K assume n in K ; ::_thesis: contradiction then ex k being Element of NAT st n = (5 * k) + 2 by A3; hence contradiction by A23, NAT_1:18; ::_thesis: verum end; take r = F4(((n - 3) / 5)); ::_thesis: ex r being Real st S6[n,r] A26: now__::_thesis:_not_n_in_N assume n in N ; ::_thesis: contradiction then consider k being Element of NAT such that A27: n = 5 * k by A1; n = (5 * k) + 0 by A27; hence contradiction by A23, NAT_1:18; ::_thesis: verum end; now__::_thesis:_not_n_in_M assume n in M ; ::_thesis: contradiction then ex k being Element of NAT st n = (5 * k) + 1 by A2; hence contradiction by A23, NAT_1:18; ::_thesis: verum end; hence ex r being Real st S6[n,r] by A26, A25, A24; ::_thesis: verum end; supposeA28: n = (5 * m) + 4 ; ::_thesis: ex r, r being Real st S6[n,r] A29: now__::_thesis:_not_n_in_L assume n in L ; ::_thesis: contradiction then ex k being Element of NAT st n = (5 * k) + 3 by A4; hence contradiction by A28, NAT_1:18; ::_thesis: verum end; A30: now__::_thesis:_not_n_in_K assume n in K ; ::_thesis: contradiction then ex k being Element of NAT st n = (5 * k) + 2 by A3; hence contradiction by A28, NAT_1:18; ::_thesis: verum end; take r = F5(((n - 4) / 5)); ::_thesis: ex r being Real st S6[n,r] A31: now__::_thesis:_not_n_in_N assume n in N ; ::_thesis: contradiction then consider k being Element of NAT such that A32: n = 5 * k by A1; n = (5 * k) + 0 by A32; hence contradiction by A28, NAT_1:18; ::_thesis: verum end; now__::_thesis:_not_n_in_M assume n in M ; ::_thesis: contradiction then ex k being Element of NAT st n = (5 * k) + 1 by A2; hence contradiction by A28, NAT_1:18; ::_thesis: verum end; hence ex r being Real st S6[n,r] by A31, A30, A29; ::_thesis: verum end; end; end; hence ex r being Real st S6[n,r] ; ::_thesis: verum end; consider f being Function of NAT,REAL such that A33: for n being Element of NAT holds S6[n,f . n] from FUNCT_2:sch_3(A6); reconsider f = f as Real_Sequence ; take f ; ::_thesis: for n being Element of NAT holds ( f . (5 * n) = F1(n) & f . ((5 * n) + 1) = F2(n) & f . ((5 * n) + 2) = F3(n) & f . ((5 * n) + 3) = F4(n) & f . ((5 * n) + 4) = F5(n) ) let n be Element of NAT ; ::_thesis: ( f . (5 * n) = F1(n) & f . ((5 * n) + 1) = F2(n) & f . ((5 * n) + 2) = F3(n) & f . ((5 * n) + 3) = F4(n) & f . ((5 * n) + 4) = F5(n) ) 5 * n in N by A1; hence f . (5 * n) = F1(((5 * n) / 5)) by A33 .= F1(n) ; ::_thesis: ( f . ((5 * n) + 1) = F2(n) & f . ((5 * n) + 2) = F3(n) & f . ((5 * n) + 3) = F4(n) & f . ((5 * n) + 4) = F5(n) ) (5 * n) + 1 in M by A2; hence f . ((5 * n) + 1) = F2(((((5 * n) + 1) - 1) / 5)) by A33 .= F2(n) ; ::_thesis: ( f . ((5 * n) + 2) = F3(n) & f . ((5 * n) + 3) = F4(n) & f . ((5 * n) + 4) = F5(n) ) (5 * n) + 2 in K by A3; hence f . ((5 * n) + 2) = F3(((((5 * n) + 2) - 2) / 5)) by A33 .= F3(n) ; ::_thesis: ( f . ((5 * n) + 3) = F4(n) & f . ((5 * n) + 4) = F5(n) ) (5 * n) + 3 in L by A4; hence f . ((5 * n) + 3) = F4(((((5 * n) + 3) - 3) / 5)) by A33 .= F4(n) ; ::_thesis: f . ((5 * n) + 4) = F5(n) (5 * n) + 4 in O by A5; hence f . ((5 * n) + 4) = F5(((((5 * n) + 4) - 4) / 5)) by A33 .= F5(n) ; ::_thesis: verum end; scheme :: SCHEME1:sch 6 PartFuncExD2{ F1() -> non empty set , F2() -> non empty set , P1[ set ], P2[ set ], F3( set ) -> Element of F2(), F4( set ) -> Element of F2() } : ex f being PartFunc of F1(),F2() st ( ( for c being Element of F1() holds ( c in dom f iff ( P1[c] or P2[c] ) ) ) & ( for c being Element of F1() st c in dom f holds ( ( P1[c] implies f . c = F3(c) ) & ( P2[c] implies f . c = F4(c) ) ) ) ) provided A1: for c being Element of F1() st P1[c] holds not P2[c] proof defpred S1[ set , set ] means ( ( P1[$1] implies $2 = F3($1) ) & ( P2[$1] implies $2 = F4($1) ) ); defpred S2[ set ] means ( P1[$1] or P2[$1] ); consider X being set such that A2: for x being set holds ( x in X iff ( x in F1() & S2[x] ) ) from XBOOLE_0:sch_1(); A3: for x being set st x in X holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in X implies ex y being set st S1[x,y] ) assume A4: x in X ; ::_thesis: ex y being set st S1[x,y] then reconsider x9 = x as Element of F1() by A2; now__::_thesis:_ex_y_being_Element_of_F2()_ex_y_being_set_st_S1[x,y] percases ( P1[x] or P2[x] ) by A2, A4; supposeA5: P1[x] ; ::_thesis: ex y being Element of F2() ex y being set st S1[x,y] take y = F3(x); ::_thesis: ex y being set st S1[x,y] P2[x9] by A1, A5; hence ex y being set st S1[x,y] ; ::_thesis: verum end; supposeA6: P2[x] ; ::_thesis: ex y being Element of F2() ex y being set st S1[x,y] take y = F4(x); ::_thesis: ex y being set st S1[x,y] P1[x9] by A1, A6; hence ex y being set st S1[x,y] ; ::_thesis: verum end; end; end; hence ex y being set st S1[x,y] ; ::_thesis: verum end; consider f being Function such that A7: ( dom f = X & ( for x being set st x in X holds S1[x,f . x] ) ) from CLASSES1:sch_1(A3); A8: X c= F1() proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in F1() ) assume x in X ; ::_thesis: x in F1() hence x in F1() by A2; ::_thesis: verum end; rng f c= F2() proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in F2() ) assume x in rng f ; ::_thesis: x in F2() then consider y being set such that A9: y in dom f and A10: x = f . y by FUNCT_1:def_3; now__::_thesis:_x_in_F2() percases ( P1[y] or P2[y] ) by A2, A7, A9; suppose P1[y] ; ::_thesis: x in F2() then f . y = F3(y) by A7, A9; hence x in F2() by A10; ::_thesis: verum end; suppose P2[y] ; ::_thesis: x in F2() then f . y = F4(y) by A7, A9; hence x in F2() by A10; ::_thesis: verum end; end; end; hence x in F2() ; ::_thesis: verum end; then reconsider q = f as PartFunc of F1(),F2() by A8, A7, RELSET_1:4; take q ; ::_thesis: ( ( for c being Element of F1() holds ( c in dom q iff ( P1[c] or P2[c] ) ) ) & ( for c being Element of F1() st c in dom q holds ( ( P1[c] implies q . c = F3(c) ) & ( P2[c] implies q . c = F4(c) ) ) ) ) thus for c being Element of F1() holds ( c in dom q iff ( P1[c] or P2[c] ) ) by A2, A7; ::_thesis: for c being Element of F1() st c in dom q holds ( ( P1[c] implies q . c = F3(c) ) & ( P2[c] implies q . c = F4(c) ) ) let b be Element of F1(); ::_thesis: ( b in dom q implies ( ( P1[b] implies q . b = F3(b) ) & ( P2[b] implies q . b = F4(b) ) ) ) assume b in dom q ; ::_thesis: ( ( P1[b] implies q . b = F3(b) ) & ( P2[b] implies q . b = F4(b) ) ) hence ( ( P1[b] implies q . b = F3(b) ) & ( P2[b] implies q . b = F4(b) ) ) by A7; ::_thesis: verum end; scheme :: SCHEME1:sch 7 PartFuncExD29{ F1() -> non empty set , F2() -> non empty set , P1[ set ], P2[ set ], F3( set ) -> Element of F2(), F4( set ) -> Element of F2() } : ex f being PartFunc of F1(),F2() st ( ( for c being Element of F1() holds ( c in dom f iff ( P1[c] or P2[c] ) ) ) & ( for c being Element of F1() st c in dom f holds ( ( P1[c] implies f . c = F3(c) ) & ( P2[c] implies f . c = F4(c) ) ) ) ) provided A1: for c being Element of F1() st P1[c] & P2[c] holds F3(c) = F4(c) proof defpred S1[ set , set ] means ( ( P1[$1] implies $2 = F3($1) ) & ( P2[$1] implies $2 = F4($1) ) ); defpred S2[ set ] means ( P1[$1] or P2[$1] ); consider Y being set such that A2: for x being set holds ( x in Y iff ( x in F1() & S2[x] ) ) from XBOOLE_0:sch_1(); A3: for x being set st x in Y holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in Y implies ex y being set st S1[x,y] ) assume A4: x in Y ; ::_thesis: ex y being set st S1[x,y] then reconsider a9 = x as Element of F1() by A2; now__::_thesis:_ex_y_being_Element_of_F2()_ex_y_being_set_st_S1[x,y] percases ( P1[a9] or P2[a9] ) by A2, A4; supposeA5: P1[a9] ; ::_thesis: ex y being Element of F2() ex y being set st S1[x,y] take y = F3(a9); ::_thesis: ex y being set st S1[x,y] now__::_thesis:_ex_y_being_set_st_S1[x,y] percases ( P2[a9] or not P2[a9] ) ; suppose P2[a9] ; ::_thesis: ex y being set st S1[x,y] then F3(a9) = F4(a9) by A1, A5; hence ex y being set st S1[x,y] ; ::_thesis: verum end; suppose P2[a9] ; ::_thesis: ex y being set st S1[x,y] hence ex y being set st S1[x,y] ; ::_thesis: verum end; end; end; hence ex y being set st S1[x,y] ; ::_thesis: verum end; supposeA6: P2[a9] ; ::_thesis: ex y being Element of F2() ex y being set st S1[x,y] take y = F4(a9); ::_thesis: ex y being set st S1[x,y] now__::_thesis:_ex_y_being_set_st_S1[x,y] percases ( P1[a9] or not P1[a9] ) ; suppose P1[a9] ; ::_thesis: ex y being set st S1[x,y] then F3(a9) = F4(a9) by A1, A6; hence ex y being set st S1[x,y] ; ::_thesis: verum end; suppose P1[a9] ; ::_thesis: ex y being set st S1[x,y] hence ex y being set st S1[x,y] ; ::_thesis: verum end; end; end; hence ex y being set st S1[x,y] ; ::_thesis: verum end; end; end; hence ex y being set st S1[x,y] ; ::_thesis: verum end; consider f being Function such that A7: ( dom f = Y & ( for x being set st x in Y holds S1[x,f . x] ) ) from CLASSES1:sch_1(A3); A8: Y c= F1() proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y or x in F1() ) assume x in Y ; ::_thesis: x in F1() hence x in F1() by A2; ::_thesis: verum end; rng f c= F2() proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in F2() ) assume x in rng f ; ::_thesis: x in F2() then consider y being set such that A9: y in dom f and A10: x = f . y by FUNCT_1:def_3; now__::_thesis:_x_in_F2() percases ( P1[y] or P2[y] ) by A2, A7, A9; suppose P1[y] ; ::_thesis: x in F2() then f . y = F3(y) by A7, A9; hence x in F2() by A10; ::_thesis: verum end; suppose P2[y] ; ::_thesis: x in F2() then f . y = F4(y) by A7, A9; hence x in F2() by A10; ::_thesis: verum end; end; end; hence x in F2() ; ::_thesis: verum end; then reconsider q = f as PartFunc of F1(),F2() by A8, A7, RELSET_1:4; take q ; ::_thesis: ( ( for c being Element of F1() holds ( c in dom q iff ( P1[c] or P2[c] ) ) ) & ( for c being Element of F1() st c in dom q holds ( ( P1[c] implies q . c = F3(c) ) & ( P2[c] implies q . c = F4(c) ) ) ) ) thus for c being Element of F1() holds ( c in dom q iff ( P1[c] or P2[c] ) ) by A2, A7; ::_thesis: for c being Element of F1() st c in dom q holds ( ( P1[c] implies q . c = F3(c) ) & ( P2[c] implies q . c = F4(c) ) ) let e be Element of F1(); ::_thesis: ( e in dom q implies ( ( P1[e] implies q . e = F3(e) ) & ( P2[e] implies q . e = F4(e) ) ) ) assume e in dom q ; ::_thesis: ( ( P1[e] implies q . e = F3(e) ) & ( P2[e] implies q . e = F4(e) ) ) hence ( ( P1[e] implies q . e = F3(e) ) & ( P2[e] implies q . e = F4(e) ) ) by A7; ::_thesis: verum end; scheme :: SCHEME1:sch 8 PartFuncExD299{ F1() -> non empty set , F2() -> non empty set , P1[ set ], F3( set ) -> Element of F2(), F4( set ) -> Element of F2() } : ex f being PartFunc of F1(),F2() st ( f is total & ( for c being Element of F1() st c in dom f holds ( ( P1[c] implies f . c = F3(c) ) & ( P1[c] implies f . c = F4(c) ) ) ) ) proof defpred S1[ set ] means P1[$1]; A1: for c being Element of F1() st P1[c] holds not S1[c] ; consider f being PartFunc of F1(),F2() such that A2: ( ( for c being Element of F1() holds ( c in dom f iff ( P1[c] or S1[c] ) ) ) & ( for c being Element of F1() st c in dom f holds ( ( P1[c] implies f . c = F3(c) ) & ( S1[c] implies f . c = F4(c) ) ) ) ) from SCHEME1:sch_6(A1); take f ; ::_thesis: ( f is total & ( for c being Element of F1() st c in dom f holds ( ( P1[c] implies f . c = F3(c) ) & ( P1[c] implies f . c = F4(c) ) ) ) ) dom f = F1() proof thus dom f c= F1() ; :: according to XBOOLE_0:def_10 ::_thesis: F1() c= dom f let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F1() or x in dom f ) assume x in F1() ; ::_thesis: x in dom f then reconsider b9 = x as Element of F1() ; ( P1[b9] or not P1[b9] ) ; hence x in dom f by A2; ::_thesis: verum end; hence f is total by PARTFUN1:def_2; ::_thesis: for c being Element of F1() st c in dom f holds ( ( P1[c] implies f . c = F3(c) ) & ( P1[c] implies f . c = F4(c) ) ) thus for c being Element of F1() st c in dom f holds ( ( P1[c] implies f . c = F3(c) ) & ( P1[c] implies f . c = F4(c) ) ) by A2; ::_thesis: verum end; scheme :: SCHEME1:sch 9 PartFuncExD3{ F1() -> non empty set , F2() -> non empty set , P1[ set ], P2[ set ], P3[ set ], F3( set ) -> Element of F2(), F4( set ) -> Element of F2(), F5( set ) -> Element of F2() } : ex f being PartFunc of F1(),F2() st ( ( for c being Element of F1() holds ( c in dom f iff ( P1[c] or P2[c] or P3[c] ) ) ) & ( for c being Element of F1() st c in dom f holds ( ( P1[c] implies f . c = F3(c) ) & ( P2[c] implies f . c = F4(c) ) & ( P3[c] implies f . c = F5(c) ) ) ) ) provided A1: for c being Element of F1() holds ( ( P1[c] implies not P2[c] ) & ( P1[c] implies not P3[c] ) & ( P2[c] implies not P3[c] ) ) proof defpred S1[ set , set ] means ( ( P1[$1] implies $2 = F3($1) ) & ( P2[$1] implies $2 = F4($1) ) & ( P3[$1] implies $2 = F5($1) ) ); defpred S2[ set ] means ( P1[$1] or P2[$1] or P3[$1] ); consider Z being set such that A2: for x being set holds ( x in Z iff ( x in F1() & S2[x] ) ) from XBOOLE_0:sch_1(); A3: for x being set st x in Z holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in Z implies ex y being set st S1[x,y] ) assume A4: x in Z ; ::_thesis: ex y being set st S1[x,y] then reconsider c9 = x as Element of F1() by A2; now__::_thesis:_ex_y_being_Element_of_F2()_ex_y_being_set_st_S1[x,y] percases ( P1[x] or P2[x] or P3[x] ) by A2, A4; supposeA5: P1[x] ; ::_thesis: ex y being Element of F2() ex y being set st S1[x,y] take y = F3(x); ::_thesis: ex y being set st S1[x,y] ( P2[c9] & P3[c9] ) by A1, A5; hence ex y being set st S1[x,y] ; ::_thesis: verum end; supposeA6: P2[x] ; ::_thesis: ex y being Element of F2() ex y being set st S1[x,y] take y = F4(x); ::_thesis: ex y being set st S1[x,y] ( P1[c9] & P3[c9] ) by A1, A6; hence ex y being set st S1[x,y] ; ::_thesis: verum end; supposeA7: P3[x] ; ::_thesis: ex y being Element of F2() ex y being set st S1[x,y] take y = F5(x); ::_thesis: ex y being set st S1[x,y] ( P1[c9] & P2[c9] ) by A1, A7; hence ex y being set st S1[x,y] ; ::_thesis: verum end; end; end; hence ex y being set st S1[x,y] ; ::_thesis: verum end; consider f being Function such that A8: ( dom f = Z & ( for x being set st x in Z holds S1[x,f . x] ) ) from CLASSES1:sch_1(A3); A9: rng f c= F2() proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in F2() ) assume x in rng f ; ::_thesis: x in F2() then consider y being set such that A10: y in dom f and A11: x = f . y by FUNCT_1:def_3; now__::_thesis:_x_in_F2() percases ( P1[y] or P2[y] or P3[y] ) by A2, A8, A10; suppose P1[y] ; ::_thesis: x in F2() then f . y = F3(y) by A8, A10; hence x in F2() by A11; ::_thesis: verum end; suppose P2[y] ; ::_thesis: x in F2() then f . y = F4(y) by A8, A10; hence x in F2() by A11; ::_thesis: verum end; suppose P3[y] ; ::_thesis: x in F2() then f . y = F5(y) by A8, A10; hence x in F2() by A11; ::_thesis: verum end; end; end; hence x in F2() ; ::_thesis: verum end; Z c= F1() proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Z or x in F1() ) assume x in Z ; ::_thesis: x in F1() hence x in F1() by A2; ::_thesis: verum end; then reconsider q = f as PartFunc of F1(),F2() by A8, A9, RELSET_1:4; take q ; ::_thesis: ( ( for c being Element of F1() holds ( c in dom q iff ( P1[c] or P2[c] or P3[c] ) ) ) & ( for c being Element of F1() st c in dom q holds ( ( P1[c] implies q . c = F3(c) ) & ( P2[c] implies q . c = F4(c) ) & ( P3[c] implies q . c = F5(c) ) ) ) ) thus for c being Element of F1() holds ( c in dom q iff ( P1[c] or P2[c] or P3[c] ) ) by A2, A8; ::_thesis: for c being Element of F1() st c in dom q holds ( ( P1[c] implies q . c = F3(c) ) & ( P2[c] implies q . c = F4(c) ) & ( P3[c] implies q . c = F5(c) ) ) let g be Element of F1(); ::_thesis: ( g in dom q implies ( ( P1[g] implies q . g = F3(g) ) & ( P2[g] implies q . g = F4(g) ) & ( P3[g] implies q . g = F5(g) ) ) ) assume g in dom q ; ::_thesis: ( ( P1[g] implies q . g = F3(g) ) & ( P2[g] implies q . g = F4(g) ) & ( P3[g] implies q . g = F5(g) ) ) hence ( ( P1[g] implies q . g = F3(g) ) & ( P2[g] implies q . g = F4(g) ) & ( P3[g] implies q . g = F5(g) ) ) by A8; ::_thesis: verum end; scheme :: SCHEME1:sch 10 PartFuncExD39{ F1() -> non empty set , F2() -> non empty set , P1[ set ], P2[ set ], P3[ set ], F3( set ) -> Element of F2(), F4( set ) -> Element of F2(), F5( set ) -> Element of F2() } : ex f being PartFunc of F1(),F2() st ( ( for c being Element of F1() holds ( c in dom f iff ( P1[c] or P2[c] or P3[c] ) ) ) & ( for c being Element of F1() st c in dom f holds ( ( P1[c] implies f . c = F3(c) ) & ( P2[c] implies f . c = F4(c) ) & ( P3[c] implies f . c = F5(c) ) ) ) ) provided A1: for c being Element of F1() holds ( ( P1[c] & P2[c] implies F3(c) = F4(c) ) & ( P1[c] & P3[c] implies F3(c) = F5(c) ) & ( P2[c] & P3[c] implies F4(c) = F5(c) ) ) proof defpred S1[ set , set ] means ( ( P1[$1] implies $2 = F3($1) ) & ( P2[$1] implies $2 = F4($1) ) & ( P3[$1] implies $2 = F5($1) ) ); defpred S2[ set ] means ( P1[$1] or P2[$1] or P3[$1] ); consider V being set such that A2: for x being set holds ( x in V iff ( x in F1() & S2[x] ) ) from XBOOLE_0:sch_1(); A3: for x being set st x in V holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in V implies ex y being set st S1[x,y] ) assume A4: x in V ; ::_thesis: ex y being set st S1[x,y] then reconsider d9 = x as Element of F1() by A2; now__::_thesis:_ex_y_being_Element_of_F2()_ex_y_being_set_st_S1[x,y] percases ( P1[d9] or P2[d9] or P3[d9] ) by A2, A4; supposeA5: P1[d9] ; ::_thesis: ex y being Element of F2() ex y being set st S1[x,y] take y = F3(d9); ::_thesis: ex y being set st S1[x,y] now__::_thesis:_ex_y_being_set_st_S1[x,y] percases ( P2[d9] or not P2[d9] ) ; supposeA6: P2[d9] ; ::_thesis: ex y being set st S1[x,y] then A7: F3(d9) = F4(d9) by A1, A5; now__::_thesis:_ex_y_being_set_st_S1[x,y] percases ( P3[d9] or not P3[d9] ) ; suppose P3[d9] ; ::_thesis: ex y being set st S1[x,y] then F4(d9) = F5(d9) by A1, A6; hence ex y being set st S1[x,y] by A7; ::_thesis: verum end; suppose P3[d9] ; ::_thesis: ex y being set st S1[x,y] hence ex y being set st S1[x,y] by A7; ::_thesis: verum end; end; end; hence ex y being set st S1[x,y] ; ::_thesis: verum end; supposeA8: P2[d9] ; ::_thesis: ex y being set st S1[x,y] now__::_thesis:_ex_y_being_set_st_S1[x,y] percases ( P3[d9] or not P3[d9] ) ; suppose P3[d9] ; ::_thesis: ex y being set st S1[x,y] then F3(d9) = F5(d9) by A1, A5; hence ex y being set st S1[x,y] by A8; ::_thesis: verum end; suppose P3[d9] ; ::_thesis: ex y being set st S1[x,y] hence ex y being set st S1[x,y] by A8; ::_thesis: verum end; end; end; hence ex y being set st S1[x,y] ; ::_thesis: verum end; end; end; hence ex y being set st S1[x,y] ; ::_thesis: verum end; supposeA9: P2[d9] ; ::_thesis: ex y being Element of F2() ex y being set st S1[x,y] take y = F4(x); ::_thesis: ex y being set st S1[x,y] now__::_thesis:_ex_y_being_set_st_S1[x,y] percases ( P1[d9] or not P1[d9] ) ; suppose P1[d9] ; ::_thesis: ex y being set st S1[x,y] then A10: F3(d9) = F4(d9) by A1, A9; now__::_thesis:_ex_y_being_set_st_S1[x,y] percases ( P3[d9] or not P3[d9] ) ; suppose P3[d9] ; ::_thesis: ex y being set st S1[x,y] then F4(d9) = F5(d9) by A1, A9; hence ex y being set st S1[x,y] by A10; ::_thesis: verum end; suppose P3[d9] ; ::_thesis: ex y being set st S1[x,y] hence ex y being set st S1[x,y] by A10; ::_thesis: verum end; end; end; hence ex y being set st S1[x,y] ; ::_thesis: verum end; supposeA11: P1[d9] ; ::_thesis: ex y being set st S1[x,y] now__::_thesis:_ex_y_being_set_st_S1[x,y] percases ( P3[d9] or not P3[d9] ) ; suppose P3[d9] ; ::_thesis: ex y being set st S1[x,y] then F4(d9) = F5(d9) by A1, A9; hence ex y being set st S1[x,y] by A11; ::_thesis: verum end; suppose P3[d9] ; ::_thesis: ex y being set st S1[x,y] hence ex y being set st S1[x,y] by A11; ::_thesis: verum end; end; end; hence ex y being set st S1[x,y] ; ::_thesis: verum end; end; end; hence ex y being set st S1[x,y] ; ::_thesis: verum end; supposeA12: P3[d9] ; ::_thesis: ex y being Element of F2() ex y being set st S1[x,y] take y = F5(x); ::_thesis: ex y being set st S1[x,y] now__::_thesis:_ex_y_being_set_st_S1[x,y] percases ( P1[d9] or not P1[d9] ) ; suppose P1[d9] ; ::_thesis: ex y being set st S1[x,y] then A13: F3(d9) = F5(d9) by A1, A12; now__::_thesis:_ex_y_being_set_st_S1[x,y] percases ( P2[d9] or not P2[d9] ) ; suppose P2[d9] ; ::_thesis: ex y being set st S1[x,y] then F4(d9) = F5(d9) by A1, A12; hence ex y being set st S1[x,y] by A13; ::_thesis: verum end; suppose P2[d9] ; ::_thesis: ex y being set st S1[x,y] hence ex y being set st S1[x,y] by A13; ::_thesis: verum end; end; end; hence ex y being set st S1[x,y] ; ::_thesis: verum end; supposeA14: P1[d9] ; ::_thesis: ex y being set st S1[x,y] now__::_thesis:_ex_y_being_set_st_S1[x,y] percases ( P2[d9] or not P2[d9] ) ; suppose P2[d9] ; ::_thesis: ex y being set st S1[x,y] then F4(d9) = F5(d9) by A1, A12; hence ex y being set st S1[x,y] by A14; ::_thesis: verum end; suppose P2[d9] ; ::_thesis: ex y being set st S1[x,y] hence ex y being set st S1[x,y] by A14; ::_thesis: verum end; end; end; hence ex y being set st S1[x,y] ; ::_thesis: verum end; end; end; hence ex y being set st S1[x,y] ; ::_thesis: verum end; end; end; hence ex y being set st S1[x,y] ; ::_thesis: verum end; consider f being Function such that A15: ( dom f = V & ( for x being set st x in V holds S1[x,f . x] ) ) from CLASSES1:sch_1(A3); A16: rng f c= F2() proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in F2() ) assume x in rng f ; ::_thesis: x in F2() then consider y being set such that A17: y in dom f and A18: x = f . y by FUNCT_1:def_3; now__::_thesis:_x_in_F2() percases ( P1[y] or P2[y] or P3[y] ) by A2, A15, A17; suppose P1[y] ; ::_thesis: x in F2() then f . y = F3(y) by A15, A17; hence x in F2() by A18; ::_thesis: verum end; suppose P2[y] ; ::_thesis: x in F2() then f . y = F4(y) by A15, A17; hence x in F2() by A18; ::_thesis: verum end; suppose P3[y] ; ::_thesis: x in F2() then f . y = F5(y) by A15, A17; hence x in F2() by A18; ::_thesis: verum end; end; end; hence x in F2() ; ::_thesis: verum end; V c= F1() proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in V or x in F1() ) assume x in V ; ::_thesis: x in F1() hence x in F1() by A2; ::_thesis: verum end; then reconsider q = f as PartFunc of F1(),F2() by A15, A16, RELSET_1:4; take q ; ::_thesis: ( ( for c being Element of F1() holds ( c in dom q iff ( P1[c] or P2[c] or P3[c] ) ) ) & ( for c being Element of F1() st c in dom q holds ( ( P1[c] implies q . c = F3(c) ) & ( P2[c] implies q . c = F4(c) ) & ( P3[c] implies q . c = F5(c) ) ) ) ) thus for c being Element of F1() holds ( c in dom q iff ( P1[c] or P2[c] or P3[c] ) ) by A2, A15; ::_thesis: for c being Element of F1() st c in dom q holds ( ( P1[c] implies q . c = F3(c) ) & ( P2[c] implies q . c = F4(c) ) & ( P3[c] implies q . c = F5(c) ) ) let i be Element of F1(); ::_thesis: ( i in dom q implies ( ( P1[i] implies q . i = F3(i) ) & ( P2[i] implies q . i = F4(i) ) & ( P3[i] implies q . i = F5(i) ) ) ) assume i in dom q ; ::_thesis: ( ( P1[i] implies q . i = F3(i) ) & ( P2[i] implies q . i = F4(i) ) & ( P3[i] implies q . i = F5(i) ) ) hence ( ( P1[i] implies q . i = F3(i) ) & ( P2[i] implies q . i = F4(i) ) & ( P3[i] implies q . i = F5(i) ) ) by A15; ::_thesis: verum end; scheme :: SCHEME1:sch 11 PartFuncExD4{ F1() -> non empty set , F2() -> non empty set , P1[ set ], P2[ set ], P3[ set ], P4[ set ], F3( set ) -> Element of F2(), F4( set ) -> Element of F2(), F5( set ) -> Element of F2(), F6( set ) -> Element of F2() } : ex f being PartFunc of F1(),F2() st ( ( for c being Element of F1() holds ( c in dom f iff ( P1[c] or P2[c] or P3[c] or P4[c] ) ) ) & ( for c being Element of F1() st c in dom f holds ( ( P1[c] implies f . c = F3(c) ) & ( P2[c] implies f . c = F4(c) ) & ( P3[c] implies f . c = F5(c) ) & ( P4[c] implies f . c = F6(c) ) ) ) ) provided A1: for c being Element of F1() holds ( ( P1[c] implies not P2[c] ) & ( P1[c] implies not P3[c] ) & ( P1[c] implies not P4[c] ) & ( P2[c] implies not P3[c] ) & ( P2[c] implies not P4[c] ) & ( P3[c] implies not P4[c] ) ) proof defpred S1[ set , set ] means ( ( P1[$1] implies $2 = F3($1) ) & ( P2[$1] implies $2 = F4($1) ) & ( P3[$1] implies $2 = F5($1) ) & ( P4[$1] implies $2 = F6($1) ) ); defpred S2[ set ] means ( P1[$1] or P2[$1] or P3[$1] or P4[$1] ); consider B being set such that A2: for x being set holds ( x in B iff ( x in F1() & S2[x] ) ) from XBOOLE_0:sch_1(); A3: for x being set st x in B holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in B implies ex y being set st S1[x,y] ) assume A4: x in B ; ::_thesis: ex y being set st S1[x,y] then reconsider e9 = x as Element of F1() by A2; now__::_thesis:_ex_y_being_Element_of_F2()_ex_y_being_set_st_S1[x,y] percases ( P1[x] or P2[x] or P3[x] or P4[x] ) by A2, A4; supposeA5: P1[x] ; ::_thesis: ex y being Element of F2() ex y being set st S1[x,y] take y = F3(x); ::_thesis: ex y being set st S1[x,y] A6: P4[e9] by A1, A5; ( P2[e9] & P3[e9] ) by A1, A5; hence ex y being set st S1[x,y] by A6; ::_thesis: verum end; supposeA7: P2[x] ; ::_thesis: ex y being Element of F2() ex y being set st S1[x,y] take y = F4(x); ::_thesis: ex y being set st S1[x,y] A8: P4[e9] by A1, A7; ( P1[e9] & P3[e9] ) by A1, A7; hence ex y being set st S1[x,y] by A8; ::_thesis: verum end; supposeA9: P3[x] ; ::_thesis: ex y being Element of F2() ex y being set st S1[x,y] take y = F5(x); ::_thesis: ex y being set st S1[x,y] A10: P4[e9] by A1, A9; ( P1[e9] & P2[e9] ) by A1, A9; hence ex y being set st S1[x,y] by A10; ::_thesis: verum end; supposeA11: P4[x] ; ::_thesis: ex y being Element of F2() ex y being set st S1[x,y] take y = F6(x); ::_thesis: ex y being set st S1[x,y] A12: P3[e9] by A1, A11; ( P1[e9] & P2[e9] ) by A1, A11; hence ex y being set st S1[x,y] by A12; ::_thesis: verum end; end; end; hence ex y being set st S1[x,y] ; ::_thesis: verum end; consider f being Function such that A13: ( dom f = B & ( for y being set st y in B holds S1[y,f . y] ) ) from CLASSES1:sch_1(A3); A14: rng f c= F2() proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in F2() ) assume x in rng f ; ::_thesis: x in F2() then consider y being set such that A15: y in dom f and A16: x = f . y by FUNCT_1:def_3; now__::_thesis:_x_in_F2() percases ( P1[y] or P2[y] or P3[y] or P4[y] ) by A2, A13, A15; suppose P1[y] ; ::_thesis: x in F2() then f . y = F3(y) by A13, A15; hence x in F2() by A16; ::_thesis: verum end; suppose P2[y] ; ::_thesis: x in F2() then f . y = F4(y) by A13, A15; hence x in F2() by A16; ::_thesis: verum end; suppose P3[y] ; ::_thesis: x in F2() then f . y = F5(y) by A13, A15; hence x in F2() by A16; ::_thesis: verum end; suppose P4[y] ; ::_thesis: x in F2() then f . y = F6(y) by A13, A15; hence x in F2() by A16; ::_thesis: verum end; end; end; hence x in F2() ; ::_thesis: verum end; B c= F1() proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in F1() ) assume x in B ; ::_thesis: x in F1() hence x in F1() by A2; ::_thesis: verum end; then reconsider q = f as PartFunc of F1(),F2() by A13, A14, RELSET_1:4; take q ; ::_thesis: ( ( for c being Element of F1() holds ( c in dom q iff ( P1[c] or P2[c] or P3[c] or P4[c] ) ) ) & ( for c being Element of F1() st c in dom q holds ( ( P1[c] implies q . c = F3(c) ) & ( P2[c] implies q . c = F4(c) ) & ( P3[c] implies q . c = F5(c) ) & ( P4[c] implies q . c = F6(c) ) ) ) ) thus for c being Element of F1() holds ( c in dom q iff ( P1[c] or P2[c] or P3[c] or P4[c] ) ) by A2, A13; ::_thesis: for c being Element of F1() st c in dom q holds ( ( P1[c] implies q . c = F3(c) ) & ( P2[c] implies q . c = F4(c) ) & ( P3[c] implies q . c = F5(c) ) & ( P4[c] implies q . c = F6(c) ) ) let o be Element of F1(); ::_thesis: ( o in dom q implies ( ( P1[o] implies q . o = F3(o) ) & ( P2[o] implies q . o = F4(o) ) & ( P3[o] implies q . o = F5(o) ) & ( P4[o] implies q . o = F6(o) ) ) ) assume o in dom q ; ::_thesis: ( ( P1[o] implies q . o = F3(o) ) & ( P2[o] implies q . o = F4(o) ) & ( P3[o] implies q . o = F5(o) ) & ( P4[o] implies q . o = F6(o) ) ) hence ( ( P1[o] implies q . o = F3(o) ) & ( P2[o] implies q . o = F4(o) ) & ( P3[o] implies q . o = F5(o) ) & ( P4[o] implies q . o = F6(o) ) ) by A13; ::_thesis: verum end; scheme :: SCHEME1:sch 12 PartFuncExS2{ F1() -> set , F2() -> set , P1[ set ], P2[ set ], F3( set ) -> set , F4( set ) -> set } : ex f being PartFunc of F1(),F2() st ( ( for x being set holds ( x in dom f iff ( x in F1() & ( P1[x] or P2[x] ) ) ) ) & ( for x being set st x in dom f holds ( ( P1[x] implies f . x = F3(x) ) & ( P2[x] implies f . x = F4(x) ) ) ) ) provided A1: for x being set st x in F1() & P1[x] holds not P2[x] and A2: for x being set st x in F1() & P1[x] holds F3(x) in F2() and A3: for x being set st x in F1() & P2[x] holds F4(x) in F2() proof defpred S1[ set , set ] means ( ( P1[$1] implies $2 = F3($1) ) & ( P2[$1] implies $2 = F4($1) ) ); defpred S2[ set ] means ( P1[$1] or P2[$1] ); consider A being set such that A4: for x being set holds ( x in A iff ( x in F1() & S2[x] ) ) from XBOOLE_0:sch_1(); A5: for x being set st x in A holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in A implies ex y being set st S1[x,y] ) assume A6: x in A ; ::_thesis: ex y being set st S1[x,y] then A7: x in F1() by A4; now__::_thesis:_ex_y,_y_being_set_st_S1[x,y] percases ( P1[x] or P2[x] ) by A4, A6; supposeA8: P1[x] ; ::_thesis: ex y, y being set st S1[x,y] take y = F3(x); ::_thesis: ex y being set st S1[x,y] P2[x] by A1, A7, A8; hence ex y being set st S1[x,y] ; ::_thesis: verum end; supposeA9: P2[x] ; ::_thesis: ex y, y being set st S1[x,y] take y = F4(x); ::_thesis: ex y being set st S1[x,y] P1[x] by A1, A7, A9; hence ex y being set st S1[x,y] ; ::_thesis: verum end; end; end; hence ex y being set st S1[x,y] ; ::_thesis: verum end; consider f being Function such that A10: ( dom f = A & ( for x being set st x in A holds S1[x,f . x] ) ) from CLASSES1:sch_1(A5); A11: A c= F1() proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in F1() ) assume x in A ; ::_thesis: x in F1() hence x in F1() by A4; ::_thesis: verum end; rng f c= F2() proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in F2() ) assume x in rng f ; ::_thesis: x in F2() then consider y being set such that A12: y in dom f and A13: x = f . y by FUNCT_1:def_3; now__::_thesis:_x_in_F2() percases ( P1[y] or P2[y] ) by A4, A10, A12; supposeA14: P1[y] ; ::_thesis: x in F2() then f . y = F3(y) by A10, A12; hence x in F2() by A2, A11, A10, A12, A13, A14; ::_thesis: verum end; supposeA15: P2[y] ; ::_thesis: x in F2() then f . y = F4(y) by A10, A12; hence x in F2() by A3, A11, A10, A12, A13, A15; ::_thesis: verum end; end; end; hence x in F2() ; ::_thesis: verum end; then reconsider f = f as PartFunc of F1(),F2() by A11, A10, RELSET_1:4; take f ; ::_thesis: ( ( for x being set holds ( x in dom f iff ( x in F1() & ( P1[x] or P2[x] ) ) ) ) & ( for x being set st x in dom f holds ( ( P1[x] implies f . x = F3(x) ) & ( P2[x] implies f . x = F4(x) ) ) ) ) thus for x being set holds ( x in dom f iff ( x in F1() & ( P1[x] or P2[x] ) ) ) by A4, A10; ::_thesis: for x being set st x in dom f holds ( ( P1[x] implies f . x = F3(x) ) & ( P2[x] implies f . x = F4(x) ) ) let x be set ; ::_thesis: ( x in dom f implies ( ( P1[x] implies f . x = F3(x) ) & ( P2[x] implies f . x = F4(x) ) ) ) assume x in dom f ; ::_thesis: ( ( P1[x] implies f . x = F3(x) ) & ( P2[x] implies f . x = F4(x) ) ) hence ( ( P1[x] implies f . x = F3(x) ) & ( P2[x] implies f . x = F4(x) ) ) by A10; ::_thesis: verum end; scheme :: SCHEME1:sch 13 PartFuncExS3{ F1() -> set , F2() -> set , P1[ set ], P2[ set ], P3[ set ], F3( set ) -> set , F4( set ) -> set , F5( set ) -> set } : ex f being PartFunc of F1(),F2() st ( ( for x being set holds ( x in dom f iff ( x in F1() & ( P1[x] or P2[x] or P3[x] ) ) ) ) & ( for x being set st x in dom f holds ( ( P1[x] implies f . x = F3(x) ) & ( P2[x] implies f . x = F4(x) ) & ( P3[x] implies f . x = F5(x) ) ) ) ) provided A1: for x being set st x in F1() holds ( ( P1[x] implies not P2[x] ) & ( P1[x] implies not P3[x] ) & ( P2[x] implies not P3[x] ) ) and A2: for x being set st x in F1() & P1[x] holds F3(x) in F2() and A3: for x being set st x in F1() & P2[x] holds F4(x) in F2() and A4: for x being set st x in F1() & P3[x] holds F5(x) in F2() proof defpred S1[ set , set ] means ( ( P1[$1] implies $2 = F3($1) ) & ( P2[$1] implies $2 = F4($1) ) & ( P3[$1] implies $2 = F5($1) ) ); defpred S2[ set ] means ( P1[$1] or P2[$1] or P3[$1] ); consider S being set such that A5: for x being set holds ( x in S iff ( x in F1() & S2[x] ) ) from XBOOLE_0:sch_1(); A6: for x being set st x in S holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in S implies ex y being set st S1[x,y] ) assume A7: x in S ; ::_thesis: ex y being set st S1[x,y] then A8: x in F1() by A5; now__::_thesis:_ex_y,_y_being_set_st_S1[x,y] percases ( P1[x] or P2[x] or P3[x] ) by A5, A7; supposeA9: P1[x] ; ::_thesis: ex y, y being set st S1[x,y] take y = F3(x); ::_thesis: ex y being set st S1[x,y] ( P2[x] & P3[x] ) by A1, A8, A9; hence ex y being set st S1[x,y] ; ::_thesis: verum end; supposeA10: P2[x] ; ::_thesis: ex y, y being set st S1[x,y] take y = F4(x); ::_thesis: ex y being set st S1[x,y] ( P1[x] & P3[x] ) by A1, A8, A10; hence ex y being set st S1[x,y] ; ::_thesis: verum end; supposeA11: P3[x] ; ::_thesis: ex y, y being set st S1[x,y] take y = F5(x); ::_thesis: ex y being set st S1[x,y] ( P1[x] & P2[x] ) by A1, A8, A11; hence ex y being set st S1[x,y] ; ::_thesis: verum end; end; end; hence ex y being set st S1[x,y] ; ::_thesis: verum end; consider f being Function such that A12: ( dom f = S & ( for x being set st x in S holds S1[x,f . x] ) ) from CLASSES1:sch_1(A6); A13: S c= F1() proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S or x in F1() ) assume x in S ; ::_thesis: x in F1() hence x in F1() by A5; ::_thesis: verum end; rng f c= F2() proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in F2() ) assume x in rng f ; ::_thesis: x in F2() then consider y being set such that A14: y in dom f and A15: x = f . y by FUNCT_1:def_3; now__::_thesis:_x_in_F2() percases ( P1[y] or P2[y] or P3[y] ) by A5, A12, A14; supposeA16: P1[y] ; ::_thesis: x in F2() then f . y = F3(y) by A12, A14; hence x in F2() by A2, A13, A12, A14, A15, A16; ::_thesis: verum end; supposeA17: P2[y] ; ::_thesis: x in F2() then f . y = F4(y) by A12, A14; hence x in F2() by A3, A13, A12, A14, A15, A17; ::_thesis: verum end; supposeA18: P3[y] ; ::_thesis: x in F2() then f . y = F5(y) by A12, A14; hence x in F2() by A4, A13, A12, A14, A15, A18; ::_thesis: verum end; end; end; hence x in F2() ; ::_thesis: verum end; then reconsider f = f as PartFunc of F1(),F2() by A13, A12, RELSET_1:4; take f ; ::_thesis: ( ( for x being set holds ( x in dom f iff ( x in F1() & ( P1[x] or P2[x] or P3[x] ) ) ) ) & ( for x being set st x in dom f holds ( ( P1[x] implies f . x = F3(x) ) & ( P2[x] implies f . x = F4(x) ) & ( P3[x] implies f . x = F5(x) ) ) ) ) thus for x being set holds ( x in dom f iff ( x in F1() & ( P1[x] or P2[x] or P3[x] ) ) ) by A5, A12; ::_thesis: for x being set st x in dom f holds ( ( P1[x] implies f . x = F3(x) ) & ( P2[x] implies f . x = F4(x) ) & ( P3[x] implies f . x = F5(x) ) ) let x be set ; ::_thesis: ( x in dom f implies ( ( P1[x] implies f . x = F3(x) ) & ( P2[x] implies f . x = F4(x) ) & ( P3[x] implies f . x = F5(x) ) ) ) assume x in dom f ; ::_thesis: ( ( P1[x] implies f . x = F3(x) ) & ( P2[x] implies f . x = F4(x) ) & ( P3[x] implies f . x = F5(x) ) ) hence ( ( P1[x] implies f . x = F3(x) ) & ( P2[x] implies f . x = F4(x) ) & ( P3[x] implies f . x = F5(x) ) ) by A12; ::_thesis: verum end; scheme :: SCHEME1:sch 14 PartFuncExS4{ F1() -> set , F2() -> set , P1[ set ], P2[ set ], P3[ set ], P4[ set ], F3( set ) -> set , F4( set ) -> set , F5( set ) -> set , F6( set ) -> set } : ex f being PartFunc of F1(),F2() st ( ( for x being set holds ( x in dom f iff ( x in F1() & ( P1[x] or P2[x] or P3[x] or P4[x] ) ) ) ) & ( for x being set st x in dom f holds ( ( P1[x] implies f . x = F3(x) ) & ( P2[x] implies f . x = F4(x) ) & ( P3[x] implies f . x = F5(x) ) & ( P4[x] implies f . x = F6(x) ) ) ) ) provided A1: for x being set st x in F1() holds ( ( P1[x] implies not P2[x] ) & ( P1[x] implies not P3[x] ) & ( P1[x] implies not P4[x] ) & ( P2[x] implies not P3[x] ) & ( P2[x] implies not P4[x] ) & ( P3[x] implies not P4[x] ) ) and A2: for x being set st x in F1() & P1[x] holds F3(x) in F2() and A3: for x being set st x in F1() & P2[x] holds F4(x) in F2() and A4: for x being set st x in F1() & P3[x] holds F5(x) in F2() and A5: for x being set st x in F1() & P4[x] holds F6(x) in F2() proof defpred S1[ set , set ] means ( ( P1[$1] implies $2 = F3($1) ) & ( P2[$1] implies $2 = F4($1) ) & ( P3[$1] implies $2 = F5($1) ) & ( P4[$1] implies $2 = F6($1) ) ); defpred S2[ set ] means ( P1[$1] or P2[$1] or P3[$1] or P4[$1] ); consider D being set such that A6: for x being set holds ( x in D iff ( x in F1() & S2[x] ) ) from XBOOLE_0:sch_1(); A7: for x being set st x in D holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in D implies ex y being set st S1[x,y] ) assume A8: x in D ; ::_thesis: ex y being set st S1[x,y] then A9: x in F1() by A6; now__::_thesis:_ex_y,_y_being_set_st_S1[x,y] percases ( P1[x] or P2[x] or P3[x] or P4[x] ) by A6, A8; supposeA10: P1[x] ; ::_thesis: ex y, y being set st S1[x,y] take y = F3(x); ::_thesis: ex y being set st S1[x,y] A11: P4[x] by A1, A9, A10; ( P2[x] & P3[x] ) by A1, A9, A10; hence ex y being set st S1[x,y] by A11; ::_thesis: verum end; supposeA12: P2[x] ; ::_thesis: ex y, y being set st S1[x,y] take y = F4(x); ::_thesis: ex y being set st S1[x,y] A13: P4[x] by A1, A9, A12; ( P1[x] & P3[x] ) by A1, A9, A12; hence ex y being set st S1[x,y] by A13; ::_thesis: verum end; supposeA14: P3[x] ; ::_thesis: ex y, y being set st S1[x,y] take y = F5(x); ::_thesis: ex y being set st S1[x,y] A15: P4[x] by A1, A9, A14; ( P1[x] & P2[x] ) by A1, A9, A14; hence ex y being set st S1[x,y] by A15; ::_thesis: verum end; supposeA16: P4[x] ; ::_thesis: ex y, y being set st S1[x,y] take y = F6(x); ::_thesis: ex y being set st S1[x,y] A17: P3[x] by A1, A9, A16; ( P1[x] & P2[x] ) by A1, A9, A16; hence ex y being set st S1[x,y] by A17; ::_thesis: verum end; end; end; hence ex y being set st S1[x,y] ; ::_thesis: verum end; consider f being Function such that A18: ( dom f = D & ( for x being set st x in D holds S1[x,f . x] ) ) from CLASSES1:sch_1(A7); A19: D c= F1() proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D or x in F1() ) assume x in D ; ::_thesis: x in F1() hence x in F1() by A6; ::_thesis: verum end; rng f c= F2() proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in F2() ) assume x in rng f ; ::_thesis: x in F2() then consider y being set such that A20: y in dom f and A21: x = f . y by FUNCT_1:def_3; now__::_thesis:_x_in_F2() percases ( P1[y] or P2[y] or P3[y] or P4[y] ) by A6, A18, A20; supposeA22: P1[y] ; ::_thesis: x in F2() then f . y = F3(y) by A18, A20; hence x in F2() by A2, A19, A18, A20, A21, A22; ::_thesis: verum end; supposeA23: P2[y] ; ::_thesis: x in F2() then f . y = F4(y) by A18, A20; hence x in F2() by A3, A19, A18, A20, A21, A23; ::_thesis: verum end; supposeA24: P3[y] ; ::_thesis: x in F2() then f . y = F5(y) by A18, A20; hence x in F2() by A4, A19, A18, A20, A21, A24; ::_thesis: verum end; supposeA25: P4[y] ; ::_thesis: x in F2() then f . y = F6(y) by A18, A20; hence x in F2() by A5, A19, A18, A20, A21, A25; ::_thesis: verum end; end; end; hence x in F2() ; ::_thesis: verum end; then reconsider f = f as PartFunc of F1(),F2() by A19, A18, RELSET_1:4; take f ; ::_thesis: ( ( for x being set holds ( x in dom f iff ( x in F1() & ( P1[x] or P2[x] or P3[x] or P4[x] ) ) ) ) & ( for x being set st x in dom f holds ( ( P1[x] implies f . x = F3(x) ) & ( P2[x] implies f . x = F4(x) ) & ( P3[x] implies f . x = F5(x) ) & ( P4[x] implies f . x = F6(x) ) ) ) ) thus for x being set holds ( x in dom f iff ( x in F1() & ( P1[x] or P2[x] or P3[x] or P4[x] ) ) ) by A6, A18; ::_thesis: for x being set st x in dom f holds ( ( P1[x] implies f . x = F3(x) ) & ( P2[x] implies f . x = F4(x) ) & ( P3[x] implies f . x = F5(x) ) & ( P4[x] implies f . x = F6(x) ) ) let x be set ; ::_thesis: ( x in dom f implies ( ( P1[x] implies f . x = F3(x) ) & ( P2[x] implies f . x = F4(x) ) & ( P3[x] implies f . x = F5(x) ) & ( P4[x] implies f . x = F6(x) ) ) ) assume x in dom f ; ::_thesis: ( ( P1[x] implies f . x = F3(x) ) & ( P2[x] implies f . x = F4(x) ) & ( P3[x] implies f . x = F5(x) ) & ( P4[x] implies f . x = F6(x) ) ) hence ( ( P1[x] implies f . x = F3(x) ) & ( P2[x] implies f . x = F4(x) ) & ( P3[x] implies f . x = F5(x) ) & ( P4[x] implies f . x = F6(x) ) ) by A18; ::_thesis: verum end; scheme :: SCHEME1:sch 15 PartFuncExCD2{ F1() -> non empty set , F2() -> non empty set , F3() -> non empty set , P1[ set , set ], P2[ set , set ], F4( set , set ) -> Element of F3(), F5( set , set ) -> Element of F3() } : ex f being PartFunc of [:F1(),F2():],F3() st ( ( for c being Element of F1() for d being Element of F2() holds ( [c,d] in dom f iff ( P1[c,d] or P2[c,d] ) ) ) & ( for c being Element of F1() for d being Element of F2() st [c,d] in dom f holds ( ( P1[c,d] implies f . [c,d] = F4(c,d) ) & ( P2[c,d] implies f . [c,d] = F5(c,d) ) ) ) ) provided A1: for c being Element of F1() for d being Element of F2() st P1[c,d] holds not P2[c,d] proof defpred S1[ set , set ] means for c being Element of F1() for t being Element of F2() st $1 = [c,t] holds ( ( P1[c,t] implies $2 = F4(c,t) ) & ( P2[c,t] implies $2 = F5(c,t) ) ); defpred S2[ set ] means for c being Element of F1() for d being Element of F2() holds ( not $1 = [c,d] or P1[c,d] or P2[c,d] ); consider F being set such that A2: for z being set holds ( z in F iff ( z in [:F1(),F2():] & S2[z] ) ) from XBOOLE_0:sch_1(); A3: for x1 being set st x1 in F holds ex z being set st S1[x1,z] proof let x1 be set ; ::_thesis: ( x1 in F implies ex z being set st S1[x1,z] ) assume A4: x1 in F ; ::_thesis: ex z being set st S1[x1,z] then x1 in [:F1(),F2():] by A2; then consider f9, g9 being set such that A5: f9 in F1() and A6: g9 in F2() and A7: x1 = [f9,g9] by ZFMISC_1:def_2; reconsider g9 = g9 as Element of F2() by A6; reconsider f9 = f9 as Element of F1() by A5; now__::_thesis:_ex_z_being_Element_of_F3()_st_ for_p_being_Element_of_F1() for_d_being_Element_of_F2()_st_x1_=_[p,d]_holds_ (_(_P1[p,d]_implies_z_=_F4(p,d)_)_&_(_P2[p,d]_implies_z_=_F5(p,d)_)_) percases ( P1[f9,g9] or P2[f9,g9] ) by A2, A4, A7; supposeA8: P1[f9,g9] ; ::_thesis: ex z being Element of F3() st for p being Element of F1() for d being Element of F2() st x1 = [p,d] holds ( ( P1[p,d] implies z = F4(p,d) ) & ( P2[p,d] implies z = F5(p,d) ) ) take z = F4(f9,g9); ::_thesis: for p being Element of F1() for d being Element of F2() st x1 = [p,d] holds ( ( P1[p,d] implies z = F4(p,d) ) & ( P2[p,d] implies z = F5(p,d) ) ) let p be Element of F1(); ::_thesis: for d being Element of F2() st x1 = [p,d] holds ( ( P1[p,d] implies z = F4(p,d) ) & ( P2[p,d] implies z = F5(p,d) ) ) let d be Element of F2(); ::_thesis: ( x1 = [p,d] implies ( ( P1[p,d] implies z = F4(p,d) ) & ( P2[p,d] implies z = F5(p,d) ) ) ) assume x1 = [p,d] ; ::_thesis: ( ( P1[p,d] implies z = F4(p,d) ) & ( P2[p,d] implies z = F5(p,d) ) ) then ( f9 = p & g9 = d ) by A7, XTUPLE_0:1; hence ( ( P1[p,d] implies z = F4(p,d) ) & ( P2[p,d] implies z = F5(p,d) ) ) by A1, A8; ::_thesis: verum end; supposeA9: P2[f9,g9] ; ::_thesis: ex z being Element of F3() st for r being Element of F1() for d being Element of F2() st x1 = [r,d] holds ( ( P1[r,d] implies z = F4(r,d) ) & ( P2[r,d] implies z = F5(r,d) ) ) take z = F5(f9,g9); ::_thesis: for r being Element of F1() for d being Element of F2() st x1 = [r,d] holds ( ( P1[r,d] implies z = F4(r,d) ) & ( P2[r,d] implies z = F5(r,d) ) ) let r be Element of F1(); ::_thesis: for d being Element of F2() st x1 = [r,d] holds ( ( P1[r,d] implies z = F4(r,d) ) & ( P2[r,d] implies z = F5(r,d) ) ) let d be Element of F2(); ::_thesis: ( x1 = [r,d] implies ( ( P1[r,d] implies z = F4(r,d) ) & ( P2[r,d] implies z = F5(r,d) ) ) ) assume x1 = [r,d] ; ::_thesis: ( ( P1[r,d] implies z = F4(r,d) ) & ( P2[r,d] implies z = F5(r,d) ) ) then ( f9 = r & g9 = d ) by A7, XTUPLE_0:1; hence ( ( P1[r,d] implies z = F4(r,d) ) & ( P2[r,d] implies z = F5(r,d) ) ) by A1, A9; ::_thesis: verum end; end; end; hence ex z being set st S1[x1,z] ; ::_thesis: verum end; consider f being Function such that A10: ( dom f = F & ( for z being set st z in F holds S1[z,f . z] ) ) from CLASSES1:sch_1(A3); A11: rng f c= F3() proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng f or z in F3() ) assume z in rng f ; ::_thesis: z in F3() then consider x1 being set such that A12: x1 in dom f and A13: z = f . x1 by FUNCT_1:def_3; x1 in [:F1(),F2():] by A2, A10, A12; then consider x, y being set such that A14: x in F1() and A15: y in F2() and A16: x1 = [x,y] by ZFMISC_1:def_2; reconsider y = y as Element of F2() by A15; reconsider x = x as Element of F1() by A14; now__::_thesis:_z_in_F3() percases ( P1[x,y] or P2[x,y] ) by A2, A10, A12, A16; suppose P1[x,y] ; ::_thesis: z in F3() then f . [x,y] = F4(x,y) by A10, A12, A16; hence z in F3() by A13, A16; ::_thesis: verum end; suppose P2[x,y] ; ::_thesis: z in F3() then f . [x,y] = F5(x,y) by A10, A12, A16; hence z in F3() by A13, A16; ::_thesis: verum end; end; end; hence z in F3() ; ::_thesis: verum end; F c= [:F1(),F2():] proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in F or z in [:F1(),F2():] ) assume z in F ; ::_thesis: z in [:F1(),F2():] hence z in [:F1(),F2():] by A2; ::_thesis: verum end; then reconsider f = f as PartFunc of [:F1(),F2():],F3() by A10, A11, RELSET_1:4; take f ; ::_thesis: ( ( for c being Element of F1() for d being Element of F2() holds ( [c,d] in dom f iff ( P1[c,d] or P2[c,d] ) ) ) & ( for c being Element of F1() for d being Element of F2() st [c,d] in dom f holds ( ( P1[c,d] implies f . [c,d] = F4(c,d) ) & ( P2[c,d] implies f . [c,d] = F5(c,d) ) ) ) ) thus for c being Element of F1() for h being Element of F2() holds ( [c,h] in dom f iff ( P1[c,h] or P2[c,h] ) ) ::_thesis: for c being Element of F1() for d being Element of F2() st [c,d] in dom f holds ( ( P1[c,d] implies f . [c,d] = F4(c,d) ) & ( P2[c,d] implies f . [c,d] = F5(c,d) ) ) proof let c be Element of F1(); ::_thesis: for h being Element of F2() holds ( [c,h] in dom f iff ( P1[c,h] or P2[c,h] ) ) let g be Element of F2(); ::_thesis: ( [c,g] in dom f iff ( P1[c,g] or P2[c,g] ) ) thus ( not [c,g] in dom f or P1[c,g] or P2[c,g] ) by A2, A10; ::_thesis: ( ( P1[c,g] or P2[c,g] ) implies [c,g] in dom f ) assume A17: ( P1[c,g] or P2[c,g] ) ; ::_thesis: [c,g] in dom f A18: now__::_thesis:_for_h9_being_Element_of_F1() for_j9_being_Element_of_F2()_holds_ (_not_[c,g]_=_[h9,j9]_or_P1[h9,j9]_or_P2[h9,j9]_) let h9 be Element of F1(); ::_thesis: for j9 being Element of F2() holds ( not [c,g] = [h9,j9] or P1[h9,j9] or P2[h9,j9] ) let j9 be Element of F2(); ::_thesis: ( not [c,g] = [h9,j9] or P1[h9,j9] or P2[h9,j9] ) assume A19: [c,g] = [h9,j9] ; ::_thesis: ( P1[h9,j9] or P2[h9,j9] ) then c = h9 by XTUPLE_0:1; hence ( P1[h9,j9] or P2[h9,j9] ) by A17, A19, XTUPLE_0:1; ::_thesis: verum end; [c,g] in [:F1(),F2():] by ZFMISC_1:87; hence [c,g] in dom f by A2, A10, A18; ::_thesis: verum end; let c be Element of F1(); ::_thesis: for d being Element of F2() st [c,d] in dom f holds ( ( P1[c,d] implies f . [c,d] = F4(c,d) ) & ( P2[c,d] implies f . [c,d] = F5(c,d) ) ) let d be Element of F2(); ::_thesis: ( [c,d] in dom f implies ( ( P1[c,d] implies f . [c,d] = F4(c,d) ) & ( P2[c,d] implies f . [c,d] = F5(c,d) ) ) ) assume [c,d] in dom f ; ::_thesis: ( ( P1[c,d] implies f . [c,d] = F4(c,d) ) & ( P2[c,d] implies f . [c,d] = F5(c,d) ) ) hence ( ( P1[c,d] implies f . [c,d] = F4(c,d) ) & ( P2[c,d] implies f . [c,d] = F5(c,d) ) ) by A10; ::_thesis: verum end; scheme :: SCHEME1:sch 16 PartFuncExCD3{ F1() -> non empty set , F2() -> non empty set , F3() -> non empty set , P1[ set , set ], P2[ set , set ], P3[ set , set ], F4( set , set ) -> Element of F3(), F5( set , set ) -> Element of F3(), F6( set , set ) -> Element of F3() } : ex f being PartFunc of [:F1(),F2():],F3() st ( ( for c being Element of F1() for d being Element of F2() holds ( [c,d] in dom f iff ( P1[c,d] or P2[c,d] or P3[c,d] ) ) ) & ( for c being Element of F1() for r being Element of F2() st [c,r] in dom f holds ( ( P1[c,r] implies f . [c,r] = F4(c,r) ) & ( P2[c,r] implies f . [c,r] = F5(c,r) ) & ( P3[c,r] implies f . [c,r] = F6(c,r) ) ) ) ) provided A1: for c being Element of F1() for s being Element of F2() holds ( ( P1[c,s] implies not P2[c,s] ) & ( P1[c,s] implies not P3[c,s] ) & ( P2[c,s] implies not P3[c,s] ) ) proof defpred S1[ set , set ] means for c being Element of F1() for t being Element of F2() st $1 = [c,t] holds ( ( P1[c,t] implies $2 = F4(c,t) ) & ( P2[c,t] implies $2 = F5(c,t) ) & ( P3[c,t] implies $2 = F6(c,t) ) ); defpred S2[ set ] means for c being Element of F1() for d being Element of F2() holds ( not $1 = [c,d] or P1[c,d] or P2[c,d] or P3[c,d] ); consider T being set such that A2: for z being set holds ( z in T iff ( z in [:F1(),F2():] & S2[z] ) ) from XBOOLE_0:sch_1(); A3: for x1 being set st x1 in T holds ex z being set st S1[x1,z] proof let x1 be set ; ::_thesis: ( x1 in T implies ex z being set st S1[x1,z] ) assume A4: x1 in T ; ::_thesis: ex z being set st S1[x1,z] then x1 in [:F1(),F2():] by A2; then consider q9, w9 being set such that A5: q9 in F1() and A6: w9 in F2() and A7: x1 = [q9,w9] by ZFMISC_1:def_2; reconsider w9 = w9 as Element of F2() by A6; reconsider q9 = q9 as Element of F1() by A5; now__::_thesis:_ex_z_being_Element_of_F3()_st_ for_c_being_Element_of_F1() for_d_being_Element_of_F2()_st_x1_=_[c,d]_holds_ (_(_P1[c,d]_implies_z_=_F4(c,d)_)_&_(_P2[c,d]_implies_z_=_F5(c,d)_)_&_(_P3[c,d]_implies_z_=_F6(c,d)_)_) percases ( P1[q9,w9] or P2[q9,w9] or P3[q9,w9] ) by A2, A4, A7; supposeA8: P1[q9,w9] ; ::_thesis: ex z being Element of F3() st for c being Element of F1() for d being Element of F2() st x1 = [c,d] holds ( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) ) take z = F4(q9,w9); ::_thesis: for c being Element of F1() for d being Element of F2() st x1 = [c,d] holds ( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) ) let c be Element of F1(); ::_thesis: for d being Element of F2() st x1 = [c,d] holds ( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) ) let d be Element of F2(); ::_thesis: ( x1 = [c,d] implies ( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) ) ) assume x1 = [c,d] ; ::_thesis: ( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) ) then ( q9 = c & w9 = d ) by A7, XTUPLE_0:1; hence ( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) ) by A1, A8; ::_thesis: verum end; supposeA9: P2[q9,w9] ; ::_thesis: ex z being Element of F3() st for c being Element of F1() for d being Element of F2() st x1 = [c,d] holds ( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) ) take z = F5(q9,w9); ::_thesis: for c being Element of F1() for d being Element of F2() st x1 = [c,d] holds ( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) ) let c be Element of F1(); ::_thesis: for d being Element of F2() st x1 = [c,d] holds ( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) ) let d be Element of F2(); ::_thesis: ( x1 = [c,d] implies ( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) ) ) assume x1 = [c,d] ; ::_thesis: ( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) ) then ( q9 = c & w9 = d ) by A7, XTUPLE_0:1; hence ( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) ) by A1, A9; ::_thesis: verum end; supposeA10: P3[q9,w9] ; ::_thesis: ex z being Element of F3() st for c being Element of F1() for d being Element of F2() st x1 = [c,d] holds ( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) ) take z = F6(q9,w9); ::_thesis: for c being Element of F1() for d being Element of F2() st x1 = [c,d] holds ( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) ) let c be Element of F1(); ::_thesis: for d being Element of F2() st x1 = [c,d] holds ( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) ) let d be Element of F2(); ::_thesis: ( x1 = [c,d] implies ( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) ) ) assume x1 = [c,d] ; ::_thesis: ( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) ) then ( q9 = c & w9 = d ) by A7, XTUPLE_0:1; hence ( ( P1[c,d] implies z = F4(c,d) ) & ( P2[c,d] implies z = F5(c,d) ) & ( P3[c,d] implies z = F6(c,d) ) ) by A1, A10; ::_thesis: verum end; end; end; hence ex z being set st S1[x1,z] ; ::_thesis: verum end; consider f being Function such that A11: ( dom f = T & ( for z being set st z in T holds S1[z,f . z] ) ) from CLASSES1:sch_1(A3); A12: rng f c= F3() proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng f or z in F3() ) assume z in rng f ; ::_thesis: z in F3() then consider x1 being set such that A13: x1 in dom f and A14: z = f . x1 by FUNCT_1:def_3; x1 in [:F1(),F2():] by A2, A11, A13; then consider x, y being set such that A15: x in F1() and A16: y in F2() and A17: x1 = [x,y] by ZFMISC_1:def_2; reconsider y = y as Element of F2() by A16; reconsider x = x as Element of F1() by A15; now__::_thesis:_z_in_F3() percases ( P1[x,y] or P2[x,y] or P3[x,y] ) by A2, A11, A13, A17; suppose P1[x,y] ; ::_thesis: z in F3() then f . [x,y] = F4(x,y) by A11, A13, A17; hence z in F3() by A14, A17; ::_thesis: verum end; suppose P2[x,y] ; ::_thesis: z in F3() then f . [x,y] = F5(x,y) by A11, A13, A17; hence z in F3() by A14, A17; ::_thesis: verum end; suppose P3[x,y] ; ::_thesis: z in F3() then f . [x,y] = F6(x,y) by A11, A13, A17; hence z in F3() by A14, A17; ::_thesis: verum end; end; end; hence z in F3() ; ::_thesis: verum end; T c= [:F1(),F2():] proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in T or z in [:F1(),F2():] ) assume z in T ; ::_thesis: z in [:F1(),F2():] hence z in [:F1(),F2():] by A2; ::_thesis: verum end; then reconsider f = f as PartFunc of [:F1(),F2():],F3() by A11, A12, RELSET_1:4; take f ; ::_thesis: ( ( for c being Element of F1() for d being Element of F2() holds ( [c,d] in dom f iff ( P1[c,d] or P2[c,d] or P3[c,d] ) ) ) & ( for c being Element of F1() for r being Element of F2() st [c,r] in dom f holds ( ( P1[c,r] implies f . [c,r] = F4(c,r) ) & ( P2[c,r] implies f . [c,r] = F5(c,r) ) & ( P3[c,r] implies f . [c,r] = F6(c,r) ) ) ) ) thus for c being Element of F1() for d being Element of F2() holds ( [c,d] in dom f iff ( P1[c,d] or P2[c,d] or P3[c,d] ) ) ::_thesis: for c being Element of F1() for r being Element of F2() st [c,r] in dom f holds ( ( P1[c,r] implies f . [c,r] = F4(c,r) ) & ( P2[c,r] implies f . [c,r] = F5(c,r) ) & ( P3[c,r] implies f . [c,r] = F6(c,r) ) ) proof let c be Element of F1(); ::_thesis: for d being Element of F2() holds ( [c,d] in dom f iff ( P1[c,d] or P2[c,d] or P3[c,d] ) ) let d be Element of F2(); ::_thesis: ( [c,d] in dom f iff ( P1[c,d] or P2[c,d] or P3[c,d] ) ) thus ( not [c,d] in dom f or P1[c,d] or P2[c,d] or P3[c,d] ) by A2, A11; ::_thesis: ( ( P1[c,d] or P2[c,d] or P3[c,d] ) implies [c,d] in dom f ) assume A18: ( P1[c,d] or P2[c,d] or P3[c,d] ) ; ::_thesis: [c,d] in dom f A19: now__::_thesis:_for_i9_being_Element_of_F1() for_o9_being_Element_of_F2()_holds_ (_not_[c,d]_=_[i9,o9]_or_P1[i9,o9]_or_P2[i9,o9]_or_P3[i9,o9]_) let i9 be Element of F1(); ::_thesis: for o9 being Element of F2() holds ( not [c,d] = [i9,o9] or P1[i9,o9] or P2[i9,o9] or P3[i9,o9] ) let o9 be Element of F2(); ::_thesis: ( not [c,d] = [i9,o9] or P1[i9,o9] or P2[i9,o9] or P3[i9,o9] ) assume A20: [c,d] = [i9,o9] ; ::_thesis: ( P1[i9,o9] or P2[i9,o9] or P3[i9,o9] ) then c = i9 by XTUPLE_0:1; hence ( P1[i9,o9] or P2[i9,o9] or P3[i9,o9] ) by A18, A20, XTUPLE_0:1; ::_thesis: verum end; [c,d] in [:F1(),F2():] by ZFMISC_1:87; hence [c,d] in dom f by A2, A11, A19; ::_thesis: verum end; let c be Element of F1(); ::_thesis: for r being Element of F2() st [c,r] in dom f holds ( ( P1[c,r] implies f . [c,r] = F4(c,r) ) & ( P2[c,r] implies f . [c,r] = F5(c,r) ) & ( P3[c,r] implies f . [c,r] = F6(c,r) ) ) let d be Element of F2(); ::_thesis: ( [c,d] in dom f implies ( ( P1[c,d] implies f . [c,d] = F4(c,d) ) & ( P2[c,d] implies f . [c,d] = F5(c,d) ) & ( P3[c,d] implies f . [c,d] = F6(c,d) ) ) ) assume [c,d] in dom f ; ::_thesis: ( ( P1[c,d] implies f . [c,d] = F4(c,d) ) & ( P2[c,d] implies f . [c,d] = F5(c,d) ) & ( P3[c,d] implies f . [c,d] = F6(c,d) ) ) hence ( ( P1[c,d] implies f . [c,d] = F4(c,d) ) & ( P2[c,d] implies f . [c,d] = F5(c,d) ) & ( P3[c,d] implies f . [c,d] = F6(c,d) ) ) by A11; ::_thesis: verum end; scheme :: SCHEME1:sch 17 PartFuncExCS2{ F1() -> set , F2() -> set , F3() -> set , P1[ set , set ], P2[ set , set ], F4( set , set ) -> set , F5( set , set ) -> set } : ex f being PartFunc of [:F1(),F2():],F3() st ( ( for x, y being set holds ( [x,y] in dom f iff ( x in F1() & y in F2() & ( P1[x,y] or P2[x,y] ) ) ) ) & ( for x, y being set st [x,y] in dom f holds ( ( P1[x,y] implies f . [x,y] = F4(x,y) ) & ( P2[x,y] implies f . [x,y] = F5(x,y) ) ) ) ) provided A1: for x, y being set st x in F1() & y in F2() & P1[x,y] holds not P2[x,y] and A2: for x, y being set st x in F1() & y in F2() & P1[x,y] holds F4(x,y) in F3() and A3: for x, y being set st x in F1() & y in F2() & P2[x,y] holds F5(x,y) in F3() proof defpred S1[ set , set ] means for x, y being set st $1 = [x,y] holds ( ( P1[x,y] implies $2 = F4(x,y) ) & ( P2[x,y] implies $2 = F5(x,y) ) ); defpred S2[ set ] means for x, y being set holds ( not $1 = [x,y] or P1[x,y] or P2[x,y] ); consider K being set such that A4: for z being set holds ( z in K iff ( z in [:F1(),F2():] & S2[z] ) ) from XBOOLE_0:sch_1(); A5: for x1 being set st x1 in K holds ex z being set st S1[x1,z] proof let x1 be set ; ::_thesis: ( x1 in K implies ex z being set st S1[x1,z] ) assume A6: x1 in K ; ::_thesis: ex z being set st S1[x1,z] then x1 in [:F1(),F2():] by A4; then consider n9, m9 being set such that A7: ( n9 in F1() & m9 in F2() ) and A8: x1 = [n9,m9] by ZFMISC_1:def_2; now__::_thesis:_ex_z_being_set_st_ for_x,_y_being_set_st_x1_=_[x,y]_holds_ (_(_P1[x,y]_implies_z_=_F4(x,y)_)_&_(_P2[x,y]_implies_z_=_F5(x,y)_)_) percases ( P1[n9,m9] or P2[n9,m9] ) by A4, A6, A8; supposeA9: P1[n9,m9] ; ::_thesis: ex z being set st for x, y being set st x1 = [x,y] holds ( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) ) take z = F4(n9,m9); ::_thesis: for x, y being set st x1 = [x,y] holds ( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) ) let x, y be set ; ::_thesis: ( x1 = [x,y] implies ( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) ) ) assume x1 = [x,y] ; ::_thesis: ( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) ) then ( n9 = x & m9 = y ) by A8, XTUPLE_0:1; hence ( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) ) by A1, A7, A9; ::_thesis: verum end; supposeA10: P2[n9,m9] ; ::_thesis: ex z being set st for x, y being set st x1 = [x,y] holds ( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) ) take z = F5(n9,m9); ::_thesis: for x, y being set st x1 = [x,y] holds ( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) ) let x, y be set ; ::_thesis: ( x1 = [x,y] implies ( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) ) ) assume x1 = [x,y] ; ::_thesis: ( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) ) then ( n9 = x & m9 = y ) by A8, XTUPLE_0:1; hence ( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) ) by A1, A7, A10; ::_thesis: verum end; end; end; hence ex z being set st S1[x1,z] ; ::_thesis: verum end; consider f being Function such that A11: ( dom f = K & ( for z being set st z in K holds S1[z,f . z] ) ) from CLASSES1:sch_1(A5); A12: rng f c= F3() proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng f or z in F3() ) assume z in rng f ; ::_thesis: z in F3() then consider x1 being set such that A13: x1 in dom f and A14: z = f . x1 by FUNCT_1:def_3; x1 in [:F1(),F2():] by A4, A11, A13; then consider x, y being set such that A15: ( x in F1() & y in F2() ) and A16: x1 = [x,y] by ZFMISC_1:def_2; now__::_thesis:_z_in_F3() percases ( P1[x,y] or P2[x,y] ) by A4, A11, A13, A16; supposeA17: P1[x,y] ; ::_thesis: z in F3() then f . [x,y] = F4(x,y) by A11, A13, A16; hence z in F3() by A2, A14, A15, A16, A17; ::_thesis: verum end; supposeA18: P2[x,y] ; ::_thesis: z in F3() then f . [x,y] = F5(x,y) by A11, A13, A16; hence z in F3() by A3, A14, A15, A16, A18; ::_thesis: verum end; end; end; hence z in F3() ; ::_thesis: verum end; K c= [:F1(),F2():] proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in K or z in [:F1(),F2():] ) assume z in K ; ::_thesis: z in [:F1(),F2():] hence z in [:F1(),F2():] by A4; ::_thesis: verum end; then reconsider f = f as PartFunc of [:F1(),F2():],F3() by A11, A12, RELSET_1:4; take f ; ::_thesis: ( ( for x, y being set holds ( [x,y] in dom f iff ( x in F1() & y in F2() & ( P1[x,y] or P2[x,y] ) ) ) ) & ( for x, y being set st [x,y] in dom f holds ( ( P1[x,y] implies f . [x,y] = F4(x,y) ) & ( P2[x,y] implies f . [x,y] = F5(x,y) ) ) ) ) thus for x, y being set holds ( [x,y] in dom f iff ( x in F1() & y in F2() & ( P1[x,y] or P2[x,y] ) ) ) ::_thesis: for x, y being set st [x,y] in dom f holds ( ( P1[x,y] implies f . [x,y] = F4(x,y) ) & ( P2[x,y] implies f . [x,y] = F5(x,y) ) ) proof let x, y be set ; ::_thesis: ( [x,y] in dom f iff ( x in F1() & y in F2() & ( P1[x,y] or P2[x,y] ) ) ) thus ( [x,y] in dom f implies ( x in F1() & y in F2() & ( P1[x,y] or P2[x,y] ) ) ) by A4, A11, ZFMISC_1:87; ::_thesis: ( x in F1() & y in F2() & ( P1[x,y] or P2[x,y] ) implies [x,y] in dom f ) assume that A19: ( x in F1() & y in F2() ) and A20: ( P1[x,y] or P2[x,y] ) ; ::_thesis: [x,y] in dom f A21: now__::_thesis:_for_z9,_q9_being_set_holds_ (_not_[x,y]_=_[z9,q9]_or_P1[z9,q9]_or_P2[z9,q9]_) let z9, q9 be set ; ::_thesis: ( not [x,y] = [z9,q9] or P1[z9,q9] or P2[z9,q9] ) assume A22: [x,y] = [z9,q9] ; ::_thesis: ( P1[z9,q9] or P2[z9,q9] ) then x = z9 by XTUPLE_0:1; hence ( P1[z9,q9] or P2[z9,q9] ) by A20, A22, XTUPLE_0:1; ::_thesis: verum end; [x,y] in [:F1(),F2():] by A19, ZFMISC_1:87; hence [x,y] in dom f by A4, A11, A21; ::_thesis: verum end; let x, y be set ; ::_thesis: ( [x,y] in dom f implies ( ( P1[x,y] implies f . [x,y] = F4(x,y) ) & ( P2[x,y] implies f . [x,y] = F5(x,y) ) ) ) assume [x,y] in dom f ; ::_thesis: ( ( P1[x,y] implies f . [x,y] = F4(x,y) ) & ( P2[x,y] implies f . [x,y] = F5(x,y) ) ) hence ( ( P1[x,y] implies f . [x,y] = F4(x,y) ) & ( P2[x,y] implies f . [x,y] = F5(x,y) ) ) by A11; ::_thesis: verum end; scheme :: SCHEME1:sch 18 PartFuncExCS3{ F1() -> set , F2() -> set , F3() -> set , P1[ set , set ], P2[ set , set ], P3[ set , set ], F4( set , set ) -> set , F5( set , set ) -> set , F6( set , set ) -> set } : ex f being PartFunc of [:F1(),F2():],F3() st ( ( for x, y being set holds ( [x,y] in dom f iff ( x in F1() & y in F2() & ( P1[x,y] or P2[x,y] or P3[x,y] ) ) ) ) & ( for x, y being set st [x,y] in dom f holds ( ( P1[x,y] implies f . [x,y] = F4(x,y) ) & ( P2[x,y] implies f . [x,y] = F5(x,y) ) & ( P3[x,y] implies f . [x,y] = F6(x,y) ) ) ) ) provided A1: for x, y being set st x in F1() & y in F2() holds ( ( P1[x,y] implies not P2[x,y] ) & ( P1[x,y] implies not P3[x,y] ) & ( P2[x,y] implies not P3[x,y] ) ) and A2: for x, y being set st x in F1() & y in F2() & P1[x,y] holds F4(x,y) in F3() and A3: for x, y being set st x in F1() & y in F2() & P2[x,y] holds F5(x,y) in F3() and A4: for x, y being set st x in F1() & y in F2() & P3[x,y] holds F6(x,y) in F3() proof defpred S1[ set , set ] means for x, y being set st $1 = [x,y] holds ( ( P1[x,y] implies $2 = F4(x,y) ) & ( P2[x,y] implies $2 = F5(x,y) ) & ( P3[x,y] implies $2 = F6(x,y) ) ); defpred S2[ set ] means for x, y being set holds ( not $1 = [x,y] or P1[x,y] or P2[x,y] or P3[x,y] ); consider L being set such that A5: for z being set holds ( z in L iff ( z in [:F1(),F2():] & S2[z] ) ) from XBOOLE_0:sch_1(); A6: for x1 being set st x1 in L holds ex z being set st S1[x1,z] proof let x1 be set ; ::_thesis: ( x1 in L implies ex z being set st S1[x1,z] ) assume A7: x1 in L ; ::_thesis: ex z being set st S1[x1,z] then x1 in [:F1(),F2():] by A5; then consider z9, a9 being set such that A8: ( z9 in F1() & a9 in F2() ) and A9: x1 = [z9,a9] by ZFMISC_1:def_2; now__::_thesis:_ex_z_being_set_st_ for_x,_y_being_set_st_x1_=_[x,y]_holds_ (_(_P1[x,y]_implies_z_=_F4(x,y)_)_&_(_P2[x,y]_implies_z_=_F5(x,y)_)_&_(_P3[x,y]_implies_z_=_F6(x,y)_)_) percases ( P1[z9,a9] or P2[z9,a9] or P3[z9,a9] ) by A5, A7, A9; supposeA10: P1[z9,a9] ; ::_thesis: ex z being set st for x, y being set st x1 = [x,y] holds ( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) & ( P3[x,y] implies z = F6(x,y) ) ) take z = F4(z9,a9); ::_thesis: for x, y being set st x1 = [x,y] holds ( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) & ( P3[x,y] implies z = F6(x,y) ) ) let x, y be set ; ::_thesis: ( x1 = [x,y] implies ( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) & ( P3[x,y] implies z = F6(x,y) ) ) ) assume x1 = [x,y] ; ::_thesis: ( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) & ( P3[x,y] implies z = F6(x,y) ) ) then ( z9 = x & a9 = y ) by A9, XTUPLE_0:1; hence ( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) & ( P3[x,y] implies z = F6(x,y) ) ) by A1, A8, A10; ::_thesis: verum end; supposeA11: P2[z9,a9] ; ::_thesis: ex z being set st for x, y being set st x1 = [x,y] holds ( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) & ( P3[x,y] implies z = F6(x,y) ) ) take z = F5(z9,a9); ::_thesis: for x, y being set st x1 = [x,y] holds ( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) & ( P3[x,y] implies z = F6(x,y) ) ) let x, y be set ; ::_thesis: ( x1 = [x,y] implies ( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) & ( P3[x,y] implies z = F6(x,y) ) ) ) assume x1 = [x,y] ; ::_thesis: ( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) & ( P3[x,y] implies z = F6(x,y) ) ) then ( z9 = x & a9 = y ) by A9, XTUPLE_0:1; hence ( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) & ( P3[x,y] implies z = F6(x,y) ) ) by A1, A8, A11; ::_thesis: verum end; supposeA12: P3[z9,a9] ; ::_thesis: ex z being set st for x, y being set st x1 = [x,y] holds ( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) & ( P3[x,y] implies z = F6(x,y) ) ) take z = F6(z9,a9); ::_thesis: for x, y being set st x1 = [x,y] holds ( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) & ( P3[x,y] implies z = F6(x,y) ) ) let x, y be set ; ::_thesis: ( x1 = [x,y] implies ( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) & ( P3[x,y] implies z = F6(x,y) ) ) ) assume x1 = [x,y] ; ::_thesis: ( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) & ( P3[x,y] implies z = F6(x,y) ) ) then ( z9 = x & a9 = y ) by A9, XTUPLE_0:1; hence ( ( P1[x,y] implies z = F4(x,y) ) & ( P2[x,y] implies z = F5(x,y) ) & ( P3[x,y] implies z = F6(x,y) ) ) by A1, A8, A12; ::_thesis: verum end; end; end; hence ex z being set st S1[x1,z] ; ::_thesis: verum end; consider f being Function such that A13: ( dom f = L & ( for z being set st z in L holds S1[z,f . z] ) ) from CLASSES1:sch_1(A6); A14: rng f c= F3() proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng f or z in F3() ) assume z in rng f ; ::_thesis: z in F3() then consider x1 being set such that A15: x1 in dom f and A16: z = f . x1 by FUNCT_1:def_3; x1 in [:F1(),F2():] by A5, A13, A15; then consider x, y being set such that A17: ( x in F1() & y in F2() ) and A18: x1 = [x,y] by ZFMISC_1:def_2; now__::_thesis:_z_in_F3() percases ( P1[x,y] or P2[x,y] or P3[x,y] ) by A5, A13, A15, A18; supposeA19: P1[x,y] ; ::_thesis: z in F3() then f . [x,y] = F4(x,y) by A13, A15, A18; hence z in F3() by A2, A16, A17, A18, A19; ::_thesis: verum end; supposeA20: P2[x,y] ; ::_thesis: z in F3() then f . [x,y] = F5(x,y) by A13, A15, A18; hence z in F3() by A3, A16, A17, A18, A20; ::_thesis: verum end; supposeA21: P3[x,y] ; ::_thesis: z in F3() then f . [x,y] = F6(x,y) by A13, A15, A18; hence z in F3() by A4, A16, A17, A18, A21; ::_thesis: verum end; end; end; hence z in F3() ; ::_thesis: verum end; L c= [:F1(),F2():] proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L or z in [:F1(),F2():] ) assume z in L ; ::_thesis: z in [:F1(),F2():] hence z in [:F1(),F2():] by A5; ::_thesis: verum end; then reconsider f = f as PartFunc of [:F1(),F2():],F3() by A13, A14, RELSET_1:4; take f ; ::_thesis: ( ( for x, y being set holds ( [x,y] in dom f iff ( x in F1() & y in F2() & ( P1[x,y] or P2[x,y] or P3[x,y] ) ) ) ) & ( for x, y being set st [x,y] in dom f holds ( ( P1[x,y] implies f . [x,y] = F4(x,y) ) & ( P2[x,y] implies f . [x,y] = F5(x,y) ) & ( P3[x,y] implies f . [x,y] = F6(x,y) ) ) ) ) thus for x, y being set holds ( [x,y] in dom f iff ( x in F1() & y in F2() & ( P1[x,y] or P2[x,y] or P3[x,y] ) ) ) ::_thesis: for x, y being set st [x,y] in dom f holds ( ( P1[x,y] implies f . [x,y] = F4(x,y) ) & ( P2[x,y] implies f . [x,y] = F5(x,y) ) & ( P3[x,y] implies f . [x,y] = F6(x,y) ) ) proof let x, y be set ; ::_thesis: ( [x,y] in dom f iff ( x in F1() & y in F2() & ( P1[x,y] or P2[x,y] or P3[x,y] ) ) ) thus ( [x,y] in dom f implies ( x in F1() & y in F2() & ( P1[x,y] or P2[x,y] or P3[x,y] ) ) ) by A5, A13, ZFMISC_1:87; ::_thesis: ( x in F1() & y in F2() & ( P1[x,y] or P2[x,y] or P3[x,y] ) implies [x,y] in dom f ) assume that A22: ( x in F1() & y in F2() ) and A23: ( P1[x,y] or P2[x,y] or P3[x,y] ) ; ::_thesis: [x,y] in dom f A24: now__::_thesis:_for_f9,_r9_being_set_holds_ (_not_[x,y]_=_[f9,r9]_or_P1[f9,r9]_or_P2[f9,r9]_or_P3[f9,r9]_) let f9, r9 be set ; ::_thesis: ( not [x,y] = [f9,r9] or P1[f9,r9] or P2[f9,r9] or P3[f9,r9] ) assume A25: [x,y] = [f9,r9] ; ::_thesis: ( P1[f9,r9] or P2[f9,r9] or P3[f9,r9] ) then x = f9 by XTUPLE_0:1; hence ( P1[f9,r9] or P2[f9,r9] or P3[f9,r9] ) by A23, A25, XTUPLE_0:1; ::_thesis: verum end; [x,y] in [:F1(),F2():] by A22, ZFMISC_1:87; hence [x,y] in dom f by A5, A13, A24; ::_thesis: verum end; let x, y be set ; ::_thesis: ( [x,y] in dom f implies ( ( P1[x,y] implies f . [x,y] = F4(x,y) ) & ( P2[x,y] implies f . [x,y] = F5(x,y) ) & ( P3[x,y] implies f . [x,y] = F6(x,y) ) ) ) assume [x,y] in dom f ; ::_thesis: ( ( P1[x,y] implies f . [x,y] = F4(x,y) ) & ( P2[x,y] implies f . [x,y] = F5(x,y) ) & ( P3[x,y] implies f . [x,y] = F6(x,y) ) ) hence ( ( P1[x,y] implies f . [x,y] = F4(x,y) ) & ( P2[x,y] implies f . [x,y] = F5(x,y) ) & ( P3[x,y] implies f . [x,y] = F6(x,y) ) ) by A13; ::_thesis: verum end; scheme :: SCHEME1:sch 19 ExFuncD3{ F1() -> non empty set , F2() -> non empty set , P1[ set ], P2[ set ], P3[ set ], F3( set ) -> Element of F2(), F4( set ) -> Element of F2(), F5( set ) -> Element of F2() } : ex f being Function of F1(),F2() st for c being Element of F1() holds ( ( P1[c] implies f . c = F3(c) ) & ( P2[c] implies f . c = F4(c) ) & ( P3[c] implies f . c = F5(c) ) ) provided A1: for c being Element of F1() holds ( ( P1[c] implies not P2[c] ) & ( P1[c] implies not P3[c] ) & ( P2[c] implies not P3[c] ) ) and A2: for c being Element of F1() holds ( P1[c] or P2[c] or P3[c] ) proof A3: for c being Element of F1() holds ( ( P1[c] implies not P2[c] ) & ( P1[c] implies not P3[c] ) & ( P2[c] implies not P3[c] ) ) by A1; consider f being PartFunc of F1(),F2() such that A4: for w being Element of F1() holds ( w in dom f iff ( P1[w] or P2[w] or P3[w] ) ) and A5: for q being Element of F1() st q in dom f holds ( ( P1[q] implies f . q = F3(q) ) & ( P2[q] implies f . q = F4(q) ) & ( P3[q] implies f . q = F5(q) ) ) from SCHEME1:sch_9(A3); set q = f; A6: dom f = F1() proof thus dom f c= F1() ; :: according to XBOOLE_0:def_10 ::_thesis: F1() c= dom f let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F1() or x in dom f ) assume x in F1() ; ::_thesis: x in dom f then reconsider t9 = x as Element of F1() ; ( P1[t9] or P2[t9] or P3[t9] ) by A2; hence x in dom f by A4; ::_thesis: verum end; then reconsider q = f as Function of F1(),F2() by FUNCT_2:def_1; take q ; ::_thesis: for c being Element of F1() holds ( ( P1[c] implies q . c = F3(c) ) & ( P2[c] implies q . c = F4(c) ) & ( P3[c] implies q . c = F5(c) ) ) let t be Element of F1(); ::_thesis: ( ( P1[t] implies q . t = F3(t) ) & ( P2[t] implies q . t = F4(t) ) & ( P3[t] implies q . t = F5(t) ) ) thus ( ( P1[t] implies q . t = F3(t) ) & ( P2[t] implies q . t = F4(t) ) & ( P3[t] implies q . t = F5(t) ) ) by A5, A6; ::_thesis: verum end; scheme :: SCHEME1:sch 20 ExFuncD4{ F1() -> non empty set , F2() -> non empty set , P1[ set ], P2[ set ], P3[ set ], P4[ set ], F3( set ) -> Element of F2(), F4( set ) -> Element of F2(), F5( set ) -> Element of F2(), F6( set ) -> Element of F2() } : ex f being Function of F1(),F2() st for c being Element of F1() holds ( ( P1[c] implies f . c = F3(c) ) & ( P2[c] implies f . c = F4(c) ) & ( P3[c] implies f . c = F5(c) ) & ( P4[c] implies f . c = F6(c) ) ) provided A1: for c being Element of F1() holds ( ( P1[c] implies not P2[c] ) & ( P1[c] implies not P3[c] ) & ( P1[c] implies not P4[c] ) & ( P2[c] implies not P3[c] ) & ( P2[c] implies not P4[c] ) & ( P3[c] implies not P4[c] ) ) and A2: for c being Element of F1() holds ( P1[c] or P2[c] or P3[c] or P4[c] ) proof A3: for c being Element of F1() holds ( ( P1[c] implies not P2[c] ) & ( P1[c] implies not P3[c] ) & ( P1[c] implies not P4[c] ) & ( P2[c] implies not P3[c] ) & ( P2[c] implies not P4[c] ) & ( P3[c] implies not P4[c] ) ) by A1; consider f being PartFunc of F1(),F2() such that A4: for r being Element of F1() holds ( r in dom f iff ( P1[r] or P2[r] or P3[r] or P4[r] ) ) and A5: for o being Element of F1() st o in dom f holds ( ( P1[o] implies f . o = F3(o) ) & ( P2[o] implies f . o = F4(o) ) & ( P3[o] implies f . o = F5(o) ) & ( P4[o] implies f . o = F6(o) ) ) from SCHEME1:sch_11(A3); set q = f; A6: dom f = F1() proof thus dom f c= F1() ; :: according to XBOOLE_0:def_10 ::_thesis: F1() c= dom f let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F1() or x in dom f ) assume x in F1() ; ::_thesis: x in dom f then reconsider w9 = x as Element of F1() ; ( P1[w9] or P2[w9] or P3[w9] or P4[w9] ) by A2; hence x in dom f by A4; ::_thesis: verum end; then reconsider q = f as Function of F1(),F2() by FUNCT_2:def_1; take q ; ::_thesis: for c being Element of F1() holds ( ( P1[c] implies q . c = F3(c) ) & ( P2[c] implies q . c = F4(c) ) & ( P3[c] implies q . c = F5(c) ) & ( P4[c] implies q . c = F6(c) ) ) let e be Element of F1(); ::_thesis: ( ( P1[e] implies q . e = F3(e) ) & ( P2[e] implies q . e = F4(e) ) & ( P3[e] implies q . e = F5(e) ) & ( P4[e] implies q . e = F6(e) ) ) thus ( ( P1[e] implies q . e = F3(e) ) & ( P2[e] implies q . e = F4(e) ) & ( P3[e] implies q . e = F5(e) ) & ( P4[e] implies q . e = F6(e) ) ) by A5, A6; ::_thesis: verum end; scheme :: SCHEME1:sch 21 FuncExCD2{ F1() -> non empty set , F2() -> non empty set , F3() -> non empty set , P1[ set , set ], F4( set , set ) -> Element of F3(), F5( set , set ) -> Element of F3() } : ex f being Function of [:F1(),F2():],F3() st for c being Element of F1() for d being Element of F2() st [c,d] in dom f holds ( ( P1[c,d] implies f . [c,d] = F4(c,d) ) & ( P1[c,d] implies f . [c,d] = F5(c,d) ) ) proof defpred S1[ set , set ] means P1[$1,$2]; A1: for c being Element of F1() for f being Element of F2() st P1[c,f] holds not S1[c,f] ; consider f being PartFunc of [:F1(),F2():],F3() such that A2: ( ( for c being Element of F1() for e being Element of F2() holds ( [c,e] in dom f iff ( P1[c,e] or S1[c,e] ) ) ) & ( for c being Element of F1() for g being Element of F2() st [c,g] in dom f holds ( ( P1[c,g] implies f . [c,g] = F4(c,g) ) & ( S1[c,g] implies f . [c,g] = F5(c,g) ) ) ) ) from SCHEME1:sch_15(A1); consider g being Function such that A3: g = f ; dom f = [:F1(),F2():] proof thus dom f c= [:F1(),F2():] ; :: according to XBOOLE_0:def_10 ::_thesis: [:F1(),F2():] c= dom f let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [:F1(),F2():] or x in dom f ) assume x in [:F1(),F2():] ; ::_thesis: x in dom f then consider y, z being set such that A4: y in F1() and A5: z in F2() and A6: x = [y,z] by ZFMISC_1:def_2; reconsider z = z as Element of F2() by A5; reconsider y = y as Element of F1() by A4; ( P1[y,z] or not P1[y,z] ) ; hence x in dom f by A2, A6; ::_thesis: verum end; then reconsider g = g as Function of [:F1(),F2():],F3() by A3, FUNCT_2:def_1; take g ; ::_thesis: for c being Element of F1() for d being Element of F2() st [c,d] in dom g holds ( ( P1[c,d] implies g . [c,d] = F4(c,d) ) & ( P1[c,d] implies g . [c,d] = F5(c,d) ) ) thus for c being Element of F1() for d being Element of F2() st [c,d] in dom g holds ( ( P1[c,d] implies g . [c,d] = F4(c,d) ) & ( P1[c,d] implies g . [c,d] = F5(c,d) ) ) by A2, A3; ::_thesis: verum end; scheme :: SCHEME1:sch 22 FuncExCD3{ F1() -> non empty set , F2() -> non empty set , F3() -> non empty set , P1[ set , set ], P2[ set , set ], P3[ set , set ], F4( set , set ) -> Element of F3(), F5( set , set ) -> Element of F3(), F6( set , set ) -> Element of F3() } : ex f being Function of [:F1(),F2():],F3() st ( ( for c being Element of F1() for d being Element of F2() holds ( [c,d] in dom f iff ( P1[c,d] or P2[c,d] or P3[c,d] ) ) ) & ( for c being Element of F1() for d being Element of F2() st [c,d] in dom f holds ( ( P1[c,d] implies f . [c,d] = F4(c,d) ) & ( P2[c,d] implies f . [c,d] = F5(c,d) ) & ( P3[c,d] implies f . [c,d] = F6(c,d) ) ) ) ) provided A1: for c being Element of F1() for d being Element of F2() holds ( ( P1[c,d] implies not P2[c,d] ) & ( P1[c,d] implies not P3[c,d] ) & ( P2[c,d] implies not P3[c,d] ) ) and A2: for c being Element of F1() for d being Element of F2() holds ( P1[c,d] or P2[c,d] or P3[c,d] ) proof A3: for c being Element of F1() for d being Element of F2() holds ( ( P1[c,d] implies not P2[c,d] ) & ( P1[c,d] implies not P3[c,d] ) & ( P2[c,d] implies not P3[c,d] ) ) by A1; consider f being PartFunc of [:F1(),F2():],F3() such that A4: ( ( for c being Element of F1() for b being Element of F2() holds ( [c,b] in dom f iff ( P1[c,b] or P2[c,b] or P3[c,b] ) ) ) & ( for a being Element of F1() for b being Element of F2() st [a,b] in dom f holds ( ( P1[a,b] implies f . [a,b] = F4(a,b) ) & ( P2[a,b] implies f . [a,b] = F5(a,b) ) & ( P3[a,b] implies f . [a,b] = F6(a,b) ) ) ) ) from SCHEME1:sch_16(A3); consider v being Function such that A5: v = f ; dom f = [:F1(),F2():] proof thus dom f c= [:F1(),F2():] ; :: according to XBOOLE_0:def_10 ::_thesis: [:F1(),F2():] c= dom f let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [:F1(),F2():] or x in dom f ) assume x in [:F1(),F2():] ; ::_thesis: x in dom f then consider y, z being set such that A6: y in F1() and A7: z in F2() and A8: x = [y,z] by ZFMISC_1:def_2; reconsider z = z as Element of F2() by A7; reconsider y = y as Element of F1() by A6; ( P1[y,z] or P2[y,z] or P3[y,z] ) by A2; hence x in dom f by A4, A8; ::_thesis: verum end; then reconsider v = v as Function of [:F1(),F2():],F3() by A5, FUNCT_2:def_1; take v ; ::_thesis: ( ( for c being Element of F1() for d being Element of F2() holds ( [c,d] in dom v iff ( P1[c,d] or P2[c,d] or P3[c,d] ) ) ) & ( for c being Element of F1() for d being Element of F2() st [c,d] in dom v holds ( ( P1[c,d] implies v . [c,d] = F4(c,d) ) & ( P2[c,d] implies v . [c,d] = F5(c,d) ) & ( P3[c,d] implies v . [c,d] = F6(c,d) ) ) ) ) thus ( ( for c being Element of F1() for d being Element of F2() holds ( [c,d] in dom v iff ( P1[c,d] or P2[c,d] or P3[c,d] ) ) ) & ( for c being Element of F1() for d being Element of F2() st [c,d] in dom v holds ( ( P1[c,d] implies v . [c,d] = F4(c,d) ) & ( P2[c,d] implies v . [c,d] = F5(c,d) ) & ( P3[c,d] implies v . [c,d] = F6(c,d) ) ) ) ) by A4, A5; ::_thesis: verum end;