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