begin
theorem
canceled;
theorem Th2:
theorem Th3:
scheme
LambdaC{
F1()
-> set ,
P1[
set ],
F2(
set )
-> set ,
F3(
set )
-> set } :
ex
f being
Function st
(
dom f = F1() & ( for
x being
set st
x in F1() holds
( (
P1[
x] implies
f . x = F2(
x) ) & (
P1[
x] implies
f . x = F3(
x) ) ) ) )
Lm1:
dom {} = {}
;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th27:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
scheme
PartFuncEx{
F1()
-> set ,
F2()
-> set ,
P1[
set ,
set ] } :
ex
f being
PartFunc of
F1(),
F2() st
( ( for
x being
set holds
(
x in dom f iff (
x in F1() & ex
y being
set st
P1[
x,
y] ) ) ) & ( for
x being
set st
x in dom f holds
P1[
x,
f . x] ) )
provided
A1:
for
x,
y being
set st
x in F1() &
P1[
x,
y] holds
y in F2()
and A2:
for
x,
y1,
y2 being
set st
x in F1() &
P1[
x,
y1] &
P1[
x,
y2] holds
y1 = y2
scheme
LambdaR{
F1()
-> set ,
F2()
-> set ,
F3(
set )
-> set ,
P1[
set ] } :
ex
f being
PartFunc of
F1(),
F2() st
( ( for
x being
set holds
(
x in dom f iff (
x in F1() &
P1[
x] ) ) ) & ( for
x being
set st
x in dom f holds
f . x = F3(
x) ) )
provided
A1:
for
x being
set st
P1[
x] holds
F3(
x)
in F2()
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th44:
theorem
theorem
theorem Th47:
theorem
canceled;
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th69:
theorem
theorem
theorem
theorem Th73:
theorem
:: deftheorem PARTFUN1:def 1 :
canceled;
:: deftheorem PARTFUN1:def 2 :
canceled;
:: deftheorem defines <: PARTFUN1:def 3 :
theorem
canceled;
theorem Th76:
theorem Th77:
theorem Th78:
theorem Th79:
theorem Th80:
theorem
theorem Th82:
theorem Th83:
theorem
theorem Th85:
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th91:
theorem Th92:
theorem
theorem Th94:
theorem
theorem
canceled;
theorem
:: deftheorem Def4 defines total PARTFUN1:def 4 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th113:
theorem
theorem
theorem
theorem
:: deftheorem Def5 defines PFuncs PARTFUN1:def 5 :
theorem
canceled;
theorem Th119:
theorem Th120:
theorem
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
:: deftheorem Def6 defines tolerates PARTFUN1:def 6 :
theorem
canceled;
theorem Th130:
theorem Th131:
theorem Th132:
theorem
canceled;
theorem
canceled;
theorem
theorem Th136:
theorem
canceled;
theorem
theorem
theorem
theorem Th141:
theorem
theorem
theorem
theorem
theorem Th146:
theorem
theorem Th148:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th158:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th162:
:: deftheorem Def7 defines TotFuncs PARTFUN1:def 7 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th168:
theorem Th169:
theorem
canceled;
theorem Th171:
theorem
canceled;
theorem
canceled;
theorem Th174:
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
begin
Lm3:
for X being set
for R being Relation of X st R = id X holds
R is total
Lm4:
for X being set
for R being Relation st R = id X holds
( R is reflexive & R is symmetric & R is antisymmetric & R is transitive )
Lm5:
for X being set holds id X is Relation of X
begin
theorem Th187:
theorem
:: deftheorem defines /. PARTFUN1:def 8 :