:: by Czes{\l}aw Byli\'nski

::

:: Received September 18, 1989

:: Copyright (c) 1990 Association of Mizar Users

begin

theorem :: PARTFUN1:1

canceled;

theorem Th2: :: PARTFUN1:2

for f, g being Function st ( for x being set st x in (dom f) /\ (dom g) holds

f . x = g . x ) holds

ex h being Function st f \/ g = h

f . x = g . x ) holds

ex h being Function st f \/ g = h

proof end;

theorem Th3: :: PARTFUN1:3

for f, g, h being Function st f \/ g = h holds

for x being set st x in (dom f) /\ (dom g) holds

f . x = g . x

for x being set st x in (dom f) /\ (dom g) holds

f . x = g . x

proof end;

scheme :: PARTFUN1:sch 1

LambdaC{ F_{1}() -> set , P_{1}[ set ], F_{2}( set ) -> set , F_{3}( set ) -> set } :

LambdaC{ F

ex f being Function st

( dom f = F_{1}() & ( for x being set st x in F_{1}() holds

( ( P_{1}[x] implies f . x = F_{2}(x) ) & ( P_{1}[x] implies f . x = F_{3}(x) ) ) ) )

( dom f = F

( ( P

proof end;

Lm1: dom {} = {}

;

Lm2: now

let X, Y be set ; :: thesis: ex E being set st

( dom E c= X & rng E c= Y )

take E = {} ; :: thesis: ( dom E c= X & rng E c= Y )

thus ( dom E c= X & rng E c= Y ) by XBOOLE_1:2; :: thesis: verum

end;
( dom E c= X & rng E c= Y )

take E = {} ; :: thesis: ( dom E c= X & rng E c= Y )

thus ( dom E c= X & rng E c= Y ) by XBOOLE_1:2; :: thesis: verum

registration

let X, Y be set ;

cluster Relation-like X -defined Y -valued Function-like Element of bool [:X,Y:];

existence

ex b_{1} being Relation of X,Y st b_{1} is Function-like

end;
cluster Relation-like X -defined Y -valued Function-like Element of bool [:X,Y:];

existence

ex b

proof end;

theorem :: PARTFUN1:4

canceled;

theorem :: PARTFUN1:5

canceled;

theorem :: PARTFUN1:6

canceled;

theorem :: PARTFUN1:7

canceled;

theorem :: PARTFUN1:8

canceled;

theorem :: PARTFUN1:9

canceled;

theorem :: PARTFUN1:10

canceled;

theorem :: PARTFUN1:11

canceled;

theorem :: PARTFUN1:12

canceled;

theorem :: PARTFUN1:13

canceled;

theorem :: PARTFUN1:14

canceled;

theorem :: PARTFUN1:15

canceled;

theorem :: PARTFUN1:16

canceled;

theorem :: PARTFUN1:17

canceled;

theorem :: PARTFUN1:18

canceled;

theorem :: PARTFUN1:19

canceled;

theorem :: PARTFUN1:20

canceled;

theorem :: PARTFUN1:21

canceled;

theorem :: PARTFUN1:22

canceled;

theorem :: PARTFUN1:23

canceled;

theorem :: PARTFUN1:24

canceled;

theorem :: PARTFUN1:25

canceled;

theorem :: PARTFUN1:26

for X, Y, y being set

for f being PartFunc of X,Y st y in rng f holds

ex x being Element of X st

( x in dom f & y = f . x )

for f being PartFunc of X,Y st y in rng f holds

ex x being Element of X st

( x in dom f & y = f . x )

proof end;

theorem Th27: :: PARTFUN1:27

proof end;

theorem :: PARTFUN1:28

canceled;

theorem :: PARTFUN1:29

canceled;

theorem :: PARTFUN1:30

canceled;

theorem :: PARTFUN1:31

canceled;

theorem :: PARTFUN1:32

canceled;

theorem :: PARTFUN1:33

canceled;

theorem :: PARTFUN1:34

for X, Y being set

for f1, f2 being PartFunc of X,Y st dom f1 = dom f2 & ( for x being Element of X st x in dom f1 holds

f1 . x = f2 . x ) holds

f1 = f2

for f1, f2 being PartFunc of X,Y st dom f1 = dom f2 & ( for x being Element of X st x in dom f1 holds

f1 . x = f2 . x ) holds

f1 = f2

proof end;

scheme :: PARTFUN1:sch 2

PartFuncEx{ F_{1}() -> set , F_{2}() -> set , P_{1}[ set , set ] } :

PartFuncEx{ F

ex f being PartFunc of F_{1}(),F_{2}() st

( ( for x being set holds

( x in dom f iff ( x in F_{1}() & ex y being set st P_{1}[x,y] ) ) ) & ( for x being set st x in dom f holds

P_{1}[x,f . x] ) )

provided( ( for x being set holds

( x in dom f iff ( x in F

P

A1:
for x, y being set st x in F_{1}() & P_{1}[x,y] holds

y in F_{2}()
and

A2: for x, y1, y2 being set st x in F_{1}() & P_{1}[x,y1] & P_{1}[x,y2] holds

y1 = y2

y in F

A2: for x, y1, y2 being set st x in F

y1 = y2

proof end;

scheme :: PARTFUN1:sch 3

LambdaR{ F_{1}() -> set , F_{2}() -> set , F_{3}( set ) -> set , P_{1}[ set ] } :

LambdaR{ F

ex f being PartFunc of F_{1}(),F_{2}() st

( ( for x being set holds

( x in dom f iff ( x in F_{1}() & P_{1}[x] ) ) ) & ( for x being set st x in dom f holds

f . x = F_{3}(x) ) )

provided
( ( for x being set holds

( x in dom f iff ( x in F

f . x = F

proof end;

definition

let X, Y, V, Z be set ;

let f be PartFunc of X,Y;

let g be PartFunc of V,Z;

:: original: *

redefine func g * f -> PartFunc of X,Z;

coherence

f * g is PartFunc of X,Z

end;
let f be PartFunc of X,Y;

let g be PartFunc of V,Z;

:: original: *

redefine func g * f -> PartFunc of X,Z;

coherence

f * g is PartFunc of X,Z

proof end;

theorem :: PARTFUN1:35

canceled;

theorem :: PARTFUN1:36

proof end;

theorem :: PARTFUN1:37

proof end;

theorem :: PARTFUN1:38

for X, Y being set

for f being PartFunc of X,Y st ( for x1, x2 being Element of X st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds

x1 = x2 ) holds

f is one-to-one

for f being PartFunc of X,Y st ( for x1, x2 being Element of X st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds

x1 = x2 ) holds

f is one-to-one

proof end;

theorem :: PARTFUN1:39

proof end;

theorem :: PARTFUN1:40

canceled;

theorem :: PARTFUN1:41

canceled;

theorem :: PARTFUN1:42

canceled;

theorem :: PARTFUN1:43

proof end;

theorem Th44: :: PARTFUN1:44

definition

let X, Y be set ;

let f be PartFunc of X,Y;

let Z be set ;

:: original: |

redefine func f | Z -> PartFunc of X,Y;

coherence

f | Z is PartFunc of X,Y by Th44;

end;
let f be PartFunc of X,Y;

let Z be set ;

:: original: |

redefine func f | Z -> PartFunc of X,Y;

coherence

f | Z is PartFunc of X,Y by Th44;

theorem :: PARTFUN1:45

proof end;

theorem :: PARTFUN1:46

theorem Th47: :: PARTFUN1:47

proof end;

theorem :: PARTFUN1:48

canceled;

theorem :: PARTFUN1:49

for X, Y, y being set

for f being PartFunc of X,Y st y in f .: X holds

ex x being Element of X st

( x in dom f & y = f . x )

for f being PartFunc of X,Y st y in f .: X holds

ex x being Element of X st

( x in dom f & y = f . x )

proof end;

theorem :: PARTFUN1:50

canceled;

theorem :: PARTFUN1:51

canceled;

theorem :: PARTFUN1:52

canceled;

theorem :: PARTFUN1:53

canceled;

theorem :: PARTFUN1:54

canceled;

theorem :: PARTFUN1:55

canceled;

theorem :: PARTFUN1:56

canceled;

theorem :: PARTFUN1:57

canceled;

theorem :: PARTFUN1:58

canceled;

theorem :: PARTFUN1:59

canceled;

theorem :: PARTFUN1:60

canceled;

theorem :: PARTFUN1:61

canceled;

theorem :: PARTFUN1:62

canceled;

theorem :: PARTFUN1:63

canceled;

theorem :: PARTFUN1:64

canceled;

theorem :: PARTFUN1:65

canceled;

theorem :: PARTFUN1:66

canceled;

theorem :: PARTFUN1:67

canceled;

theorem :: PARTFUN1:68

canceled;

theorem Th69: :: PARTFUN1:69

proof end;

theorem :: PARTFUN1:70

proof end;

theorem :: PARTFUN1:71

proof end;

theorem :: PARTFUN1:72

for x, X, Y being set

for f being Function st dom f = {x} & x in X & f . x in Y holds

f is PartFunc of X,Y

for f being Function st dom f = {x} & x in X & f . x in Y holds

f is PartFunc of X,Y

proof end;

theorem Th73: :: PARTFUN1:73

proof end;

theorem :: PARTFUN1:74

proof end;

definition

let f be Function;

let X, Y be set ;

canceled;

canceled;

func <:f,X,Y:> -> PartFunc of X,Y equals :: PARTFUN1:def 3

(Y | f) | X;

coherence

(Y | f) | X is PartFunc of X,Y by Th47;

end;
let X, Y be set ;

canceled;

canceled;

func <:f,X,Y:> -> PartFunc of X,Y equals :: PARTFUN1:def 3

(Y | f) | X;

coherence

(Y | f) | X is PartFunc of X,Y by Th47;

:: deftheorem PARTFUN1:def 1 :

canceled;

:: deftheorem PARTFUN1:def 2 :

canceled;

:: deftheorem defines <: PARTFUN1:def 3 :

for f being Function

for X, Y being set holds <:f,X,Y:> = (Y | f) | X;

theorem :: PARTFUN1:75

canceled;

theorem Th76: :: PARTFUN1:76

proof end;

theorem Th77: :: PARTFUN1:77

proof end;

theorem Th78: :: PARTFUN1:78

for x, X, Y being set

for f being Function holds

( x in dom <:f,X,Y:> iff ( x in dom f & x in X & f . x in Y ) )

for f being Function holds

( x in dom <:f,X,Y:> iff ( x in dom f & x in X & f . x in Y ) )

proof end;

theorem Th79: :: PARTFUN1:79

for x, X, Y being set

for f being Function st x in dom f & x in X & f . x in Y holds

<:f,X,Y:> . x = f . x

for f being Function st x in dom f & x in X & f . x in Y holds

<:f,X,Y:> . x = f . x

proof end;

theorem Th80: :: PARTFUN1:80

proof end;

theorem :: PARTFUN1:81

proof end;

theorem Th82: :: PARTFUN1:82

proof end;

theorem Th83: :: PARTFUN1:83

proof end;

theorem :: PARTFUN1:84

for X1, X2, Y1, Y2 being set

for f being Function st X1 c= X2 & Y1 c= Y2 holds

<:f,X1,Y1:> c= <:f,X2,Y2:>

for f being Function st X1 c= X2 & Y1 c= Y2 holds

<:f,X1,Y1:> c= <:f,X2,Y2:>

proof end;

theorem Th85: :: PARTFUN1:85

proof end;

theorem :: PARTFUN1:86

theorem :: PARTFUN1:87

proof end;

theorem :: PARTFUN1:88

canceled;

theorem :: PARTFUN1:89

canceled;

theorem :: PARTFUN1:90

canceled;

theorem Th91: :: PARTFUN1:91

proof end;

theorem Th92: :: PARTFUN1:92

proof end;

theorem :: PARTFUN1:93

for Y, Z, X being set

for f, g being Function st (rng f) /\ (dom g) c= Y holds

<:g,Y,Z:> * <:f,X,Y:> = <:(g * f),X,Z:>

for f, g being Function st (rng f) /\ (dom g) c= Y holds

<:g,Y,Z:> * <:f,X,Y:> = <:(g * f),X,Z:>

proof end;

theorem Th94: :: PARTFUN1:94

proof end;

theorem :: PARTFUN1:95

proof end;

theorem :: PARTFUN1:96

canceled;

theorem :: PARTFUN1:97

proof end;

definition

let X be set ;

let f be X -defined Relation;

attr f is total means :Def4: :: PARTFUN1:def 4

dom f = X;

end;
let f be X -defined Relation;

attr f is total means :Def4: :: PARTFUN1:def 4

dom f = X;

:: deftheorem Def4 defines total PARTFUN1:def 4 :

for X being set

for f being b

( f is total iff dom f = X );

registration

let X be empty set ;

let Y be set ;

cluster -> total Element of bool [:X,Y:];

coherence

for b_{1} being Relation of X,Y holds b_{1} is total

end;
let Y be set ;

cluster -> total Element of bool [:X,Y:];

coherence

for b

proof end;

registration

let X be non empty set ;

let Y be empty set ;

cluster -> non total Element of bool [:X,Y:];

coherence

for b_{1} being Relation of X,Y holds not b_{1} is total

end;
let Y be empty set ;

cluster -> non total Element of bool [:X,Y:];

coherence

for b

proof end;

theorem :: PARTFUN1:98

canceled;

theorem :: PARTFUN1:99

canceled;

theorem :: PARTFUN1:100

canceled;

theorem :: PARTFUN1:101

canceled;

theorem :: PARTFUN1:102

canceled;

theorem :: PARTFUN1:103

canceled;

theorem :: PARTFUN1:104

canceled;

theorem :: PARTFUN1:105

canceled;

theorem :: PARTFUN1:106

canceled;

theorem :: PARTFUN1:107

canceled;

theorem :: PARTFUN1:108

canceled;

theorem :: PARTFUN1:109

canceled;

theorem :: PARTFUN1:110

canceled;

theorem :: PARTFUN1:111

canceled;

theorem :: PARTFUN1:112

canceled;

theorem Th113: :: PARTFUN1:113

proof end;

theorem :: PARTFUN1:114

theorem :: PARTFUN1:115

proof end;

theorem :: PARTFUN1:116

proof end;

theorem :: PARTFUN1:117

proof end;

definition

let X, Y be set ;

func PFuncs (X,Y) -> set means :Def5: :: PARTFUN1:def 5

for x being set holds

( x in it iff ex f being Function st

( x = f & dom f c= X & rng f c= Y ) );

existence

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ex f being Function st

( x = f & dom f c= X & rng f c= Y ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ex f being Function st

( x = f & dom f c= X & rng f c= Y ) ) ) & ( for x being set holds

( x in b_{2} iff ex f being Function st

( x = f & dom f c= X & rng f c= Y ) ) ) holds

b_{1} = b_{2}

end;
func PFuncs (X,Y) -> set means :Def5: :: PARTFUN1:def 5

for x being set holds

( x in it iff ex f being Function st

( x = f & dom f c= X & rng f c= Y ) );

existence

ex b

for x being set holds

( x in b

( x = f & dom f c= X & rng f c= Y ) )

proof end;

uniqueness for b

( x in b

( x = f & dom f c= X & rng f c= Y ) ) ) & ( for x being set holds

( x in b

( x = f & dom f c= X & rng f c= Y ) ) ) holds

b

proof end;

:: deftheorem Def5 defines PFuncs PARTFUN1:def 5 :

for X, Y, b

( b

( x in b

( x = f & dom f c= X & rng f c= Y ) ) );

registration

let X, Y be set ;

cluster PFuncs (X,Y) -> non empty ;

coherence

not PFuncs (X,Y) is empty

end;
cluster PFuncs (X,Y) -> non empty ;

coherence

not PFuncs (X,Y) is empty

proof end;

theorem :: PARTFUN1:118

canceled;

theorem Th119: :: PARTFUN1:119

proof end;

theorem Th120: :: PARTFUN1:120

proof end;

theorem :: PARTFUN1:121

theorem :: PARTFUN1:122

proof end;

theorem :: PARTFUN1:123

proof end;

theorem :: PARTFUN1:124

canceled;

theorem :: PARTFUN1:125

canceled;

theorem :: PARTFUN1:126

canceled;

theorem :: PARTFUN1:127

canceled;

theorem :: PARTFUN1:128

proof end;

definition

let f, g be Function;

pred f tolerates g means :Def6: :: PARTFUN1:def 6

for x being set st x in (dom f) /\ (dom g) holds

f . x = g . x;

reflexivity

for f being Function

for x being set st x in (dom f) /\ (dom f) holds

f . x = f . x ;

symmetry

for f, g being Function st ( for x being set st x in (dom f) /\ (dom g) holds

f . x = g . x ) holds

for x being set st x in (dom g) /\ (dom f) holds

g . x = f . x ;

end;
pred f tolerates g means :Def6: :: PARTFUN1:def 6

for x being set st x in (dom f) /\ (dom g) holds

f . x = g . x;

reflexivity

for f being Function

for x being set st x in (dom f) /\ (dom f) holds

f . x = f . x ;

symmetry

for f, g being Function st ( for x being set st x in (dom f) /\ (dom g) holds

f . x = g . x ) holds

for x being set st x in (dom g) /\ (dom f) holds

g . x = f . x ;

:: deftheorem Def6 defines tolerates PARTFUN1:def 6 :

for f, g being Function holds

( f tolerates g iff for x being set st x in (dom f) /\ (dom g) holds

f . x = g . x );

theorem :: PARTFUN1:129

canceled;

theorem Th130: :: PARTFUN1:130

proof end;

theorem Th131: :: PARTFUN1:131

proof end;

theorem Th132: :: PARTFUN1:132

for f, g being Function st dom f c= dom g holds

( f tolerates g iff for x being set st x in dom f holds

f . x = g . x )

( f tolerates g iff for x being set st x in dom f holds

f . x = g . x )

proof end;

theorem :: PARTFUN1:133

canceled;

theorem :: PARTFUN1:134

canceled;

theorem :: PARTFUN1:135

theorem Th136: :: PARTFUN1:136

proof end;

theorem :: PARTFUN1:137

canceled;

theorem :: PARTFUN1:138

proof end;

theorem :: PARTFUN1:139

theorem :: PARTFUN1:140

for X, Y being set

for f, g being PartFunc of X,Y

for h being Function st f tolerates h & g c= f holds

g tolerates h

for f, g being PartFunc of X,Y

for h being Function st f tolerates h & g c= f holds

g tolerates h

proof end;

theorem Th141: :: PARTFUN1:141

proof end;

theorem :: PARTFUN1:142

proof end;

theorem :: PARTFUN1:143

proof end;

theorem :: PARTFUN1:144

proof end;

theorem :: PARTFUN1:145

proof end;

theorem Th146: :: PARTFUN1:146

proof end;

theorem :: PARTFUN1:147

theorem Th148: :: PARTFUN1:148

for X, Y being set

for f, g being PartFunc of X,Y st f is total & g is total & f tolerates g holds

f = g

for f, g being PartFunc of X,Y st f is total & g is total & f tolerates g holds

f = g

proof end;

theorem :: PARTFUN1:149

canceled;

theorem :: PARTFUN1:150

canceled;

theorem :: PARTFUN1:151

canceled;

theorem :: PARTFUN1:152

canceled;

theorem :: PARTFUN1:153

canceled;

theorem :: PARTFUN1:154

canceled;

theorem :: PARTFUN1:155

canceled;

theorem :: PARTFUN1:156

canceled;

theorem :: PARTFUN1:157

canceled;

theorem Th158: :: PARTFUN1:158

for X, Y being set

for f, g, h being PartFunc of X,Y st f tolerates h & g tolerates h & h is total holds

f tolerates g

for f, g, h being PartFunc of X,Y st f tolerates h & g tolerates h & h is total holds

f tolerates g

proof end;

theorem :: PARTFUN1:159

canceled;

theorem :: PARTFUN1:160

canceled;

theorem :: PARTFUN1:161

canceled;

theorem Th162: :: PARTFUN1:162

for X, Y being set

for f, g being PartFunc of X,Y st ( Y = {} implies X = {} ) & f tolerates g holds

ex h being PartFunc of X,Y st

( h is total & f tolerates h & g tolerates h )

for f, g being PartFunc of X,Y st ( Y = {} implies X = {} ) & f tolerates g holds

ex h being PartFunc of X,Y st

( h is total & f tolerates h & g tolerates h )

proof end;

definition

let X, Y be set ;

let f be PartFunc of X,Y;

func TotFuncs f -> set means :Def7: :: PARTFUN1:def 7

for x being set holds

( x in it iff ex g being PartFunc of X,Y st

( g = x & g is total & f tolerates g ) );

existence

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ex g being PartFunc of X,Y st

( g = x & g is total & f tolerates g ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ex g being PartFunc of X,Y st

( g = x & g is total & f tolerates g ) ) ) & ( for x being set holds

( x in b_{2} iff ex g being PartFunc of X,Y st

( g = x & g is total & f tolerates g ) ) ) holds

b_{1} = b_{2}

end;
let f be PartFunc of X,Y;

func TotFuncs f -> set means :Def7: :: PARTFUN1:def 7

for x being set holds

( x in it iff ex g being PartFunc of X,Y st

( g = x & g is total & f tolerates g ) );

existence

ex b

for x being set holds

( x in b

( g = x & g is total & f tolerates g ) )

proof end;

uniqueness for b

( x in b

( g = x & g is total & f tolerates g ) ) ) & ( for x being set holds

( x in b

( g = x & g is total & f tolerates g ) ) ) holds

b

proof end;

:: deftheorem Def7 defines TotFuncs PARTFUN1:def 7 :

for X, Y being set

for f being PartFunc of X,Y

for b

( b

( x in b

( g = x & g is total & f tolerates g ) ) );

theorem :: PARTFUN1:163

canceled;

theorem :: PARTFUN1:164

canceled;

theorem :: PARTFUN1:165

canceled;

theorem :: PARTFUN1:166

canceled;

theorem :: PARTFUN1:167

canceled;

theorem Th168: :: PARTFUN1:168

for X, Y being set

for f being PartFunc of X,Y

for g being set st g in TotFuncs f holds

g is PartFunc of X,Y

for f being PartFunc of X,Y

for g being set st g in TotFuncs f holds

g is PartFunc of X,Y

proof end;

theorem Th169: :: PARTFUN1:169

proof end;

theorem :: PARTFUN1:170

canceled;

theorem Th171: :: PARTFUN1:171

for X, Y being set

for f being PartFunc of X,Y

for g being Function st g in TotFuncs f holds

f tolerates g

for f being PartFunc of X,Y

for g being Function st g in TotFuncs f holds

f tolerates g

proof end;

registration

let X be non empty set ;

let Y be empty set ;

let f be PartFunc of X,Y;

cluster TotFuncs f -> empty ;

coherence

TotFuncs f is empty

end;
let Y be empty set ;

let f be PartFunc of X,Y;

cluster TotFuncs f -> empty ;

coherence

TotFuncs f is empty

proof end;

theorem :: PARTFUN1:172

canceled;

theorem :: PARTFUN1:173

canceled;

theorem Th174: :: PARTFUN1:174

proof end;

theorem :: PARTFUN1:175

theorem :: PARTFUN1:176

theorem :: PARTFUN1:177

canceled;

theorem :: PARTFUN1:178

canceled;

theorem :: PARTFUN1:179

canceled;

theorem :: PARTFUN1:180

canceled;

theorem :: PARTFUN1:181

canceled;

theorem :: PARTFUN1:182

canceled;

theorem :: PARTFUN1:183

canceled;

theorem :: PARTFUN1:184

canceled;

theorem :: PARTFUN1:185

for X, Y being set

for f, g being PartFunc of X,Y st TotFuncs f meets TotFuncs g holds

f tolerates g

for f, g being PartFunc of X,Y st TotFuncs f meets TotFuncs g holds

f tolerates g

proof end;

theorem :: PARTFUN1:186

for X, Y being set

for f, g being PartFunc of X,Y st ( Y = {} implies X = {} ) & f tolerates g holds

TotFuncs f meets TotFuncs g

for f, g being PartFunc of X,Y st ( Y = {} implies X = {} ) & f tolerates g holds

TotFuncs f meets TotFuncs g

proof end;

begin

Lm3: for X being set

for R being Relation of X st R = id X holds

R is total

proof end;

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 )

proof end;

Lm5: for X being set holds id X is Relation of X

proof end;

registration

let X be set ;

cluster Relation-like X -defined X -valued reflexive symmetric antisymmetric transitive total Element of bool [:X,X:];

existence

ex b_{1} being Relation of X st

( b_{1} is total & b_{1} is reflexive & b_{1} is symmetric & b_{1} is antisymmetric & b_{1} is transitive )

end;
cluster Relation-like X -defined X -valued reflexive symmetric antisymmetric transitive total Element of bool [:X,X:];

existence

ex b

( b

proof end;

registration

cluster Relation-like symmetric transitive -> reflexive set ;

coherence

for b_{1} being Relation st b_{1} is symmetric & b_{1} is transitive holds

b_{1} is reflexive

end;
coherence

for b

b

proof end;

registration

let X be set ;

cluster id X -> symmetric antisymmetric transitive ;

coherence

( id X is symmetric & id X is antisymmetric & id X is transitive ) by Lm4;

end;
cluster id X -> symmetric antisymmetric transitive ;

coherence

( id X is symmetric & id X is antisymmetric & id X is transitive ) by Lm4;

definition

let X be set ;

:: original: id

redefine func id X -> total Relation of X;

coherence

id X is total Relation of X by Lm3, Lm5;

end;
:: original: id

redefine func id X -> total Relation of X;

coherence

id X is total Relation of X by Lm3, Lm5;

scheme :: PARTFUN1:sch 4

LambdaC9{ F_{1}() -> non empty set , P_{1}[ set ], F_{2}( set ) -> set , F_{3}( set ) -> set } :

LambdaC9{ F

ex f being Function st

( dom f = F_{1}() & ( for x being Element of F_{1}() holds

( ( P_{1}[x] implies f . x = F_{2}(x) ) & ( P_{1}[x] implies f . x = F_{3}(x) ) ) ) )

( dom f = F

( ( P

proof end;

begin

theorem Th187: :: PARTFUN1:187

for x, y, z being set

for f, g being Function st f tolerates g & [x,y] in f & [x,z] in g holds

y = z

for f, g being Function st f tolerates g & [x,y] in f & [x,z] in g holds

y = z

proof end;

theorem :: PARTFUN1:188

for A being set st A is functional & ( for f, g being Function st f in A & g in A holds

f tolerates g ) holds

union A is Function

f tolerates g ) holds

union A is Function

proof end;

definition

let D be set ;

let p be D -valued Function;

let i be set ;

assume A1: i in dom p ;

func p /. i -> Element of D equals :: PARTFUN1:def 8

p . i;

coherence

p . i is Element of D by A1, Th27;

end;
let p be D -valued Function;

let i be set ;

assume A1: i in dom p ;

func p /. i -> Element of D equals :: PARTFUN1:def 8

p . i;

coherence

p . i is Element of D by A1, Th27;

:: deftheorem defines /. PARTFUN1:def 8 :

for D being set

for p being b

for i being set st i in dom p holds

p /. i = p . i;

registration

let X, Y be non empty set ;

cluster Relation-like X -defined Y -valued Function-like non empty Element of bool [:X,Y:];

existence

not for b_{1} being PartFunc of X,Y holds b_{1} is empty

end;
cluster Relation-like X -defined Y -valued Function-like non empty Element of bool [:X,Y:];

existence

not for b

proof end;

registration

let A, B be set ;

cluster PFuncs (A,B) -> functional ;

coherence

PFuncs (A,B) is functional

end;
cluster PFuncs (A,B) -> functional ;

coherence

PFuncs (A,B) is functional

proof end;