FUNCT_2: Functions from a Set to a Set

:: Functions from a Set to a Set
:: by Czes{\l}aw Byli\'nski
::
:: Received April 6, 1989
:: Copyright (c) 1990 Association of Mizar Users

begin

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 Relation-like X -defined Y -valued Function-like quasi_total Element of bool [:X,Y:];
existence

proof end;

end;

registration

let X, Y be set ;
cluster Function-like total -> quasi_total Element of bool [:X,Y:];
coherence

proof end;

end;

definition

let X, Y be set ;
mode Function of X,Y is quasi_total PartFunc 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 :: FUNCT_2:12

for X being set
for f being Function of X,X holds f in Funcs (X,X) by Th11;

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 Th11;

end;

registration

let X be non empty set ;
let Y be empty set ;
cluster Funcs (X,Y) -> empty ;
coherence

proof end;

end;

theorem :: FUNCT_2:13

canceled;

theorem :: FUNCT_2:14

canceled;

theorem :: FUNCT_2:15

canceled;

theorem :: FUNCT_2:16

for X, Y being set
for f being Function of X,Y st ( 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 Th17: :: FUNCT_2:17

for X, Y, y being set
for f being Function of X,Y st y in rng f 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 quasi_total Relation of X,Y
for g being quasi_total Relation of Y,Z st ( not Y = {} or Z = {} or X = {} ) holds
f * g is quasi_total

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 Z <> {} & rng f = Y & rng g = Z holds
rng (g * f) = Z

proof end;

theorem Th21: :: 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 :: 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 = {} ) & 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;

definition

let Y be set ;
let f be Y -valued Relation;
attr f is onto means :Def3: :: FUNCT_2:def 3
rng f = Y;

end;

:: deftheorem Def3 defines onto FUNCT_2:def 3 :

theorem :: FUNCT_2:29

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

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 Th33: :: FUNCT_2:33

for X being set
for Y, Z being non empty set
for f being Function of X,Y
for g being Function of Y,Z st f is onto & g is onto holds
g * f is onto

proof end;

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 Th38: :: 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 by RELSET_1:34;

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 :: FUNCT_2:44

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

theorem :: FUNCT_2:45

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

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 :: FUNCT_2:47

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

theorem Th48: :: 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 Th50: :: 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 :: 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 = {} ) holds
f " Q c= (g * f) " (g .: Q)

proof end;

theorem :: FUNCT_2:54

canceled;

theorem :: FUNCT_2:55

canceled;

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 = {} ;

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;

theorem Th67: :: FUNCT_2:67

for X being set
for f being Function of X,X holds dom f = X

proof end;

registration

let X, Y be set ;
let f be quasi_total PartFunc of X,Y;
let g be quasi_total PartFunc of X,X;
cluster g * f -> quasi_total PartFunc of X,Y;
coherence

proof end;

end;

registration

let X, Y be set ;
let f be quasi_total PartFunc of Y,Y;
let g be quasi_total PartFunc of X,Y;
cluster g * f -> quasi_total PartFunc of X,Y;
coherence

proof end;

end;

theorem :: FUNCT_2:68

canceled;

theorem :: FUNCT_2:69

canceled;

theorem :: FUNCT_2:70

canceled;

theorem :: FUNCT_2:71

canceled;

theorem :: FUNCT_2:72

canceled;

theorem Th73: :: FUNCT_2:73

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

proof end;

theorem :: FUNCT_2:74

canceled;

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

canceled;

theorem :: FUNCT_2:80

canceled;

theorem :: FUNCT_2:81

canceled;

theorem :: FUNCT_2:82

canceled;

definition

let X, Y be set ;
let f be PartFunc 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 Function-like bijective -> one-to-one onto Element of bool [:X,Y:];
coherence by Def4;
cluster Function-like one-to-one onto -> bijective Element of bool [:X,Y:];
coherence by Def4;

end;

registration

let X be set ;
cluster Relation-like X -defined X -valued Function-like quasi_total bijective Element of bool [: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;

registration

let X be set ;
let f, g be onto PartFunc of X,X;
cluster g * f -> onto PartFunc of X,X;
coherence

proof end;

end;

registration

let X be set ;
let f, g be bijective Function of X,X;
cluster f * g -> bijective Function of X,X;
coherence ;

end;

registration

let X be set ;
cluster reflexive Function-like total quasi_total -> bijective Element of bool [: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 Th92: :: 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 Function-like quasi_total -> total Element of bool [:X,D:];
coherence

proof end;

end;

registration

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;
cluster f * g -> quasi_total PartFunc 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 Th113: :: 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 :: FUNCT_2:118

canceled;

theorem :: FUNCT_2:119

canceled;

theorem :: FUNCT_2:120

canceled;

begin

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 5
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 :: 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 ;

theorem :: 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 ;

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 by PARTFUN1:87;

registration

let X be set ;
let f be Function of X,X;
cluster <:f,X,X:> -> total ;
coherence by Th133;

end;

theorem :: FUNCT_2:134

canceled;

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 by PARTFUN1:148;

theorem :: FUNCT_2:143

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

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

canceled;

theorem :: FUNCT_2:150

canceled;

theorem :: FUNCT_2:151

canceled;

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 by PARTFUN1:def 7;

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 by Th155;

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} by Th161;

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 Function-like quasi_total -> non empty Element of bool [:A,B:];
coherence by Def1, RELAT_1:60;

end;

begin

scheme :: FUNCT_2:sch 6
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 7
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 8
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 9
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 10
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;

definition

let A, B, C be non empty set ;
canceled;
let f be Function of A,[:B,C:];
:: original: pr1
redefine func pr1 f -> Function of A,B means :Def6: :: FUNCT_2:def 6
for x being Element of A holds it . x = (f . x) `1 ;
coherence

proof end;

compatibility

proof end;

:: original: pr2
redefine func pr2 f -> Function of A,C means :Def7: :: FUNCT_2:def 7
for x being Element of A holds it . x = (f . x) `2 ;
coherence

proof end;

compatibility

proof end;

end;

:: deftheorem FUNCT_2:def 5 :

:: deftheorem Def6 defines pr1 FUNCT_2:def 6 :

:: deftheorem Def7 defines pr2 FUNCT_2:def 7 :

definition

let A1 be set ;
let B1 be non empty set ;
let A2 be set ;
let B2 be non empty set ;
let f1 be Function of A1,B1;
let f2 be Function of A2,B2;
:: original: =
redefine pred f1 = f2 means :: FUNCT_2:def 8
( A1 = A2 & ( for a being Element of A1 holds f1 . a = f2 . a ) );
compatibility

proof end;

end;

:: deftheorem defines = FUNCT_2:def 8 :

definition

let A, B be set ;
let f1, f2 be Function of A,B;
:: original: =
redefine pred f1 = f2 means :: FUNCT_2:def 9
for a being Element of A holds f1 . a = f2 . a;
compatibility by Th113;

end;

:: deftheorem defines = FUNCT_2:def 9 :

theorem :: FUNCT_2:170

for N being set
for f being Function of N,(bool N) ex R being Relation of N st
for i being set st i in N holds
Im (R,i) = f . i

proof end;

theorem Th171: :: FUNCT_2:171

for X being set
for A being Subset of X holds (id X) " A = A

proof end;

theorem :: FUNCT_2:172

for A, B being non empty set
for f being Function of A,B
for A0 being Subset of A
for B0 being Subset of B holds
( f .: A0 c= B0 iff A0 c= f " B0 )

proof end;

theorem :: FUNCT_2:173

for A, B being non empty set
for f being Function of A,B
for A0 being non empty Subset of A
for f0 being Function of A0,B st ( for c being Element of A st c in A0 holds
f . c = f0 . c ) holds
f | A0 = f0

proof end;

theorem :: FUNCT_2:174

for f being Function
for A0, C being set st C c= A0 holds
f .: C = (f | A0) .: C

proof end;

theorem :: FUNCT_2:175

for f being Function
for A0, D being set st f " D c= A0 holds
f " D = (f | A0) " D

proof end;

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

ex t being Function of F₁(),F₂() st
for a being Element of F₁() holds t . a in F₃(a)

provided

A1: for a being Element of F₁() holds F₂() meets F₃(a)

proof end;

theorem Th176: :: FUNCT_2:176

for X, D being non empty set
for p being Function of X,D
for i being Element of X holds p /. i = p . i

proof end;

registration

let X, D be non empty set ;
let p be Function of X,D;
let i be Element of X;
identify p /. i with p . i;
correctness by Th176;

end;

theorem :: FUNCT_2:177

for S, X being set
for f being Function of S,X
for A being Subset of X st ( X = {} implies S = {} ) holds
(f " A) ` = f " (A `)

proof end;

theorem :: FUNCT_2:178

for X, Y, Z being set
for D being non empty set
for f being Function of X,D st Y c= X & f .: Y c= Z holds
f | Y is Function of Y,Z

proof end;

definition

let T, S be non empty set ;
let f be Function of T,S;
let G be Subset-Family of S;
func f " G -> Subset-Family of T means :Def10: :: FUNCT_2:def 10
for A being Subset of T holds
( A in it iff ex B being Subset of S st
( B in G & A = f " B ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines " FUNCT_2:def 10 :

theorem :: FUNCT_2:179

for T, S being non empty set
for f being Function of T,S
for A, B being Subset-Family of S st A c= B holds
f " A c= f " B

proof end;

definition

let T, S be non empty set ;
let f be Function of T,S;
let G be Subset-Family of T;
func f .: G -> Subset-Family of S means :Def11: :: FUNCT_2:def 11
for A being Subset of S holds
( A in it iff ex B being Subset of T st
( B in G & A = f .: B ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines .: FUNCT_2:def 11 :

theorem :: FUNCT_2:180

for T, S being non empty set
for f being Function of T,S
for A, B being Subset-Family of T st A c= B holds
f .: A c= f .: B

proof end;

theorem :: FUNCT_2:181

for T, S being non empty set
for f being Function of T,S
for B being Subset-Family of S
for P being Subset of S st f .: (f " B) is Cover of P holds
B is Cover of P

proof end;

theorem :: FUNCT_2:182

for T, S being non empty set
for f being Function of T,S
for B being Subset-Family of T
for P being Subset of T st B is Cover of P holds
f " (f .: B) is Cover of P

proof end;

theorem :: FUNCT_2:183

for T, S being non empty set
for f being Function of T,S
for Q being Subset-Family of S holds union (f .: (f " Q)) c= union Q

proof end;

theorem :: FUNCT_2:184

for T, S being non empty set
for f being Function of T,S
for P being Subset-Family of T holds union P c= union (f " (f .: P))

proof end;

definition

let X, Y, Z be set ;
let f be Function of X,Y;
let p be PartFunc of Y,Z;
assume that
A1: Y <> {} and
A2: rng f c= dom p ;
func p /* f -> Function of X,Z equals :Def12: :: FUNCT_2:def 12
p * f;
coherence

proof end;

end;

:: deftheorem Def12 defines /* FUNCT_2:def 12 :

theorem Th185: :: FUNCT_2:185

for Z, X being set
for Y being non empty set
for f being Function of X,Y
for p being PartFunc of Y,Z
for x being Element of X st X <> {} & rng f c= dom p holds
(p /* f) . x = p . (f . x)

proof end;

theorem Th186: :: FUNCT_2:186

for Z, X being set
for Y being non empty set
for f being Function of X,Y
for p being PartFunc of Y,Z
for x being Element of X st X <> {} & rng f c= dom p holds
(p /* f) . x = p /. (f . x)

proof end;

theorem :: FUNCT_2:187

for Z, X being set
for Y being non empty set
for f being Function of X,Y
for p being PartFunc of Y,Z
for g being Function of X,X st rng f c= dom p holds
(p /* f) * g = p /* (f * g)

proof end;

theorem :: FUNCT_2:188

for X, Y being non empty set
for f being Function of X,Y holds
( f is constant iff ex y being Element of Y st rng f = {y} )

proof end;

theorem :: FUNCT_2:189

for A, B being non empty set
for x being Element of A
for f being Function of A,B holds f . x in rng f

proof end;

theorem Th190: :: FUNCT_2:190

for y, A, B being set
for f being Function of A,B st y in rng f holds
ex x being Element of A st y = f . x

proof end;

theorem :: FUNCT_2:191

for Z being set
for A, B being non empty set
for f being Function of A,B st ( for x being Element of A holds f . x in Z ) holds
rng f c= Z

proof end;

theorem :: FUNCT_2:192

for Y, X being non empty set
for Z being set
for f being Function of X,Y
for g being PartFunc of Y,Z
for x being Element of X st g is total holds
(g /* f) . x = g . (f . x)

proof end;

theorem :: FUNCT_2:193

for Y, X being non empty set
for Z being set
for f being Function of X,Y
for g being PartFunc of Y,Z
for x being Element of X st g is total holds
(g /* f) . x = g /. (f . x)

proof end;

theorem Th194: :: FUNCT_2:194

for X, Y being non empty set
for Z, S being set
for f being Function of X,Y
for g being PartFunc of Y,Z st rng f c= dom (g | S) holds
(g | S) /* f = g /* f

proof end;

theorem :: FUNCT_2:195

for X, Y being non empty set
for Z, S, T being set
for f being Function of X,Y
for g being PartFunc of Y,Z st rng f c= dom (g | S) & S c= T holds
(g | S) /* f = (g | T) /* f

proof end;

theorem :: FUNCT_2:196

for D, A, B being non empty set
for H being Function of D,[:A,B:]
for d being Element of D holds H . d = [((pr1 H) . d),((pr2 H) . d)]

proof end;

theorem :: FUNCT_2:197

for A1, A2, B1, B2 being set
for f being Function of A1,A2
for g being Function of B1,B2 st f tolerates g holds
f /\ g is Function of (A1 /\ B1),(A2 /\ B2)

proof end;

registration

let A, B be set ;
cluster Funcs (A,B) -> functional ;
coherence

proof end;

end;

definition

let A, B be set ;
mode FUNCTION_DOMAIN of A,B -> non empty set means :Def13: :: FUNCT_2:def 13
for x being Element of it holds x is Function of A,B;
existence

proof end;

end;

:: deftheorem Def13 defines FUNCTION_DOMAIN FUNCT_2:def 13 :

registration

let A, B be set ;
cluster -> functional FUNCTION_DOMAIN of A,B;
coherence

proof end;

end;

theorem :: FUNCT_2:198

for P, Q being set
for f being Function of P,Q holds {f} is FUNCTION_DOMAIN of P,Q

proof end;

theorem Th199: :: FUNCT_2:199

for P being set
for B being non empty set holds Funcs (P,B) is FUNCTION_DOMAIN of P,B

proof end;

definition

let A be set ;
let B be non empty set ;
:: original: Funcs
redefine func Funcs (A,B) -> FUNCTION_DOMAIN of A,B;
coherence by Th199;
let F be FUNCTION_DOMAIN of A,B;
:: original: Element
redefine mode Element of F -> Function of A,B;
coherence by Def13;

end;

registration

let I be set ;
cluster id I -> I -defined total I -defined Function;
coherence ;

end;

definition

let X, A be non empty set ;
let F be Function of X,A;
let x be set ;
assume A1: x in X ;
:: original: /.
redefine func F /. x -> Element of A equals :: FUNCT_2:def 14
F . x;
compatibility

proof end;

end;

:: deftheorem defines /. FUNCT_2:def 14 :

theorem :: FUNCT_2:200

for X being non empty set
for f being Function of X,X
for g being b₁ -valued Function holds dom (f * g) = dom g

proof end;

theorem :: FUNCT_2:201

for X being non empty set
for f being Function of X,X st ( for x being Element of X holds f . x = x ) holds
f = id X

proof end;