:: PARTFUN1 semantic presentation

theorem Th1: :: PARTFUN1:1

for b₁, b₂, b₃, b₄, b₅, b₆ being set st b₁ c= [:b₂,b₃:] & b₄ c= [:b₅,b₆:] holds
b₁ \/ b₄ c= [:(b₂ \/ b₅),(b₃ \/ b₆):]

proof end;

theorem Th2: :: PARTFUN1:2

for b₁, b₂ being Function st ( for b₃ being set st b₃ in (dom b₁) /\ (dom b₂) holds
b₁ . b₃ = b₂ . b₃ ) holds
ex b₃ being Function st b₁ \/ b₂ = b₃

proof end;

theorem Th3: :: PARTFUN1:3

for b₁, b₂, b₃ being Function st b₁ \/ b₂ = b₃ holds
for b₄ being set st b₄ in (dom b₁) /\ (dom b₂) holds
b₁ . b₄ = b₂ . b₄

proof end;

scheme :: PARTFUN1:sch 1
s1{ F₁() -> set , P₁[ set ], F₂( set ) -> set , F₃( set ) -> set } :

ex b₁ being Function st
( dom b₁ = F₁() & ( for b₂ being set st b₂ in F₁() holds
( ( P₁[b₂] implies b₁ . b₂ = F₂(b₂) ) & ( P₁[b₂] implies b₁ . b₂ = F₃(b₂) ) ) ) )

proof end;

registration

cluster empty set ;
existence

proof end;

end;

Lemma4: dom {} = {}
;

theorem Th4: :: PARTFUN1:4

canceled;

theorem Th5: :: PARTFUN1:5

canceled;

theorem Th6: :: PARTFUN1:6

canceled;

theorem Th7: :: PARTFUN1:7

canceled;

theorem Th8: :: PARTFUN1:8

canceled;

theorem Th9: :: PARTFUN1:9

canceled;

theorem Th10: :: PARTFUN1:10

rng {} = {} ;

E5: now

let c₁, c₂ be set ;
take c₃ = {} ;
thus ( dom c₃ c= c₁ & rng c₃ c= c₂ ) by XBOOLE_1:2;

end;

Lemma6: for b₁, b₂ being set
for b₃ being Relation holds
( b₃ is Relation of b₁,b₂ iff ( dom b₃ c= b₁ & rng b₃ c= b₂ ) )
by RELSET_1:11, RELSET_1:12;

registration

let c₁, c₂ be set ;
cluster Function-like Relation of a₁,a₂;
existence

proof end;

end;

definition

let c₁, c₂ be set ;
mode PartFunc of a₁,a₂ is Function-like Relation of a₁,a₂;

end;

theorem Th11: :: PARTFUN1:11

canceled;

theorem Th12: :: PARTFUN1:12

canceled;

theorem Th13: :: PARTFUN1:13

canceled;

theorem Th14: :: PARTFUN1:14

canceled;

theorem Th15: :: PARTFUN1:15

canceled;

theorem Th16: :: PARTFUN1:16

canceled;

theorem Th17: :: PARTFUN1:17

canceled;

theorem Th18: :: PARTFUN1:18

canceled;

theorem Th19: :: PARTFUN1:19

canceled;

theorem Th20: :: PARTFUN1:20

canceled;

theorem Th21: :: PARTFUN1:21

canceled;

theorem Th22: :: PARTFUN1:22

canceled;

theorem Th23: :: PARTFUN1:23

canceled;

theorem Th24: :: PARTFUN1:24

for b₁ being Function holds b₁ is PartFunc of dom b₁, rng b₁ by Lemma6;

theorem Th25: :: PARTFUN1:25

for b₁ being set
for b₂ being Function st rng b₂ c= b₁ holds
b₂ is PartFunc of dom b₂,b₁ by Lemma6;

theorem Th26: :: PARTFUN1:26

for b₁, b₂, b₃ being set
for b₄ being PartFunc of b₁,b₂ st b₃ in rng b₄ holds
ex b₅ being Element of b₁ st
( b₅ in dom b₄ & b₃ = b₄ . b₅ )

proof end;

theorem Th27: :: PARTFUN1:27

for b₁, b₂, b₃ being set
for b₄ being PartFunc of b₁,b₂ st b₃ in dom b₄ holds
b₄ . b₃ in b₂

proof end;

theorem Th28: :: PARTFUN1:28

for b₁, b₂, b₃ being set
for b₄ being PartFunc of b₁,b₂ st dom b₄ c= b₃ holds
b₄ is PartFunc of b₃,b₂

proof end;

theorem Th29: :: PARTFUN1:29

for b₁, b₂, b₃ being set
for b₄ being PartFunc of b₁,b₂ st rng b₄ c= b₃ holds
b₄ is PartFunc of b₁,b₃

proof end;

theorem Th30: :: PARTFUN1:30

for b₁, b₂, b₃ being set
for b₄ being PartFunc of b₁,b₂ st b₁ c= b₃ holds
b₄ is PartFunc of b₃,b₂

proof end;

theorem Th31: :: PARTFUN1:31

for b₁, b₂, b₃ being set
for b₄ being PartFunc of b₁,b₂ st b₂ c= b₃ holds
b₄ is PartFunc of b₁,b₃

proof end;

theorem Th32: :: PARTFUN1:32

for b₁, b₂, b₃, b₄ being set
for b₅ being PartFunc of b₁,b₂ st b₁ c= b₃ & b₂ c= b₄ holds
b₅ is PartFunc of b₃,b₄

proof end;

theorem Th33: :: PARTFUN1:33

for b₁, b₂ being set
for b₃ being Function
for b₄ being PartFunc of b₁,b₂ st b₃ c= b₄ holds
b₃ is PartFunc of b₁,b₂

proof end;

theorem Th34: :: PARTFUN1:34

for b₁, b₂ being set
for b₃, b₄ being PartFunc of b₁,b₂ st dom b₃ = dom b₄ & ( for b₅ being Element of b₁ st b₅ in dom b₃ holds
b₃ . b₅ = b₄ . b₅ ) holds
b₃ = b₄

proof end;

theorem Th35: :: PARTFUN1:35

for b₁, b₂, b₃ being set
for b₄, b₅ being PartFunc of [:b₁,b₂:],b₃ st dom b₄ = dom b₅ & ( for b₆, b₇ being set st [b₆,b₇] in dom b₄ holds
b₄ . [b₆,b₇] = b₅ . [b₆,b₇] ) holds
b₄ = b₅

proof end;

scheme :: PARTFUN1:sch 2
s2{ F₁() -> set , F₂() -> set , P₁[ set , set ] } :

ex b₁ being PartFunc of F₁(),F₂() st
( ( for b₂ being set holds
( b₂ in dom b₁ iff ( b₂ in F₁() & ex b₃ being set st P₁[b₂,b₃] ) ) ) & ( for b₂ being set st b₂ in dom b₁ holds
P₁[b₂,b₁ . b₂] ) )

provided

E11: for b₁, b₂ being set st b₁ in F₁() & P₁[b₁,b₂] holds
b₂ in F₂() and
E12: for b₁, b₂, b₃ being set st b₁ in F₁() & P₁[b₁,b₂] & P₁[b₁,b₃] holds
b₂ = b₃

proof end;

scheme :: PARTFUN1:sch 3
s3{ F₁() -> set , F₂() -> set , F₃( set ) -> set , P₁[ set ] } :

ex b₁ being PartFunc of F₁(),F₂() st
( ( for b₂ being set holds
( b₂ in dom b₁ iff ( b₂ in F₁() & P₁[b₂] ) ) ) & ( for b₂ being set st b₂ in dom b₁ holds
b₁ . b₂ = F₃(b₂) ) )

provided

E11: for b₁ being set st P₁[b₁] holds
F₃(b₁) in F₂()

proof end;

scheme :: PARTFUN1:sch 4
s4{ F₁() -> set , F₂() -> set , F₃() -> set , P₁[ set , set , set ] } :

ex b₁ being PartFunc of [:F₁(),F₂():],F₃() st
( ( for b₂, b₃ being set holds
( [b₂,b₃] in dom b₁ iff ( b₂ in F₁() & b₃ in F₂() & ex b₄ being set st P₁[b₂,b₃,b₄] ) ) ) & ( for b₂, b₃ being set st [b₂,b₃] in dom b₁ holds
P₁[b₂,b₃,b₁ . [b₂,b₃]] ) )

provided

E11: for b₁, b₂, b₃ being set st b₁ in F₁() & b₂ in F₂() & P₁[b₁,b₂,b₃] holds
b₃ in F₃() and
E12: for b₁, b₂, b₃, b₄ being set st b₁ in F₁() & b₂ in F₂() & P₁[b₁,b₂,b₃] & P₁[b₁,b₂,b₄] holds
b₃ = b₄

proof end;

scheme :: PARTFUN1:sch 5
s5{ F₁() -> set , F₂() -> set , F₃() -> set , F₄( set , set ) -> set , P₁[ set , set ] } :

ex b₁ being PartFunc of [:F₁(),F₂():],F₃() st
( ( for b₂, b₃ being set holds
( [b₂,b₃] in dom b₁ iff ( b₂ in F₁() & b₃ in F₂() & P₁[b₂,b₃] ) ) ) & ( for b₂, b₃ being set st [b₂,b₃] in dom b₁ holds
b₁ . [b₂,b₃] = F₄(b₂,b₃) ) )

provided

E11: for b₁, b₂ being set st P₁[b₁,b₂] holds
F₄(b₁,b₂) in F₃()

proof end;

definition

let c₁, c₂, c₃, c₄ be set ;
let c₅ be PartFunc of c₁,c₂;
let c₆ be PartFunc of c₃,c₄;
redefine func * as c₆ * c₅ -> PartFunc of a₁,a₄;
coherence

proof end;

end;

theorem Th36: :: PARTFUN1:36

for b₁, b₂ being set
for b₃ being Relation of b₁,b₂ holds (id b₁) * b₃ = b₃

proof end;

theorem Th37: :: PARTFUN1:37

for b₁, b₂ being set
for b₃ being Relation of b₁,b₂ holds b₃ * (id b₂) = b₃

proof end;

theorem Th38: :: PARTFUN1:38

for b₁, b₂ being set
for b₃ being PartFunc of b₁,b₂ st ( for b₄, b₅ being Element of b₁ st b₄ in dom b₃ & b₅ in dom b₃ & b₃ . b₄ = b₃ . b₅ holds
b₄ = b₅ ) holds
b₃ is one-to-one

proof end;

theorem Th39: :: PARTFUN1:39

for b₁, b₂ being set
for b₃ being PartFunc of b₁,b₂ st b₃ is one-to-one holds
b₃ " is PartFunc of b₂,b₁

proof end;

theorem Th40: :: PARTFUN1:40

canceled;

theorem Th41: :: PARTFUN1:41

canceled;

theorem Th42: :: PARTFUN1:42

canceled;

theorem Th43: :: PARTFUN1:43

for b₁, b₂, b₃ being set
for b₄ being PartFunc of b₁,b₂ holds b₄ | b₃ is PartFunc of b₃,b₂

proof end;

theorem Th44: :: PARTFUN1:44

for b₁, b₂, b₃ being set
for b₄ being PartFunc of b₁,b₂ holds b₄ | b₃ is PartFunc of b₁,b₂ ;

definition

let c₁, c₂ be set ;
let c₃ be PartFunc of c₁,c₂;
let c₄ be set ;
redefine func | as c₃ | c₄ -> PartFunc of a₁,a₂;
coherence by Th44;

end;

theorem Th45: :: PARTFUN1:45

for b₁, b₂, b₃ being set
for b₄ being PartFunc of b₁,b₂ holds b₃ | b₄ is PartFunc of b₁,b₃

proof end;

theorem Th46: :: PARTFUN1:46

for b₁, b₂, b₃ being set
for b₄ being PartFunc of b₁,b₂ holds b₃ | b₄ is PartFunc of b₁,b₂ ;

theorem Th47: :: PARTFUN1:47

for b₁, b₂ being set
for b₃ being Function holds (b₁ | b₃) | b₂ is PartFunc of b₂,b₁

proof end;

theorem Th48: :: PARTFUN1:48

canceled;

theorem Th49: :: PARTFUN1:49

for b₁, b₂, b₃ being set
for b₄ being PartFunc of b₁,b₂ st b₃ in b₄ .: b₁ holds
ex b₅ being Element of b₁ st
( b₅ in dom b₄ & b₃ = b₄ . b₅ )

proof end;

theorem Th50: :: PARTFUN1:50

canceled;

theorem Th51: :: PARTFUN1:51

for b₁, b₂ being set
for b₃ being PartFunc of b₁,b₂ holds b₃ .: b₁ = rng b₃

proof end;

theorem Th52: :: PARTFUN1:52

canceled;

theorem Th53: :: PARTFUN1:53

for b₁, b₂ being set
for b₃ being PartFunc of b₁,b₂ holds b₃ " b₂ = dom b₃

proof end;

theorem Th54: :: PARTFUN1:54

for b₁ being set
for b₂ being PartFunc of {} ,b₁ holds
( dom b₂ = {} & rng b₂ = {} )

proof end;

theorem Th55: :: PARTFUN1:55

for b₁, b₂ being set
for b₃ being Function st dom b₃ = {} holds
b₃ is PartFunc of b₁,b₂

proof end;

theorem Th56: :: PARTFUN1:56

for b₁, b₂ being set holds {} is PartFunc of b₁,b₂ by Lemma4, Th55;

theorem Th57: :: PARTFUN1:57

for b₁ being set
for b₂ being PartFunc of {} ,b₁ holds b₂ = {}

proof end;

theorem Th58: :: PARTFUN1:58

for b₁, b₂ being set
for b₃ being PartFunc of {} ,b₁
for b₄ being PartFunc of {} ,b₂ holds b₃ = b₄

proof end;

theorem Th59: :: PARTFUN1:59

for b₁ being set
for b₂ being PartFunc of {} ,b₁ holds b₂ is one-to-one by Th57;

theorem Th60: :: PARTFUN1:60

for b₁, b₂ being set
for b₃ being PartFunc of {} ,b₁ holds b₃ .: b₂ = {}

proof end;

theorem Th61: :: PARTFUN1:61

for b₁, b₂ being set
for b₃ being PartFunc of {} ,b₁ holds b₃ " b₂ = {}

proof end;

theorem Th62: :: PARTFUN1:62

for b₁ being set
for b₂ being PartFunc of b₁, {} holds
( dom b₂ = {} & rng b₂ = {} )

proof end;

theorem Th63: :: PARTFUN1:63

for b₁, b₂ being set
for b₃ being Function st rng b₃ = {} holds
b₃ is PartFunc of b₁,b₂

proof end;

theorem Th64: :: PARTFUN1:64

for b₁ being set
for b₂ being PartFunc of b₁, {} holds b₂ = {}

proof end;

theorem Th65: :: PARTFUN1:65

for b₁, b₂ being set
for b₃ being PartFunc of b₁, {}
for b₄ being PartFunc of b₂, {} holds b₃ = b₄

proof end;

theorem Th66: :: PARTFUN1:66

for b₁ being set
for b₂ being PartFunc of b₁, {} holds b₂ is one-to-one by Th64;

theorem Th67: :: PARTFUN1:67

for b₁, b₂ being set
for b₃ being PartFunc of b₁, {} holds b₃ .: b₂ = {}

proof end;

theorem Th68: :: PARTFUN1:68

for b₁, b₂ being set
for b₃ being PartFunc of b₁, {} holds b₃ " b₂ = {}

proof end;

theorem Th69: :: PARTFUN1:69

for b₁, b₂ being set
for b₃ being PartFunc of {b₁},b₂ holds rng b₃ c= {(b₃ . b₁)}

proof end;

theorem Th70: :: PARTFUN1:70

for b₁, b₂ being set
for b₃ being PartFunc of {b₁},b₂ holds b₃ is one-to-one

proof end;

theorem Th71: :: PARTFUN1:71

for b₁, b₂, b₃ being set
for b₄ being PartFunc of {b₁},b₂ holds b₄ .: b₃ c= {(b₄ . b₁)}

proof end;

theorem Th72: :: PARTFUN1:72

for b₁, b₂, b₃ being set
for b₄ being Function st dom b₄ = {b₁} & b₁ in b₂ & b₄ . b₁ in b₃ holds
b₄ is PartFunc of b₂,b₃

proof end;

theorem Th73: :: PARTFUN1:73

for b₁, b₂, b₃ being set
for b₄ being PartFunc of b₁,{b₂} st b₃ in dom b₄ holds
b₄ . b₃ = b₂

proof end;

theorem Th74: :: PARTFUN1:74

for b₁, b₂ being set
for b₃, b₄ being PartFunc of b₁,{b₂} st dom b₃ = dom b₄ holds
b₃ = b₄

proof end;

definition

let c₁ be Function;
let c₂, c₃ be set ;
canceled;
canceled;
func <:c₁,c₂,c₃:> -> PartFunc of a₂,a₃ equals :: PARTFUN1:def 3
(a₃ | a₁) | a₂;
coherence by Th47;

end;

:: deftheorem Def1 PARTFUN1:def 1 :

:: deftheorem Def2 PARTFUN1:def 2 :

:: deftheorem Def3 defines <: PARTFUN1:def 3 :

theorem Th75: :: PARTFUN1:75

canceled;

theorem Th76: :: PARTFUN1:76

for b₁, b₂ being set
for b₃ being Function holds <:b₃,b₁,b₂:> c= b₃

proof end;

theorem Th77: :: PARTFUN1:77

for b₁, b₂ being set
for b₃ being Function holds
( dom <:b₃,b₁,b₂:> c= dom b₃ & rng <:b₃,b₁,b₂:> c= rng b₃ )

proof end;

theorem Th78: :: PARTFUN1:78

for b₁, b₂, b₃ being set
for b₄ being Function holds
( b₁ in dom <:b₄,b₂,b₃:> iff ( b₁ in dom b₄ & b₁ in b₂ & b₄ . b₁ in b₃ ) )

proof end;

theorem Th79: :: PARTFUN1:79

for b₁, b₂, b₃ being set
for b₄ being Function st b₁ in dom b₄ & b₁ in b₂ & b₄ . b₁ in b₃ holds
<:b₄,b₂,b₃:> . b₁ = b₄ . b₁

proof end;

theorem Th80: :: PARTFUN1:80

for b₁, b₂, b₃ being set
for b₄ being Function st b₁ in dom <:b₄,b₂,b₃:> holds
<:b₄,b₂,b₃:> . b₁ = b₄ . b₁

proof end;

theorem Th81: :: PARTFUN1:81

for b₁, b₂ being set
for b₃, b₄ being Function st b₃ c= b₄ holds
<:b₃,b₁,b₂:> c= <:b₄,b₁,b₂:>

proof end;

theorem Th82: :: PARTFUN1:82

for b₁, b₂, b₃ being set
for b₄ being Function st b₁ c= b₂ holds
<:b₄,b₁,b₃:> c= <:b₄,b₂,b₃:>

proof end;

theorem Th83: :: PARTFUN1:83

for b₁, b₂, b₃ being set
for b₄ being Function st b₁ c= b₂ holds
<:b₄,b₃,b₁:> c= <:b₄,b₃,b₂:>

proof end;

theorem Th84: :: PARTFUN1:84

for b₁, b₂, b₃, b₄ being set
for b₅ being Function st b₁ c= b₂ & b₃ c= b₄ holds
<:b₅,b₁,b₃:> c= <:b₅,b₂,b₄:>

proof end;

theorem Th85: :: PARTFUN1:85

for b₁, b₂ being set
for b₃ being Function st dom b₃ c= b₁ & rng b₃ c= b₂ holds
b₃ = <:b₃,b₁,b₂:>

proof end;

theorem Th86: :: PARTFUN1:86

for b₁ being Function holds b₁ = <:b₁,(dom b₁),(rng b₁):> by Th85;

theorem Th87: :: PARTFUN1:87

for b₁, b₂ being set
for b₃ being PartFunc of b₁,b₂ holds <:b₃,b₁,b₂:> = b₃

proof end;

theorem Th88: :: PARTFUN1:88

canceled;

theorem Th89: :: PARTFUN1:89

canceled;

theorem Th90: :: PARTFUN1:90

canceled;

theorem Th91: :: PARTFUN1:91

for b₁, b₂ being set holds <:{} ,b₁,b₂:> = {}

proof end;

theorem Th92: :: PARTFUN1:92

for b₁, b₂, b₃ being set
for b₄, b₅ being Function holds <:b₅,b₁,b₂:> * <:b₄,b₃,b₁:> c= <:(b₅ * b₄),b₃,b₂:>

proof end;

theorem Th93: :: PARTFUN1:93

for b₁, b₂, b₃ being set
for b₄, b₅ being Function st (rng b₄) /\ (dom b₅) c= b₁ holds
<:b₅,b₁,b₂:> * <:b₄,b₃,b₁:> = <:(b₅ * b₄),b₃,b₂:>

proof end;

theorem Th94: :: PARTFUN1:94

for b₁, b₂ being set
for b₃ being Function st b₃ is one-to-one holds
<:b₃,b₁,b₂:> is one-to-one

proof end;

theorem Th95: :: PARTFUN1:95

for b₁, b₂ being set
for b₃ being Function st b₃ is one-to-one holds
<:b₃,b₁,b₂:> " = <:(b₃ " ),b₂,b₁:>

proof end;

theorem Th96: :: PARTFUN1:96

for b₁, b₂, b₃ being set
for b₄ being Function holds <:b₄,b₁,b₂:> | b₃ = <:b₄,(b₁ /\ b₃),b₂:> by RELAT_1:100;

theorem Th97: :: PARTFUN1:97

for b₁, b₂, b₃ being set
for b₄ being Function holds b₁ | <:b₄,b₂,b₃:> = <:b₄,b₂,(b₁ /\ b₃):>

proof end;

definition

let c₁, c₂ be set ;
let c₃ be Relation of c₁,c₂;
attr a₃ is total means :Def4: :: PARTFUN1:def 4
dom a₃ = a₁;

end;

:: deftheorem Def4 defines total PARTFUN1:def 4 :

theorem Th98: :: PARTFUN1:98

canceled;

theorem Th99: :: PARTFUN1:99

for b₁, b₂ being set
for b₃ being PartFunc of b₁,b₂ st b₃ is total & b₂ = {} holds
b₁ = {}

proof end;

theorem Th100: :: PARTFUN1:100

canceled;

theorem Th101: :: PARTFUN1:101

canceled;

theorem Th102: :: PARTFUN1:102

canceled;

theorem Th103: :: PARTFUN1:103

canceled;

theorem Th104: :: PARTFUN1:104

canceled;

theorem Th105: :: PARTFUN1:105

canceled;

theorem Th106: :: PARTFUN1:106

canceled;

theorem Th107: :: PARTFUN1:107

canceled;

theorem Th108: :: PARTFUN1:108

canceled;

theorem Th109: :: PARTFUN1:109

canceled;

theorem Th110: :: PARTFUN1:110

canceled;

theorem Th111: :: PARTFUN1:111

canceled;

theorem Th112: :: PARTFUN1:112

for b₁ being set
for b₂ being PartFunc of {} ,b₁ holds b₂ is total

proof end;

theorem Th113: :: PARTFUN1:113

for b₁, b₂ being set
for b₃ being Function st <:b₃,b₁,b₂:> is total holds
b₁ c= dom b₃

proof end;

theorem Th114: :: PARTFUN1:114

for b₁, b₂ being set st <:{} ,b₁,b₂:> is total holds
b₁ = {}

proof end;

theorem Th115: :: PARTFUN1:115

for b₁, b₂ being set
for b₃ being Function st b₁ c= dom b₃ & rng b₃ c= b₂ holds
<:b₃,b₁,b₂:> is total

proof end;

theorem Th116: :: PARTFUN1:116

for b₁, b₂ being set
for b₃ being Function st <:b₃,b₁,b₂:> is total holds
b₃ .: b₁ c= b₂

proof end;

theorem Th117: :: PARTFUN1:117

for b₁, b₂ being set
for b₃ being Function st b₁ c= dom b₃ & b₃ .: b₁ c= b₂ holds
<:b₃,b₁,b₂:> is total

proof end;

definition

let c₁, c₂ be set ;
func PFuncs c₁,c₂ -> set means :Def5: :: PARTFUN1:def 5
for b₁ being set holds
( b₁ in a₃ iff ex b₂ being Function st
( b₁ = b₂ & dom b₂ c= a₁ & rng b₂ c= a₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines PFuncs PARTFUN1:def 5 :

registration

let c₁, c₂ be set ;
cluster PFuncs a₁,a₂ -> non empty ;
coherence

proof end;

end;

theorem Th118: :: PARTFUN1:118

canceled;

theorem Th119: :: PARTFUN1:119

for b₁, b₂ being set
for b₃ being PartFunc of b₁,b₂ holds b₃ in PFuncs b₁,b₂

proof end;

theorem Th120: :: PARTFUN1:120

for b₁, b₂, b₃ being set st b₃ in PFuncs b₁,b₂ holds
b₃ is PartFunc of b₁,b₂

proof end;

theorem Th121: :: PARTFUN1:121

for b₁, b₂ being set
for b₃ being Element of PFuncs b₁,b₂ holds b₃ is PartFunc of b₁,b₂ by Th120;

theorem Th122: :: PARTFUN1:122

for b₁ being set holds PFuncs {} ,b₁ = {{} }

proof end;

theorem Th123: :: PARTFUN1:123

for b₁ being set holds PFuncs b₁,{} = {{} }

proof end;

theorem Th124: :: PARTFUN1:124

canceled;

theorem Th125: :: PARTFUN1:125

for b₁, b₂, b₃ being set st b₁ c= b₂ holds
PFuncs b₁,b₃ c= PFuncs b₂,b₃

proof end;

theorem Th126: :: PARTFUN1:126

for b₁, b₂ being set holds PFuncs {} ,b₁ c= PFuncs b₂,b₁

proof end;

theorem Th127: :: PARTFUN1:127

for b₁, b₂, b₃ being set st b₁ c= b₂ holds
PFuncs b₃,b₁ c= PFuncs b₃,b₂

proof end;

theorem Th128: :: PARTFUN1:128

for b₁, b₂, b₃, b₄ being set st b₁ c= b₂ & b₃ c= b₄ holds
PFuncs b₁,b₃ c= PFuncs b₂,b₄

proof end;

definition

let c₁, c₂ be Function;
pred c₁ tolerates c₂ means :Def6: :: PARTFUN1:def 6
for b₁ being set st b₁ in (dom a₁) /\ (dom a₂) holds
a₁ . b₁ = a₂ . b₁;
reflexivity ;
symmetry ;

end;

:: deftheorem Def6 defines tolerates PARTFUN1:def 6 :

theorem Th129: :: PARTFUN1:129

canceled;

theorem Th130: :: PARTFUN1:130

for b₁, b₂ being Function holds
( b₁ tolerates b₂ iff ex b₃ being Function st b₁ \/ b₂ = b₃ )

proof end;

theorem Th131: :: PARTFUN1:131

for b₁, b₂ being Function holds
( b₁ tolerates b₂ iff ex b₃ being Function st
( b₁ c= b₃ & b₂ c= b₃ ) )

proof end;

theorem Th132: :: PARTFUN1:132

for b₁, b₂ being Function st dom b₁ c= dom b₂ holds
( b₁ tolerates b₂ iff for b₃ being set st b₃ in dom b₁ holds
b₁ . b₃ = b₂ . b₃ )

proof end;

theorem Th133: :: PARTFUN1:133

canceled;

theorem Th134: :: PARTFUN1:134

canceled;

theorem Th135: :: PARTFUN1:135

for b₁, b₂ being Function st b₁ c= b₂ holds
b₁ tolerates b₂ by Th131;

theorem Th136: :: PARTFUN1:136

for b₁, b₂ being Function st dom b₁ = dom b₂ & b₁ tolerates b₂ holds
b₁ = b₂

proof end;

theorem Th137: :: PARTFUN1:137

canceled;

theorem Th138: :: PARTFUN1:138

for b₁, b₂ being Function st dom b₁ misses dom b₂ holds
b₁ tolerates b₂

proof end;

theorem Th139: :: PARTFUN1:139

for b₁, b₂, b₃ being Function st b₁ c= b₃ & b₂ c= b₃ holds
b₁ tolerates b₂ by Th131;

theorem Th140: :: PARTFUN1:140

for b₁, b₂ being set
for b₃, b₄ being PartFunc of b₁,b₂
for b₅ being Function st b₃ tolerates b₅ & b₄ c= b₃ holds
b₄ tolerates b₅

proof end;

theorem Th141: :: PARTFUN1:141

for b₁ being Function holds {} tolerates b₁

proof end;

theorem Th142: :: PARTFUN1:142

for b₁, b₂ being set
for b₃ being Function holds <:{} ,b₁,b₂:> tolerates b₃

proof end;

theorem Th143: :: PARTFUN1:143

for b₁, b₂ being set
for b₃, b₄ being PartFunc of b₁,{b₂} holds b₃ tolerates b₄

proof end;

theorem Th144: :: PARTFUN1:144

for b₁ being set
for b₂ being Function holds b₂ | b₁ tolerates b₂

proof end;

theorem Th145: :: PARTFUN1:145

for b₁ being set
for b₂ being Function holds b₁ | b₂ tolerates b₂

proof end;

theorem Th146: :: PARTFUN1:146

for b₁, b₂ being set
for b₃ being Function holds (b₁ | b₃) | b₂ tolerates b₃

proof end;

theorem Th147: :: PARTFUN1:147

for b₁, b₂ being set
for b₃ being Function holds <:b₃,b₁,b₂:> tolerates b₃ by Th146;

theorem Th148: :: PARTFUN1:148

for b₁, b₂ being set
for b₃, b₄ being PartFunc of b₁,b₂ st b₃ is total & b₄ is total & b₃ tolerates b₄ holds
b₃ = b₄

proof end;

theorem Th149: :: PARTFUN1:149

canceled;

theorem Th150: :: PARTFUN1:150

canceled;

theorem Th151: :: PARTFUN1:151

canceled;

theorem Th152: :: PARTFUN1:152

canceled;

theorem Th153: :: PARTFUN1:153

canceled;

theorem Th154: :: PARTFUN1:154

canceled;

theorem Th155: :: PARTFUN1:155

canceled;

theorem Th156: :: PARTFUN1:156

canceled;

theorem Th157: :: PARTFUN1:157

canceled;

theorem Th158: :: PARTFUN1:158

for b₁, b₂ being set
for b₃, b₄, b₅ being PartFunc of b₁,b₂ st b₃ tolerates b₅ & b₄ tolerates b₅ & b₅ is total holds
b₃ tolerates b₄

proof end;

theorem Th159: :: PARTFUN1:159

canceled;

theorem Th160: :: PARTFUN1:160

canceled;

theorem Th161: :: PARTFUN1:161

canceled;

theorem Th162: :: PARTFUN1:162

for b₁, b₂ being set
for b₃, b₄ being PartFunc of b₁,b₂ st ( b₂ = {} implies b₁ = {} ) & b₃ tolerates b₄ holds
ex b₅ being PartFunc of b₁,b₂ st
( b₅ is total & b₃ tolerates b₅ & b₄ tolerates b₅ )

proof end;

definition

let c₁, c₂ be set ;
let c₃ be PartFunc of c₁,c₂;
func TotFuncs c₃ -> set means :Def7: :: PARTFUN1:def 7
for b₁ being set holds
( b₁ in a₄ iff ex b₂ being PartFunc of a₁,a₂ st
( b₂ = b₁ & b₂ is total & a₃ tolerates b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines TotFuncs PARTFUN1:def 7 :

theorem Th163: :: PARTFUN1:163

canceled;

theorem Th164: :: PARTFUN1:164

canceled;

theorem Th165: :: PARTFUN1:165

canceled;

theorem Th166: :: PARTFUN1:166

canceled;

theorem Th167: :: PARTFUN1:167

canceled;

theorem Th168: :: PARTFUN1:168

for b₁, b₂ being set
for b₃ being PartFunc of b₁,b₂
for b₄ being set st b₄ in TotFuncs b₃ holds
b₄ is PartFunc of b₁,b₂

proof end;

theorem Th169: :: PARTFUN1:169

for b₁, b₂ being set
for b₃, b₄ being PartFunc of b₁,b₂ st b₄ in TotFuncs b₃ holds
b₄ is total

proof end;

theorem Th170: :: PARTFUN1:170

canceled;

theorem Th171: :: PARTFUN1:171

for b₁, b₂ being set
for b₃ being PartFunc of b₁,b₂
for b₄ being Function st b₄ in TotFuncs b₃ holds
b₃ tolerates b₄

proof end;

theorem Th172: :: PARTFUN1:172

for b₁ being set
for b₂ being PartFunc of b₁, {} st b₁ <> {} holds
TotFuncs b₂ = {}

proof end;

theorem Th173: :: PARTFUN1:173

canceled;

theorem Th174: :: PARTFUN1:174

for b₁, b₂ being set
for b₃ being PartFunc of b₁,b₂ holds
( b₃ is total iff TotFuncs b₃ = {b₃} )

proof end;

theorem Th175: :: PARTFUN1:175

for b₁ being set
for b₂ being PartFunc of {} ,b₁ holds TotFuncs b₂ = {b₂}

proof end;

theorem Th176: :: PARTFUN1:176

for b₁ being set
for b₂ being PartFunc of {} ,b₁ holds TotFuncs b₂ = {{} }

proof end;

theorem Th177: :: PARTFUN1:177

canceled;

theorem Th178: :: PARTFUN1:178

canceled;

theorem Th179: :: PARTFUN1:179

canceled;

theorem Th180: :: PARTFUN1:180

canceled;

theorem Th181: :: PARTFUN1:181

canceled;

theorem Th182: :: PARTFUN1:182

canceled;

theorem Th183: :: PARTFUN1:183

canceled;

theorem Th184: :: PARTFUN1:184

canceled;

theorem Th185: :: PARTFUN1:185

for b₁, b₂ being set
for b₃, b₄ being PartFunc of b₁,b₂ st TotFuncs b₃ meets TotFuncs b₄ holds
b₃ tolerates b₄

proof end;

theorem Th186: :: PARTFUN1:186

for b₁, b₂ being set
for b₃, b₄ being PartFunc of b₁,b₂ st ( b₂ = {} implies b₁ = {} ) & b₃ tolerates b₄ holds
TotFuncs b₃ meets TotFuncs b₄

proof end;

Lemma55: for b₁ being set
for b₂ being Relation of b₁ st b₂ = id b₁ holds
b₂ is total

proof end;

Lemma56: for b₁ being set
for b₂ being Relation st b₂ = id b₁ holds
( b₂ is reflexive & b₂ is symmetric & b₂ is antisymmetric & b₂ is transitive )

proof end;

Lemma57: for b₁ being set holds id b₁ is Relation of b₁

proof end;

registration

let c₁ be set ;
cluster reflexive symmetric antisymmetric transitive total Relation of a₁,a₁;
existence

proof end;

end;

registration

cluster symmetric transitive -> reflexive set ;
coherence

proof end;

end;

registration

let c₁ be set ;
cluster id a₁ -> reflexive symmetric antisymmetric transitive ;
coherence by Lemma56;

end;

definition

let c₁ be set ;
redefine func id as id c₁ -> total Relation of a₁;
coherence by Lemma55, Lemma57;

end;