:: Schemes of Existence of some Types of Functions
:: by Jaros{\l}aw Kotowicz
::
:: Received September 21, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users


theorem :: SCHEME1:1
for n being Nat ex m being Element of NAT st
( n = 2 * m or n = (2 * m) + 1 )
proof 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 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 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 end;

scheme :: SCHEME1:sch 1
ExRealSubseq{ F1() -> Real_Sequence, P1[ object ] } :
ex q being Real_Sequence st
( q is subsequence of F1() & ( for n being 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 end;

scheme :: SCHEME1:sch 2
ExRealSeq2{ F1( set ) -> Element of REAL , F2( set ) -> Element of 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 end;

scheme :: SCHEME1:sch 3
ExRealSeq3{ F1( set ) -> Element of REAL , F2( set ) -> Element of REAL , F3( set ) -> Element of 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 end;

scheme :: SCHEME1:sch 4
ExRealSeq4{ F1( set ) -> Element of REAL , F2( set ) -> Element of REAL , F3( set ) -> Element of REAL , F4( set ) -> Element of 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 end;

scheme :: SCHEME1:sch 5
ExRealSeq5{ F1( set ) -> Element of REAL , F2( set ) -> Element of REAL , F3( set ) -> Element of REAL , F4( set ) -> Element of REAL , F5( set ) -> Element of 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 end;

scheme :: SCHEME1:sch 6
PartFuncExD2{ F1() -> non empty set , F2() -> non empty set , P1[ object ], P2[ object ], F3( object ) -> Element of F2(), F4( object ) -> 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 end;

scheme :: SCHEME1:sch 7
PartFuncExD29{ F1() -> non empty set , F2() -> non empty set , P1[ object ], P2[ object ], F3( object ) -> Element of F2(), F4( object ) -> 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 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 end;

scheme :: SCHEME1:sch 9
PartFuncExD3{ F1() -> non empty set , F2() -> non empty set , P1[ object ], P2[ object ], P3[ object ], F3( object ) -> Element of F2(), F4( object ) -> Element of F2(), F5( object ) -> 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 end;

scheme :: SCHEME1:sch 10
PartFuncExD39{ F1() -> non empty set , F2() -> non empty set , P1[ object ], P2[ object ], P3[ object ], F3( object ) -> Element of F2(), F4( object ) -> Element of F2(), F5( object ) -> 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 end;

scheme :: SCHEME1:sch 11
PartFuncExD4{ F1() -> non empty set , F2() -> non empty set , P1[ object ], P2[ object ], P3[ object ], P4[ object ], F3( object ) -> Element of F2(), F4( object ) -> Element of F2(), F5( object ) -> Element of F2(), F6( object ) -> 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 end;

scheme :: SCHEME1:sch 12
PartFuncExS2{ F1() -> set , F2() -> set , P1[ object ], P2[ object ], F3( object ) -> set , F4( object ) -> set } :
ex f being PartFunc of F1(),F2() st
( ( for x being object holds
( x in dom f iff ( x in F1() & ( P1[x] or P2[x] ) ) ) ) & ( for x being object 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 object st x in F1() & P1[x] holds
not P2[x] and
A2: for x being object st x in F1() & P1[x] holds
F3(x) in F2() and
A3: for x being object st x in F1() & P2[x] holds
F4(x) in F2()
proof end;

scheme :: SCHEME1:sch 13
PartFuncExS3{ F1() -> set , F2() -> set , P1[ object ], P2[ object ], P3[ object ], F3( object ) -> set , F4( object ) -> set , F5( object ) -> set } :
ex f being PartFunc of F1(),F2() st
( ( for x being object holds
( x in dom f iff ( x in F1() & ( P1[x] or P2[x] or P3[x] ) ) ) ) & ( for x being object 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 object 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 object st x in F1() & P1[x] holds
F3(x) in F2() and
A3: for x being object st x in F1() & P2[x] holds
F4(x) in F2() and
A4: for x being object st x in F1() & P3[x] holds
F5(x) in F2()
proof end;

scheme :: SCHEME1:sch 14
PartFuncExS4{ F1() -> set , F2() -> set , P1[ object ], P2[ object ], P3[ object ], P4[ object ], F3( object ) -> set , F4( object ) -> set , F5( object ) -> set , F6( object ) -> set } :
ex f being PartFunc of F1(),F2() st
( ( for x being object holds
( x in dom f iff ( x in F1() & ( P1[x] or P2[x] or P3[x] or P4[x] ) ) ) ) & ( for x being object 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 object 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 object st x in F1() & P1[x] holds
F3(x) in F2() and
A3: for x being object st x in F1() & P2[x] holds
F4(x) in F2() and
A4: for x being object st x in F1() & P3[x] holds
F5(x) in F2() and
A5: for x being object st x in F1() & P4[x] holds
F6(x) in F2()
proof 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 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 end;

scheme :: SCHEME1:sch 17
PartFuncExCS2{ F1() -> set , F2() -> set , F3() -> set , P1[ object , object ], P2[ object , object ], F4( object , object ) -> object , F5( object , object ) -> object } :
ex f being PartFunc of [:F1(),F2():],F3() st
( ( for x, y being object holds
( [x,y] in dom f iff ( x in F1() & y in F2() & ( P1[x,y] or P2[x,y] ) ) ) ) & ( for x, y being object 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 object st x in F1() & y in F2() & P1[x,y] holds
not P2[x,y] and
A2: for x, y being object st x in F1() & y in F2() & P1[x,y] holds
F4(x,y) in F3() and
A3: for x, y being object st x in F1() & y in F2() & P2[x,y] holds
F5(x,y) in F3()
proof end;

scheme :: SCHEME1:sch 18
PartFuncExCS3{ F1() -> set , F2() -> set , F3() -> set , P1[ object , object ], P2[ object , object ], P3[ object , object ], F4( object , object ) -> object , F5( object , object ) -> object , F6( object , object ) -> object } :
ex f being PartFunc of [:F1(),F2():],F3() st
( ( for x, y being object 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 object 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 object 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 object st x in F1() & y in F2() & P1[x,y] holds
F4(x,y) in F3() and
A3: for x, y being object st x in F1() & y in F2() & P2[x,y] holds
F5(x,y) in F3() and
A4: for x, y being object st x in F1() & y in F2() & P3[x,y] holds
F6(x,y) in F3()
proof 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 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 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 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 end;