:: FUNCT_2 semantic presentation

definition

let X, Y be set ;
let R be Relation of X,Y;
attr R is quasi_total means :Def1: :: FUNCT_2:def 1
X = dom R if ( Y = {} implies X = {} )
otherwise R = {} ;
consistency ;

end;

:: deftheorem Def1 defines quasi_total FUNCT_2:def 1 :

registration

let X, Y be set ;
cluster Function-like quasi_total Relation of X,Y;
existence

proof end;

end;

registration

let X, Y be set ;
cluster total -> quasi_total Relation of X,Y;
coherence

proof end;

end;

definition

let X, Y be set ;
mode Function of X,Y is Function-like quasi_total Relation of X,Y;

end;

theorem :: FUNCT_2:1

canceled;

theorem :: FUNCT_2:2

canceled;

theorem :: FUNCT_2:3

for f being Function holds f is Function of dom f, rng f

proof end;

theorem Th4: :: FUNCT_2:4

for Y being set
for f being Function st rng f c= Y holds
f is Function of dom f,Y

proof end;

theorem :: FUNCT_2:5

for X, Y being set
for f being Function st dom f = X & ( for x being set st x in X holds
f . x in Y ) holds
f is Function of X,Y

proof end;

theorem Th6: :: FUNCT_2:6

for X, Y, x being set
for f being Function of X,Y st Y <> {} & x in X holds
f . x in rng f

proof end;

theorem Th7: :: FUNCT_2:7

for X, Y, x being set
for f being Function of X,Y st Y <> {} & x in X holds
f . x in Y

proof end;

theorem :: FUNCT_2:8

for X, Y, Z being set
for f being Function of X,Y st ( Y = {} implies X = {} ) & rng f c= Z holds
f is Function of X,Z

proof end;

theorem :: FUNCT_2:9

for X, Y, Z being set
for f being Function of X,Y st ( Y = {} implies X = {} ) & Y c= Z holds
f is Function of X,Z

proof end;

scheme :: FUNCT_2:sch 1
FuncEx1{ F₁() -> set , F₂() -> set , P₁[ set , set ] } :

ex f being Function of F₁(),F₂() st
for x being set st x in F₁() holds
P₁[x,f . x]

provided

A1: for x being set st x in F₁() holds
ex y being set st
( y in F₂() & P₁[x,y] )

proof end;

scheme :: FUNCT_2:sch 2
Lambda1{ F₁() -> set , F₂() -> set , F₃( set ) -> set } :

ex f being Function of F₁(),F₂() st
for x being set st x in F₁() holds
f . x = F₃(x)

provided

A1: for x being set st x in F₁() holds
F₃(x) in F₂()

proof end;

definition

let X, Y be set ;
func Funcs X,Y -> set means :Def2: :: FUNCT_2:def 2
for x being set holds
( x in it iff ex f being Function st
( x = f & dom f = X & rng f c= Y ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines Funcs FUNCT_2:def 2 :

theorem :: FUNCT_2:10

canceled;

theorem Th11: :: FUNCT_2:11

for X, Y being set
for f being Function of X,Y st ( Y = {} implies X = {} ) holds
f in Funcs X,Y

proof end;

theorem Th12: :: FUNCT_2:12

for X being set
for f being Function of X,X holds f in Funcs X,X

proof end;

registration

let X be set ;
let Y be non empty set ;
cluster Funcs X,Y -> non empty ;
coherence by Th11;

end;

registration

let X be set ;
cluster Funcs X,X -> non empty ;
coherence by Th12;

end;

theorem :: FUNCT_2:13

canceled;

theorem Th14: :: FUNCT_2:14

for X being set st X <> {} holds
Funcs X,{} = {}

proof end;

theorem :: FUNCT_2:15

canceled;

theorem :: FUNCT_2:16

for X, Y being set
for f being Function of X,Y st Y <> {} & ( for y being set st y in Y holds
ex x being set st
( x in X & y = f . x ) ) holds
rng f = Y

proof end;

theorem :: FUNCT_2:17

for X, Y, y being set
for f being Function of X,Y st y in Y & rng f = Y holds
ex x being set st
( x in X & f . x = y )

proof end;

theorem Th18: :: FUNCT_2:18

for X, Y being set
for f1, f2 being Function of X,Y st ( for x being set st x in X holds
f1 . x = f2 . x ) holds
f1 = f2

proof end;

theorem Th19: :: FUNCT_2:19

for X, Y, Z being set
for f being Function of X,Y
for g being Function of Y,Z st ( not Y = {} or Z = {} or X = {} ) holds
g * f is Function of X,Z

proof end;

theorem :: FUNCT_2:20

for X, Y, Z being set
for f being Function of X,Y
for g being Function of Y,Z st Y <> {} & Z <> {} & rng f = Y & rng g = Z holds
rng (g * f) = Z

proof end;

theorem :: FUNCT_2:21

for X, Y, x being set
for f being Function of X,Y
for g being Function st Y <> {} & x in X holds
(g * f) . x = g . (f . x)

proof end;

theorem :: FUNCT_2:22

for X, Y being set
for f being Function of X,Y st Y <> {} holds
( rng f = Y iff for Z being set st Z <> {} holds
for g, h being Function of Y,Z st g * f = h * f holds
g = h )

proof end;

theorem Th23: :: FUNCT_2:23

for X, Y being set
for f being Relation of X,Y holds
( (id X) * f = f & f * (id Y) = f )

proof end;

theorem :: FUNCT_2:24

for X, Y being set
for f being Function of X,Y
for g being Function of Y,X st f * g = id Y holds
rng f = Y

proof end;

theorem :: FUNCT_2:25

for X, Y being set
for f being Function of X,Y st ( Y = {} implies X = {} ) holds
( f is one-to-one iff for x1, x2 being set st x1 in X & x2 in X & f . x1 = f . x2 holds
x1 = x2 )

proof end;

theorem :: FUNCT_2:26

for X, Y, Z being set
for f being Function of X,Y
for g being Function of Y,Z st ( Z = {} implies Y = {} ) & ( Y = {} implies X = {} ) & g * f is one-to-one holds
f is one-to-one

proof end;

theorem :: FUNCT_2:27

for X, Y being set
for f being Function of X,Y st X <> {} & Y <> {} holds
( f is one-to-one iff for Z being set
for g, h being Function of Z,X st f * g = f * h holds
g = h )

proof end;

theorem :: FUNCT_2:28

for X, Y, Z being set
for f being Function of X,Y
for g being Function of Y,Z st Z <> {} & rng (g * f) = Z & g is one-to-one holds
rng f = Y

proof end;

theorem :: FUNCT_2:29

for X, Y being set
for f being Function of X,Y
for g being Function of Y,X st Y <> {} & g * f = id X holds
( f is one-to-one & rng g = X )

proof end;

theorem :: FUNCT_2:30

for X, Y, Z being set
for f being Function of X,Y
for g being Function of Y,Z st ( Z = {} implies Y = {} ) & g * f is one-to-one & rng f = Y holds
( f is one-to-one & g is one-to-one )

proof end;

theorem Th31: :: FUNCT_2:31

for X, Y being set
for f being Function of X,Y st f is one-to-one & rng f = Y holds
f " is Function of Y,X

proof end;

theorem :: FUNCT_2:32

for X, Y, x being set
for f being Function of X,Y st Y <> {} & f is one-to-one & x in X holds
(f " ) . (f . x) = x

proof end;

theorem :: FUNCT_2:33

canceled;

theorem :: FUNCT_2:34

for X, Y being set
for f being Function of X,Y
for g being Function of Y,X st X <> {} & Y <> {} & rng f = Y & f is one-to-one & ( for y, x being set holds
( y in Y & g . y = x iff ( x in X & f . x = y ) ) ) holds
g = f "

proof end;

theorem :: FUNCT_2:35

for X, Y being set
for f being Function of X,Y st Y <> {} & rng f = Y & f is one-to-one holds
( (f " ) * f = id X & f * (f " ) = id Y )

proof end;

theorem :: FUNCT_2:36

for X, Y being set
for f being Function of X,Y
for g being Function of Y,X st X <> {} & Y <> {} & rng f = Y & g * f = id X & f is one-to-one holds
g = f "

proof end;

theorem :: FUNCT_2:37

for X, Y being set
for f being Function of X,Y st Y <> {} & ex g being Function of Y,X st g * f = id X holds
f is one-to-one

proof end;

theorem :: FUNCT_2:38

for X, Y, Z being set
for f being Function of X,Y st ( Y = {} implies X = {} ) & Z c= X holds
f | Z is Function of Z,Y

proof end;

theorem :: FUNCT_2:39

canceled;

theorem :: FUNCT_2:40

for X, Y, Z being set
for f being Function of X,Y st X c= Z holds
f | Z = f

proof end;

theorem :: FUNCT_2:41

for X, Y, x, Z being set
for f being Function of X,Y st Y <> {} & x in X & f . x in Z holds
(Z | f) . x = f . x

proof end;

theorem :: FUNCT_2:42

canceled;

theorem :: FUNCT_2:43

for X, Y, P being set
for f being Function of X,Y st Y <> {} holds
for y being set st ex x being set st
( x in X & x in P & y = f . x ) holds
y in f .: P

proof end;

theorem Th44: :: FUNCT_2:44

for X, Y, P being set
for f being Function of X,Y holds f .: P c= Y

proof end;

definition

let X, Y be set ;
let f be Function of X,Y;
let P be set ;
:: original: .:
redefine func f .: P -> Subset of Y;
coherence by Th44;

end;

theorem Th45: :: FUNCT_2:45

for X, Y being set
for f being Function of X,Y st ( Y = {} implies X = {} ) holds
f .: X = rng f

proof end;

theorem :: FUNCT_2:46

for X, Y, Q being set
for f being Function of X,Y st Y <> {} holds
for x being set holds
( x in f " Q iff ( x in X & f . x in Q ) )

proof end;

theorem Th47: :: FUNCT_2:47

for X, Y, Q being set
for f being PartFunc of X,Y holds f " Q c= X

proof end;

definition

let X, Y be set ;
let f be PartFunc of X,Y;
let Q be set ;
:: original: "
redefine func f " Q -> Subset of X;
coherence by Th47;

end;

theorem :: FUNCT_2:48

for X, Y being set
for f being Function of X,Y st ( Y = {} implies X = {} ) holds
f " Y = X

proof end;

theorem :: FUNCT_2:49

for X, Y being set
for f being Function of X,Y holds
( ( for y being set st y in Y holds
f " {y} <> {} ) iff rng f = Y )

proof end;

theorem :: FUNCT_2:50

for X, Y, P being set
for f being Function of X,Y st ( Y = {} implies X = {} ) & P c= X holds
P c= f " (f .: P)

proof end;

theorem Th51: :: FUNCT_2:51

for X, Y being set
for f being Function of X,Y st ( Y = {} implies X = {} ) holds
f " (f .: X) = X

proof end;

theorem :: FUNCT_2:52

canceled;

theorem :: FUNCT_2:53

for X, Y, Z, Q being set
for f being Function of X,Y
for g being Function of Y,Z st ( Z = {} implies Y = {} ) & ( Y = {} implies X = {} ) holds
f " Q c= (g * f) " (g .: Q)

proof end;

theorem :: FUNCT_2:54

canceled;

theorem Th55: :: FUNCT_2:55

for Y being set
for f being Function st dom f = {} holds
f is Function of {} ,Y

proof end;

theorem :: FUNCT_2:56

canceled;

theorem :: FUNCT_2:57

canceled;

theorem :: FUNCT_2:58

canceled;

theorem :: FUNCT_2:59

for Y, P being set
for f being Function of {} ,Y holds f .: P = {}

proof end;

theorem :: FUNCT_2:60

for Y, Q being set
for f being Function of {} ,Y holds f " Q = {}

proof end;

theorem :: FUNCT_2:61

for x, Y being set
for f being Function of {x},Y st Y <> {} holds
f . x in Y

proof end;

theorem Th62: :: FUNCT_2:62

for x, Y being set
for f being Function of {x},Y st Y <> {} holds
rng f = {(f . x)}

proof end;

theorem :: FUNCT_2:63

canceled;

theorem :: FUNCT_2:64

for x, Y, P being set
for f being Function of {x},Y st Y <> {} holds
f .: P c= {(f . x)}

proof end;

theorem Th65: :: FUNCT_2:65

for X, y, x being set
for f being Function of X,{y} st x in X holds
f . x = y

proof end;

theorem Th66: :: FUNCT_2:66

for X, y being set
for f1, f2 being Function of X,{y} holds f1 = f2

proof end;

definition

let X be set ;
let f, g be Function of X,X;
:: original: *
redefine func g * f -> Function of X,X;
coherence

proof end;

end;

theorem Th67: :: FUNCT_2:67

for X being set
for f being Function of X,X holds
( dom f = X & rng f c= X )

proof end;

theorem :: FUNCT_2:68

canceled;

theorem :: FUNCT_2:69

canceled;

theorem :: FUNCT_2:70

for X, x being set
for f being Function of X,X
for g being Function st x in X holds
(g * f) . x = g . (f . x)

proof end;

theorem :: FUNCT_2:71

canceled;

theorem :: FUNCT_2:72

canceled;

theorem Th73: :: FUNCT_2:73

for X being set
for f, g being Function of X,X st rng f = X & rng g = X holds
rng (g * f) = X

proof end;

theorem :: FUNCT_2:74

for X being set
for f being Relation of X,X holds
( f * (id X) = f & (id X) * f = f ) by Th23;

theorem :: FUNCT_2:75

for X being set
for f, g being Function of X,X st g * f = f & rng f = X holds
g = id X

proof end;

theorem :: FUNCT_2:76

for X being set
for f, g being Function of X,X st f * g = f & f is one-to-one holds
g = id X

proof end;

theorem Th77: :: FUNCT_2:77

for X being set
for f being Function of X,X holds
( f is one-to-one iff for x1, x2 being set st x1 in X & x2 in X & f . x1 = f . x2 holds
x1 = x2 )

proof end;

theorem :: FUNCT_2:78

canceled;

theorem :: FUNCT_2:79

for X being set
for f being Function of X,X holds f .: X = rng f

proof end;

theorem :: FUNCT_2:80

canceled;

theorem :: FUNCT_2:81

canceled;

theorem :: FUNCT_2:82

for X being set
for f being Function of X,X holds f " (f .: X) = X

proof end;

definition

let X, Y be set ;
let f be Function of X,Y;
attr f is onto means :Def3: :: FUNCT_2:def 3
rng f = Y;

end;

:: deftheorem Def3 defines onto FUNCT_2:def 3 :

definition

let X, Y be set ;
let f be Function of X,Y;
attr f is bijective means :Def4: :: FUNCT_2:def 4
( f is one-to-one & f is onto );

end;

:: deftheorem Def4 defines bijective FUNCT_2:def 4 :

registration

let X, Y be set ;
cluster bijective -> one-to-one onto Relation of X,Y;
coherence by Def4;
cluster one-to-one onto -> bijective Relation of X,Y;
coherence by Def4;

end;

registration

let X be set ;
cluster one-to-one onto bijective Relation of X,X;
existence

proof end;

end;

definition

let X be set ;
mode Permutation of X is bijective Function of X,X;

end;

theorem Th83: :: FUNCT_2:83

for X being set
for f being Function of X,X st f is one-to-one & rng f = X holds
f is Permutation of X

proof end;

theorem :: FUNCT_2:84

canceled;

theorem :: FUNCT_2:85

for X being set
for f being Function of X,X st f is one-to-one holds
for x1, x2 being set st x1 in X & x2 in X & f . x1 = f . x2 holds
x1 = x2 by Th77;

definition

let X be set ;
let f, g be Permutation of X;
:: original: *
redefine func g * f -> Permutation of X;
coherence

proof end;

end;

registration

let X be set ;
cluster total reflexive -> one-to-one onto bijective Relation of X,X;
coherence

proof end;

end;

definition

let X be set ;
let f be Permutation of X;
:: original: "
redefine func f " -> Permutation of X;
coherence

proof end;

end;

theorem :: FUNCT_2:86

for X being set
for f, g being Permutation of X st g * f = g holds
f = id X

proof end;

theorem :: FUNCT_2:87

for X being set
for f, g being Permutation of X st g * f = id X holds
g = f "

proof end;

theorem :: FUNCT_2:88

for X being set
for f being Permutation of X holds
( (f " ) * f = id X & f * (f " ) = id X )

proof end;

theorem :: FUNCT_2:89

canceled;

theorem :: FUNCT_2:90

canceled;

theorem :: FUNCT_2:91

canceled;

theorem :: FUNCT_2:92

for X, P being set
for f being Permutation of X st P c= X holds
( f .: (f " P) = P & f " (f .: P) = P )

proof end;

registration

let X be set ;
let D be non empty set ;
cluster quasi_total -> total quasi_total Relation of X,D;
coherence

proof end;

end;

definition

let X be set ;
let D be non empty set ;
let Z be set ;
let f be Function of X,D;
let g be Function of D,Z;
:: original: *
redefine func g * f -> Function of X,Z;
coherence by Th19;

end;

definition

let C be non empty set ;
let D be set ;
let f be Function of C,D;
let c be Element of C;
:: original: .
redefine func f . c -> Element of D;
coherence

proof end;

end;

scheme :: FUNCT_2:sch 3
FuncExD{ F₁() -> non empty set , F₂() -> non empty set , P₁[ set , set ] } :

ex f being Function of F₁(),F₂() st
for x being Element of F₁() holds P₁[x,f . x]

provided

A1: for x being Element of F₁() ex y being Element of F₂() st P₁[x,y]

proof end;

scheme :: FUNCT_2:sch 4
LambdaD{ F₁() -> non empty set , F₂() -> non empty set , F₃( Element of F₁()) -> Element of F₂() } :

ex f being Function of F₁(),F₂() st
for x being Element of F₁() holds f . x = F₃(x)

proof end;

theorem :: FUNCT_2:93

canceled;

theorem :: FUNCT_2:94

canceled;

theorem :: FUNCT_2:95

canceled;

theorem :: FUNCT_2:96

canceled;

theorem :: FUNCT_2:97

canceled;

theorem :: FUNCT_2:98

canceled;

theorem :: FUNCT_2:99

canceled;

theorem :: FUNCT_2:100

canceled;

theorem :: FUNCT_2:101

canceled;

theorem :: FUNCT_2:102

canceled;

theorem :: FUNCT_2:103

canceled;

theorem :: FUNCT_2:104

canceled;

theorem :: FUNCT_2:105

canceled;

theorem :: FUNCT_2:106

canceled;

theorem :: FUNCT_2:107

canceled;

theorem :: FUNCT_2:108

canceled;

theorem :: FUNCT_2:109

canceled;

theorem :: FUNCT_2:110

canceled;

theorem :: FUNCT_2:111

canceled;

theorem :: FUNCT_2:112

canceled;

theorem :: FUNCT_2:113

for X, Y being set
for f1, f2 being Function of X,Y st ( for x being Element of X holds f1 . x = f2 . x ) holds
f1 = f2

proof end;

theorem :: FUNCT_2:114

canceled;

theorem Th115: :: FUNCT_2:115

for X, Y, P being set
for f being Function of X,Y
for y being set st y in f .: P holds
ex x being set st
( x in X & x in P & y = f . x )

proof end;

theorem :: FUNCT_2:116

for X, Y, P being set
for f being Function of X,Y
for y being set st y in f .: P holds
ex c being Element of X st
( c in P & y = f . c )

proof end;

theorem :: FUNCT_2:117

canceled;

theorem Th118: :: FUNCT_2:118

for X, Y, Z being set
for f1, f2 being Function of [:X,Y:],Z st ( for x, y being set st x in X & y in Y holds
f1 . [x,y] = f2 . [x,y] ) holds
f1 = f2

proof end;

theorem :: FUNCT_2:119

for X, Y, Z, x, y being set
for f being Function of [:X,Y:],Z st x in X & y in Y & Z <> {} holds
f . [x,y] in Z

proof end;

scheme :: FUNCT_2:sch 5
FuncEx2{ F₁() -> set , F₂() -> set , F₃() -> set , P₁[ set , set , set ] } :

ex f being Function of [:F₁(),F₂():],F₃() st
for x, y being set st x in F₁() & y in F₂() holds
P₁[x,y,f . [x,y]]

provided

A1: for x, y being set st x in F₁() & y in F₂() holds
ex z being set st
( z in F₃() & P₁[x,y,z] )

proof end;

scheme :: FUNCT_2:sch 6
Lambda2{ F₁() -> set , F₂() -> set , F₃() -> set , F₄( set , set ) -> set } :

ex f being Function of [:F₁(),F₂():],F₃() st
for x, y being set st x in F₁() & y in F₂() holds
f . [x,y] = F₄(x,y)

provided

A1: for x, y being set st x in F₁() & y in F₂() holds
F₄(x,y) in F₃()

proof end;

theorem :: FUNCT_2:120

for X, Y, Z being set
for f1, f2 being Function of [:X,Y:],Z st ( for x being Element of X
for y being Element of Y holds f1 . [x,y] = f2 . [x,y] ) holds
f1 = f2

proof end;

scheme :: FUNCT_2:sch 7
FuncEx2D{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> non empty set , P₁[ set , set , set ] } :

ex f being Function of [:F₁(),F₂():],F₃() st
for x being Element of F₁()
for y being Element of F₂() holds P₁[x,y,f . [x,y]]

provided

A1: for x being Element of F₁()
for y being Element of F₂() ex z being Element of F₃() st P₁[x,y,z]

proof end;

scheme :: FUNCT_2:sch 8
Lambda2D{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> non empty set , F₄( Element of F₁(), Element of F₂()) -> Element of F₃() } :

ex f being Function of [:F₁(),F₂():],F₃() st
for x being Element of F₁()
for y being Element of F₂() holds f . [x,y] = F₄(x,y)

proof end;

theorem Th121: :: FUNCT_2:121

for X, Y, f being set st f in Funcs X,Y holds
f is Function of X,Y

proof end;

scheme :: FUNCT_2:sch 9
Lambda1C{ F₁() -> set , F₂() -> set , P₁[ set ], F₃( set ) -> set , F₄( set ) -> set } :

ex f being Function of F₁(),F₂() st
for x being set st x in F₁() holds
( ( P₁[x] implies f . x = F₃(x) ) & ( P₁[x] implies f . x = F₄(x) ) )

provided

A1: for x being set st x in F₁() holds
( ( P₁[x] implies F₃(x) in F₂() ) & ( P₁[x] implies F₄(x) in F₂() ) )

proof end;

theorem :: FUNCT_2:122

canceled;

theorem :: FUNCT_2:123

canceled;

theorem :: FUNCT_2:124

canceled;

theorem :: FUNCT_2:125

canceled;

theorem :: FUNCT_2:126

canceled;

theorem :: FUNCT_2:127

canceled;

theorem :: FUNCT_2:128

canceled;

theorem :: FUNCT_2:129

canceled;

theorem :: FUNCT_2:130

for X, Y being set
for f being PartFunc of X,Y st dom f = X holds
f is Function of X,Y

proof end;

theorem Th131: :: FUNCT_2:131

for X, Y being set
for f being PartFunc of X,Y st f is total holds
f is Function of X,Y

proof end;

theorem Th132: :: FUNCT_2:132

for X, Y being set
for f being PartFunc of X,Y st ( Y = {} implies X = {} ) & f is Function of X,Y holds
f is total

proof end;

theorem Th133: :: FUNCT_2:133

for X, Y being set
for f being Function of X,Y st ( Y = {} implies X = {} ) holds
<:f,X,Y:> is total

proof end;

theorem :: FUNCT_2:134

for X being set
for f being Function of X,X holds <:f,X,X:> is total

proof end;

theorem :: FUNCT_2:135

canceled;

theorem Th136: :: FUNCT_2:136

for X, Y being set
for f being PartFunc of X,Y st ( Y = {} implies X = {} ) holds
ex g being Function of X,Y st
for x being set st x in dom f holds
g . x = f . x

proof end;

theorem :: FUNCT_2:137

canceled;

theorem :: FUNCT_2:138

canceled;

theorem :: FUNCT_2:139

canceled;

theorem :: FUNCT_2:140

canceled;

theorem :: FUNCT_2:141

for X, Y being set holds Funcs X,Y c= PFuncs X,Y

proof end;

theorem Th142: :: FUNCT_2:142

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

proof end;

theorem :: FUNCT_2:143

for X being set
for f, g being Function of X,X st f tolerates g holds
f = g

proof end;

theorem :: FUNCT_2:144

canceled;

theorem Th145: :: FUNCT_2:145

for X, Y being set
for f being PartFunc of X,Y
for g being Function of X,Y st ( Y = {} implies X = {} ) holds
( f tolerates g iff for x being set st x in dom f holds
f . x = g . x )

proof end;

theorem :: FUNCT_2:146

for X being set
for f being PartFunc of X,X
for g being Function of X,X holds
( f tolerates g iff for x being set st x in dom f holds
f . x = g . x )

proof end;

theorem :: FUNCT_2:147

canceled;

theorem Th148: :: FUNCT_2:148

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

proof end;

theorem :: FUNCT_2:149

for X being set
for f being PartFunc of X,X ex g being Function of X,X st f tolerates g

proof end;

theorem :: FUNCT_2:150

canceled;

theorem Th151: :: FUNCT_2:151

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

proof end;

theorem :: FUNCT_2:152

for X being set
for f, g being PartFunc of X,X
for h being Function of X,X st f tolerates h & g tolerates h holds
f tolerates g

proof end;

theorem :: FUNCT_2:153

canceled;

theorem :: FUNCT_2:154

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

proof end;

theorem Th155: :: FUNCT_2:155

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

proof end;

theorem :: FUNCT_2:156

for X being set
for f being PartFunc of X,X
for g being Function of X,X st f tolerates g holds
g in TotFuncs f

proof end;

theorem :: FUNCT_2:157

canceled;

theorem Th158: :: FUNCT_2:158

for X, Y being set
for f being PartFunc of X,Y
for g being set st g in TotFuncs f holds
g is Function of X,Y

proof end;

theorem :: FUNCT_2:159

for X, Y being set
for f being PartFunc of X,Y holds TotFuncs f c= Funcs X,Y

proof end;

theorem :: FUNCT_2:160

for X, Y being set holds TotFuncs <:{} ,X,Y:> = Funcs X,Y

proof end;

theorem Th161: :: FUNCT_2:161

for X, Y being set
for f being Function of X,Y st ( Y = {} implies X = {} ) holds
TotFuncs <:f,X,Y:> = {f}

proof end;

theorem :: FUNCT_2:162

for X being set
for f being Function of X,X holds TotFuncs <:f,X,X:> = {f}

proof end;

theorem :: FUNCT_2:163

canceled;

theorem :: FUNCT_2:164

for X, y being set
for f being PartFunc of X,{y}
for g being Function of X,{y} holds TotFuncs f = {g}

proof end;

theorem :: FUNCT_2:165

for X, Y being set
for f, g being PartFunc of X,Y st g c= f holds
TotFuncs f c= TotFuncs g

proof end;

theorem Th166: :: FUNCT_2:166

for X, Y being set
for f, g being PartFunc of X,Y st dom g c= dom f & TotFuncs f c= TotFuncs g holds
g c= f

proof end;

theorem Th167: :: FUNCT_2:167

for X, Y being set
for f, g being PartFunc of X,Y st TotFuncs f c= TotFuncs g & ( for y being set holds Y <> {y} ) holds
g c= f

proof end;

theorem :: FUNCT_2:168

for X, Y being set
for f, g being PartFunc of X,Y st ( for y being set holds Y <> {y} ) & TotFuncs f = TotFuncs g holds
f = g

proof end;

registration

let A, B be non empty set ;
cluster -> non empty total Relation of A,B;
coherence by Def1, RELAT_1:60;

end;

definition

let o, m, r be set ;
func o,m :-> r -> Function of [:{o},{m}:],{r} means :: FUNCT_2:def 5
verum;
existence ;
uniqueness by Th66;

end;

:: deftheorem defines :-> FUNCT_2:def 5 :

scheme :: FUNCT_2:sch 10
LambdaSep1{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> Element of F₁(), F₄() -> Element of F₂(), F₅( set ) -> Element of F₂() } :

ex f being Function of F₁(),F₂() st
( f . F₃() = F₄() & ( for x being Element of F₁() st x <> F₃() holds
f . x = F₅(x) ) )

proof end;

scheme :: FUNCT_2:sch 11
LambdaSep2{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> Element of F₁(), F₄() -> Element of F₁(), F₅() -> Element of F₂(), F₆() -> Element of F₂(), F₇( set ) -> Element of F₂() } :

ex f being Function of F₁(),F₂() st
( f . F₃() = F₅() & f . F₄() = F₆() & ( for x being Element of F₁() st x <> F₃() & x <> F₄() holds
f . x = F₇(x) ) )

provided

A1: F₃() <> F₄()

proof end;

theorem :: FUNCT_2:169

for A, B being set
for f being Function st f in Funcs A,B holds
( dom f = A & rng f c= B )

proof end;

scheme :: FUNCT_2:sch 12
FunctRealEx{ F₁() -> non empty set , F₂() -> set , F₃( set ) -> set } :

ex f being Function of F₁(),F₂() st
for x being Element of F₁() holds f . x = F₃(x)

provided

A1: for x being Element of F₁() holds F₃(x) in F₂()

proof end;

scheme :: FUNCT_2:sch 13
KappaMD{ F₁() -> non empty set , F₂() -> non empty set , F₃( set ) -> set } :

ex f being Function of F₁(),F₂() st
for x being Element of F₁() holds f . x = F₃(x)

provided

A1: for x being Element of F₁() holds F₃(x) is Element of F₂()

proof end;

scheme :: FUNCT_2:sch 14
NonUniqExMD{ F₁() -> non empty set , F₂() -> non empty set , P₁[ set , set ] } :

ex f being Function of F₁(),F₂() st
for x being Element of F₁() holds P₁[x,f . x]

provided

A1: for x being Element of F₁() ex y being Element of F₂() st P₁[x,y]

proof end;