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

::

:: Received March 3, 1989

:: Copyright (c) 1990 Association of Mizar Users

begin

definition

let X be set ;

attr X is Function-like means :Def1: :: FUNCT_1:def 1

for x, y1, y2 being set st [x,y1] in X & [x,y2] in X holds

y1 = y2;

end;
attr X is Function-like means :Def1: :: FUNCT_1:def 1

for x, y1, y2 being set st [x,y1] in X & [x,y2] in X holds

y1 = y2;

:: deftheorem Def1 defines Function-like FUNCT_1:def 1 :

for X being set holds

( X is Function-like iff for x, y1, y2 being set st [x,y1] in X & [x,y2] in X holds

y1 = y2 );

registration

cluster empty -> Function-like set ;

coherence

for b_{1} being set st b_{1} is empty holds

b_{1} is Function-like

end;
coherence

for b

b

proof end;

registration

cluster Relation-like Function-like set ;

existence

ex b_{1} being Relation st b_{1} is Function-like

end;
existence

ex b

proof end;

registration
end;

theorem :: FUNCT_1:1

canceled;

theorem :: FUNCT_1:2

canceled;

definition

let f be Function;

let x be set ;

canceled;

canceled;

func f . x -> set means :Def4: :: FUNCT_1:def 4

[x,it] in f if x in dom f

otherwise it = {} ;

existence

( ( x in dom f implies ex b_{1} being set st [x,b_{1}] in f ) & ( not x in dom f implies ex b_{1} being set st b_{1} = {} ) )
by RELAT_1:def 4;

uniqueness

for b_{1}, b_{2} being set holds

( ( x in dom f & [x,b_{1}] in f & [x,b_{2}] in f implies b_{1} = b_{2} ) & ( not x in dom f & b_{1} = {} & b_{2} = {} implies b_{1} = b_{2} ) )
by Def1;

consistency

for b_{1} being set holds verum
;

end;
let x be set ;

canceled;

canceled;

func f . x -> set means :Def4: :: FUNCT_1:def 4

[x,it] in f if x in dom f

otherwise it = {} ;

existence

( ( x in dom f implies ex b

uniqueness

for b

( ( x in dom f & [x,b

consistency

for b

:: deftheorem FUNCT_1:def 2 :

canceled;

:: deftheorem FUNCT_1:def 3 :

canceled;

:: deftheorem Def4 defines . FUNCT_1:def 4 :

for f being Function

for x, b

( ( x in dom f implies ( b

theorem :: FUNCT_1:3

canceled;

theorem :: FUNCT_1:4

canceled;

theorem :: FUNCT_1:5

canceled;

theorem :: FUNCT_1:6

canceled;

theorem :: FUNCT_1:7

canceled;

theorem Th8: :: FUNCT_1:8

proof end;

theorem Th9: :: FUNCT_1:9

for f, g being Function st dom f = dom g & ( for x being set st x in dom f holds

f . x = g . x ) holds

f = g

f . x = g . x ) holds

f = g

proof end;

definition

let f be Function;

redefine func proj2 f means :Def5: :: FUNCT_1:def 5

for y being set holds

( y in it iff ex x being set st

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

compatibility

for b_{1} being set holds

( b_{1} = rng f iff for y being set holds

( y in b_{1} iff ex x being set st

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

end;
redefine func proj2 f means :Def5: :: FUNCT_1:def 5

for y being set holds

( y in it iff ex x being set st

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

compatibility

for b

( b

( y in b

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

proof end;

:: deftheorem Def5 defines rng FUNCT_1:def 5 :

for f being Function

for b

( b

( y in b

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

theorem :: FUNCT_1:10

canceled;

theorem :: FUNCT_1:11

canceled;

theorem Th12: :: FUNCT_1:12

theorem :: FUNCT_1:13

canceled;

theorem Th14: :: FUNCT_1:14

proof end;

scheme :: FUNCT_1:sch 2

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

FuncEx{ F

ex f being Function st

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

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

provided( dom f = F

P

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

y1 = y2 and

A2: for x being set st x in F_{1}() holds

ex y being set st P_{1}[x,y]

y1 = y2 and

A2: for x being set st x in F

ex y being set st P

proof end;

scheme :: FUNCT_1:sch 3

Lambda{ F_{1}() -> set , F_{2}( set ) -> set } :

Lambda{ F

ex f being Function st

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

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

( dom f = F

f . x = F

proof end;

theorem Th15: :: FUNCT_1:15

proof end;

theorem :: FUNCT_1:16

proof end;

theorem :: FUNCT_1:17

proof end;

theorem :: FUNCT_1:18

proof end;

theorem :: FUNCT_1:19

for Y being set

for f being Function st ( for y being set st y in Y holds

ex x being set st

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

Y c= rng f

for f being Function st ( for y being set st y in Y holds

ex x being set st

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

Y c= rng f

proof end;

registration
end;

theorem :: FUNCT_1:20

for f, g, h being Function st ( for x being set holds

( x in dom h iff ( x in dom f & f . x in dom g ) ) ) & ( for x being set st x in dom h holds

h . x = g . (f . x) ) holds

h = g * f

( x in dom h iff ( x in dom f & f . x in dom g ) ) ) & ( for x being set st x in dom h holds

h . x = g . (f . x) ) holds

h = g * f

proof end;

theorem Th21: :: FUNCT_1:21

for x being set

for g, f being Function holds

( x in dom (g * f) iff ( x in dom f & f . x in dom g ) )

for g, f being Function holds

( x in dom (g * f) iff ( x in dom f & f . x in dom g ) )

proof end;

theorem Th22: :: FUNCT_1:22

proof end;

theorem Th23: :: FUNCT_1:23

proof end;

theorem :: FUNCT_1:24

canceled;

theorem :: FUNCT_1:25

proof end;

theorem :: FUNCT_1:26

canceled;

theorem Th27: :: FUNCT_1:27

proof end;

theorem :: FUNCT_1:28

canceled;

theorem :: FUNCT_1:29

canceled;

theorem :: FUNCT_1:30

canceled;

theorem :: FUNCT_1:31

canceled;

theorem :: FUNCT_1:32

canceled;

theorem :: FUNCT_1:33

for Y being set

for f being Function st rng f c= Y & ( for g, h being Function st dom g = Y & dom h = Y & g * f = h * f holds

g = h ) holds

Y = rng f

for f being Function st rng f c= Y & ( for g, h being Function st dom g = Y & dom h = Y & g * f = h * f holds

g = h ) holds

Y = rng f

proof end;

registration
end;

theorem Th34: :: FUNCT_1:34

for X being set

for f being Function holds

( f = id X iff ( dom f = X & ( for x being set st x in X holds

f . x = x ) ) )

for f being Function holds

( f = id X iff ( dom f = X & ( for x being set st x in X holds

f . x = x ) ) )

proof end;

theorem :: FUNCT_1:35

theorem :: FUNCT_1:36

canceled;

theorem Th37: :: FUNCT_1:37

proof end;

theorem :: FUNCT_1:38

proof end;

theorem :: FUNCT_1:39

canceled;

theorem :: FUNCT_1:40

for x, Y being set

for f being Function holds

( x in dom ((id Y) * f) iff ( x in dom f & f . x in Y ) )

for f being Function holds

( x in dom ((id Y) * f) iff ( x in dom f & f . x in Y ) )

proof end;

theorem :: FUNCT_1:41

canceled;

theorem :: FUNCT_1:42

canceled;

theorem :: FUNCT_1:43

proof end;

theorem Th44: :: FUNCT_1:44

proof end;

definition

let f be Function;

canceled;

canceled;

attr f is one-to-one means :Def8: :: FUNCT_1:def 8

for x1, x2 being set st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds

x1 = x2;

end;
canceled;

canceled;

attr f is one-to-one means :Def8: :: FUNCT_1:def 8

for x1, x2 being set st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds

x1 = x2;

:: deftheorem FUNCT_1:def 6 :

canceled;

:: deftheorem FUNCT_1:def 7 :

canceled;

:: deftheorem Def8 defines one-to-one FUNCT_1:def 8 :

for f being Function holds

( f is one-to-one iff for x1, x2 being set st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds

x1 = x2 );

theorem :: FUNCT_1:45

canceled;

theorem Th46: :: FUNCT_1:46

proof end;

theorem Th47: :: FUNCT_1:47

proof end;

theorem :: FUNCT_1:48

for g, f being Function st g * f is one-to-one & rng f = dom g holds

( f is one-to-one & g is one-to-one )

( f is one-to-one & g is one-to-one )

proof end;

theorem :: FUNCT_1:49

for f being Function holds

( f is one-to-one iff for g, h being Function st rng g c= dom f & rng h c= dom f & dom g = dom h & f * g = f * h holds

g = h )

( f is one-to-one iff for g, h being Function st rng g c= dom f & rng h c= dom f & dom g = dom h & f * g = f * h holds

g = h )

proof end;

theorem :: FUNCT_1:50

for X being set

for f, g being Function st dom f = X & dom g = X & rng g c= X & f is one-to-one & f * g = f holds

g = id X

for f, g being Function st dom f = X & dom g = X & rng g c= X & f is one-to-one & f * g = f holds

g = id X

proof end;

theorem :: FUNCT_1:51

proof end;

registration
end;

theorem :: FUNCT_1:52

theorem :: FUNCT_1:53

proof end;

registration

cluster empty Relation-like Function-like -> one-to-one set ;

coherence

for b_{1} being Function st b_{1} is empty holds

b_{1} is one-to-one

end;
coherence

for b

b

proof end;

registration

cluster Relation-like Function-like one-to-one set ;

existence

ex b_{1} being Function st b_{1} is one-to-one

end;
existence

ex b

proof end;

registration

let f be one-to-one Function;

cluster f ~ -> Function-like ;

coherence

f ~ is Function-like

end;
cluster f ~ -> Function-like ;

coherence

f ~ is Function-like

proof end;

definition

let f be Function;

assume A1: f is one-to-one ;

func f " -> Function equals :Def9: :: FUNCT_1:def 9

f ~ ;

coherence

f ~ is Function by A1;

end;
assume A1: f is one-to-one ;

func f " -> Function equals :Def9: :: FUNCT_1:def 9

f ~ ;

coherence

f ~ is Function by A1;

:: deftheorem Def9 defines " FUNCT_1:def 9 :

for f being Function st f is one-to-one holds

f " = f ~ ;

theorem Th54: :: FUNCT_1:54

for f being Function st f is one-to-one holds

for g being Function holds

( g = f " iff ( dom g = rng f & ( for y, x being set holds

( y in rng f & x = g . y iff ( x in dom f & y = f . x ) ) ) ) )

for g being Function holds

( g = f " iff ( dom g = rng f & ( for y, x being set holds

( y in rng f & x = g . y iff ( x in dom f & y = f . x ) ) ) ) )

proof end;

theorem Th55: :: FUNCT_1:55

proof end;

theorem Th56: :: FUNCT_1:56

for x being set

for f being Function st f is one-to-one & x in dom f holds

( x = (f ") . (f . x) & x = ((f ") * f) . x )

for f being Function st f is one-to-one & x in dom f holds

( x = (f ") . (f . x) & x = ((f ") * f) . x )

proof end;

theorem Th57: :: FUNCT_1:57

for y being set

for f being Function st f is one-to-one & y in rng f holds

( y = f . ((f ") . y) & y = (f * (f ")) . y )

for f being Function st f is one-to-one & y in rng f holds

( y = f . ((f ") . y) & y = (f * (f ")) . y )

proof end;

theorem Th58: :: FUNCT_1:58

proof end;

theorem Th59: :: FUNCT_1:59

proof end;

theorem :: FUNCT_1:60

for f, g being Function st f is one-to-one & dom f = rng g & rng f = dom g & ( for x, y being set st x in dom f & y in dom g holds

( f . x = y iff g . y = x ) ) holds

g = f "

( f . x = y iff g . y = x ) ) holds

g = f "

proof end;

theorem Th61: :: FUNCT_1:61

proof end;

theorem Th62: :: FUNCT_1:62

proof end;

registration

let f be one-to-one Function;

cluster f " -> one-to-one ;

coherence

f " is one-to-one by Th62;

let g be one-to-one Function;

cluster g * f -> one-to-one ;

coherence

g * f is one-to-one by Th46;

end;
cluster f " -> one-to-one ;

coherence

f " is one-to-one by Th62;

let g be one-to-one Function;

cluster g * f -> one-to-one ;

coherence

g * f is one-to-one by Th46;

Lm1: for X being set

for g2, f, g1 being Function st rng g2 = X & f * g2 = id (dom g1) & g1 * f = id X holds

g1 = g2

proof end;

theorem Th63: :: FUNCT_1:63

proof end;

theorem :: FUNCT_1:64

proof end;

theorem :: FUNCT_1:65

proof end;

theorem :: FUNCT_1:66

proof end;

theorem :: FUNCT_1:67

proof end;

registration

let f be Function;

let X be set ;

cluster f | X -> Function-like ;

coherence

f | X is Function-like

end;
let X be set ;

cluster f | X -> Function-like ;

coherence

f | X is Function-like

proof end;

theorem :: FUNCT_1:68

for X being set

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

g . x = f . x ) holds

g = f | X

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

g . x = f . x ) holds

g = f | X

proof end;

theorem :: FUNCT_1:69

canceled;

theorem Th70: :: FUNCT_1:70

proof end;

theorem Th71: :: FUNCT_1:71

proof end;

theorem Th72: :: FUNCT_1:72

proof end;

theorem :: FUNCT_1:73

proof end;

theorem :: FUNCT_1:74

canceled;

theorem :: FUNCT_1:75

canceled;

theorem :: FUNCT_1:76

canceled;

theorem :: FUNCT_1:77

canceled;

theorem :: FUNCT_1:78

canceled;

theorem :: FUNCT_1:79

canceled;

theorem :: FUNCT_1:80

canceled;

theorem :: FUNCT_1:81

canceled;

theorem :: FUNCT_1:82

for X, Y being set

for f being Function st X c= Y holds

( (f | X) | Y = f | X & (f | Y) | X = f | X ) by RELAT_1:102, RELAT_1:103;

for f being Function st X c= Y holds

( (f | X) | Y = f | X & (f | Y) | X = f | X ) by RELAT_1:102, RELAT_1:103;

theorem :: FUNCT_1:83

canceled;

theorem :: FUNCT_1:84

proof end;

registration

let Y be set ;

let f be Function;

cluster Y | f -> Function-like ;

coherence

Y | f is Function-like

end;
let f be Function;

cluster Y | f -> Function-like ;

coherence

Y | f is Function-like

proof end;

theorem Th85: :: FUNCT_1:85

for Y being set

for g, f being Function holds

( g = Y | f iff ( ( for x being set holds

( x in dom g iff ( x in dom f & f . x in Y ) ) ) & ( for x being set st x in dom g holds

g . x = f . x ) ) )

for g, f being Function holds

( g = Y | f iff ( ( for x being set holds

( x in dom g iff ( x in dom f & f . x in Y ) ) ) & ( for x being set st x in dom g holds

g . x = f . x ) ) )

proof end;

theorem :: FUNCT_1:86

for x, Y being set

for f being Function holds

( x in dom (Y | f) iff ( x in dom f & f . x in Y ) ) by Th85;

for f being Function holds

( x in dom (Y | f) iff ( x in dom f & f . x in Y ) ) by Th85;

theorem :: FUNCT_1:87

theorem :: FUNCT_1:88

canceled;

theorem :: FUNCT_1:89

proof end;

theorem :: FUNCT_1:90

canceled;

theorem :: FUNCT_1:91

canceled;

theorem :: FUNCT_1:92

canceled;

theorem :: FUNCT_1:93

canceled;

theorem :: FUNCT_1:94

canceled;

theorem :: FUNCT_1:95

canceled;

theorem :: FUNCT_1:96

canceled;

theorem :: FUNCT_1:97

for X, Y being set

for f being Function st X c= Y holds

( Y | (X | f) = X | f & X | (Y | f) = X | f ) by RELAT_1:129, RELAT_1:130;

for f being Function st X c= Y holds

( Y | (X | f) = X | f & X | (Y | f) = X | f ) by RELAT_1:129, RELAT_1:130;

theorem :: FUNCT_1:98

canceled;

theorem :: FUNCT_1:99

proof end;

definition

let f be Function;

let X be set ;

canceled;

canceled;

redefine func f .: X means :Def12: :: FUNCT_1:def 12

for y being set holds

( y in it iff ex x being set st

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

compatibility

for b_{1} being set holds

( b_{1} = f .: X iff for y being set holds

( y in b_{1} iff ex x being set st

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

end;
let X be set ;

canceled;

canceled;

redefine func f .: X means :Def12: :: FUNCT_1:def 12

for y being set holds

( y in it iff ex x being set st

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

compatibility

for b

( b

( y in b

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

proof end;

:: deftheorem FUNCT_1:def 10 :

canceled;

:: deftheorem FUNCT_1:def 11 :

canceled;

:: deftheorem Def12 defines .: FUNCT_1:def 12 :

for f being Function

for X being set

for b

( b

( y in b

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

theorem :: FUNCT_1:100

canceled;

theorem :: FUNCT_1:101

canceled;

theorem :: FUNCT_1:102

canceled;

theorem :: FUNCT_1:103

canceled;

theorem :: FUNCT_1:104

canceled;

theorem :: FUNCT_1:105

canceled;

theorem :: FUNCT_1:106

canceled;

theorem :: FUNCT_1:107

canceled;

theorem :: FUNCT_1:108

canceled;

theorem :: FUNCT_1:109

canceled;

theorem :: FUNCT_1:110

canceled;

theorem :: FUNCT_1:111

canceled;

theorem :: FUNCT_1:112

canceled;

theorem :: FUNCT_1:113

canceled;

theorem :: FUNCT_1:114

canceled;

theorem :: FUNCT_1:115

canceled;

theorem :: FUNCT_1:116

canceled;

theorem Th117: :: FUNCT_1:117

proof end;

theorem :: FUNCT_1:118

for x1, x2 being set

for f being Function st x1 in dom f & x2 in dom f holds

f .: {x1,x2} = {(f . x1),(f . x2)}

for f being Function st x1 in dom f & x2 in dom f holds

f .: {x1,x2} = {(f . x1),(f . x2)}

proof end;

theorem :: FUNCT_1:119

canceled;

theorem :: FUNCT_1:120

proof end;

theorem Th121: :: FUNCT_1:121

for X1, X2 being set

for f being Function st f is one-to-one holds

f .: (X1 /\ X2) = (f .: X1) /\ (f .: X2)

for f being Function st f is one-to-one holds

f .: (X1 /\ X2) = (f .: X1) /\ (f .: X2)

proof end;

theorem :: FUNCT_1:122

for f being Function st ( for X1, X2 being set holds f .: (X1 /\ X2) = (f .: X1) /\ (f .: X2) ) holds

f is one-to-one

f is one-to-one

proof end;

theorem :: FUNCT_1:123

for X1, X2 being set

for f being Function st f is one-to-one holds

f .: (X1 \ X2) = (f .: X1) \ (f .: X2)

for f being Function st f is one-to-one holds

f .: (X1 \ X2) = (f .: X1) \ (f .: X2)

proof end;

theorem :: FUNCT_1:124

for f being Function st ( for X1, X2 being set holds f .: (X1 \ X2) = (f .: X1) \ (f .: X2) ) holds

f is one-to-one

f is one-to-one

proof end;

theorem :: FUNCT_1:125

proof end;

theorem :: FUNCT_1:126

proof end;

definition

let f be Function;

let Y be set ;

redefine func f " Y means :Def13: :: FUNCT_1:def 13

for x being set holds

( x in it iff ( x in dom f & f . x in Y ) );

compatibility

for b_{1} being set holds

( b_{1} = f " Y iff for x being set holds

( x in b_{1} iff ( x in dom f & f . x in Y ) ) )

end;
let Y be set ;

redefine func f " Y means :Def13: :: FUNCT_1:def 13

for x being set holds

( x in it iff ( x in dom f & f . x in Y ) );

compatibility

for b

( b

( x in b

proof end;

:: deftheorem Def13 defines " FUNCT_1:def 13 :

for f being Function

for Y being set

for b

( b

( x in b

theorem :: FUNCT_1:127

canceled;

theorem :: FUNCT_1:128

canceled;

theorem :: FUNCT_1:129

canceled;

theorem :: FUNCT_1:130

canceled;

theorem :: FUNCT_1:131

canceled;

theorem :: FUNCT_1:132

canceled;

theorem :: FUNCT_1:133

canceled;

theorem :: FUNCT_1:134

canceled;

theorem :: FUNCT_1:135

canceled;

theorem :: FUNCT_1:136

canceled;

theorem Th137: :: FUNCT_1:137

proof end;

theorem :: FUNCT_1:138

proof end;

theorem :: FUNCT_1:139

proof end;

theorem :: FUNCT_1:140

canceled;

theorem :: FUNCT_1:141

proof end;

theorem Th142: :: FUNCT_1:142

proof end;

theorem :: FUNCT_1:143

for Y being set

for R being Relation st ( for y being set st y in Y holds

R " {y} <> {} ) holds

Y c= rng R

for R being Relation st ( for y being set st y in Y holds

R " {y} <> {} ) holds

Y c= rng R

proof end;

theorem Th144: :: FUNCT_1:144

for f being Function holds

( ( for y being set st y in rng f holds

ex x being set st f " {y} = {x} ) iff f is one-to-one )

( ( for y being set st y in rng f holds

ex x being set st f " {y} = {x} ) iff f is one-to-one )

proof end;

theorem Th145: :: FUNCT_1:145

proof end;

theorem Th146: :: FUNCT_1:146

proof end;

theorem :: FUNCT_1:147

proof end;

theorem :: FUNCT_1:148

proof end;

theorem Th149: :: FUNCT_1:149

proof end;

theorem :: FUNCT_1:150

proof end;

theorem :: FUNCT_1:151

proof end;

theorem Th152: :: FUNCT_1:152

proof end;

theorem :: FUNCT_1:153

proof end;

theorem :: FUNCT_1:154

proof end;

theorem :: FUNCT_1:155

proof end;

theorem :: FUNCT_1:156

for Y being set

for f, g, h being Function st Y = rng f & dom g = Y & dom h = Y & g * f = h * f holds

g = h

for f, g, h being Function st Y = rng f & dom g = Y & dom h = Y & g * f = h * f holds

g = h

proof end;

theorem :: FUNCT_1:157

for X1, X2 being set

for f being Function st f .: X1 c= f .: X2 & X1 c= dom f & f is one-to-one holds

X1 c= X2

for f being Function st f .: X1 c= f .: X2 & X1 c= dom f & f is one-to-one holds

X1 c= X2

proof end;

theorem Th158: :: FUNCT_1:158

proof end;

theorem :: FUNCT_1:159

proof end;

theorem :: FUNCT_1:160

proof end;

theorem :: FUNCT_1:161

proof end;

begin

theorem :: FUNCT_1:162

proof end;

definition

let f be Function;

redefine attr f is empty-yielding means :: FUNCT_1:def 14

for x being set st x in dom f holds

f . x is empty ;

compatibility

( f is empty-yielding iff for x being set st x in dom f holds

f . x is empty )

end;
redefine attr f is empty-yielding means :: FUNCT_1:def 14

for x being set st x in dom f holds

f . x is empty ;

compatibility

( f is empty-yielding iff for x being set st x in dom f holds

f . x is empty )

proof end;

:: deftheorem defines empty-yielding FUNCT_1:def 14 :

for f being Function holds

( f is empty-yielding iff for x being set st x in dom f holds

f . x is empty );

definition

let F be Function;

redefine attr F is non-empty means :Def15: :: FUNCT_1:def 15

for n being set st n in dom F holds

not F . n is empty ;

compatibility

( F is non-empty iff for n being set st n in dom F holds

not F . n is empty )

end;
redefine attr F is non-empty means :Def15: :: FUNCT_1:def 15

for n being set st n in dom F holds

not F . n is empty ;

compatibility

( F is non-empty iff for n being set st n in dom F holds

not F . n is empty )

proof end;

:: deftheorem Def15 defines non-empty FUNCT_1:def 15 :

for F being Function holds

( F is non-empty iff for n being set st n in dom F holds

not F . n is empty );

registration

cluster Relation-like non-empty Function-like set ;

existence

ex b_{1} being Function st b_{1} is non-empty

end;
existence

ex b

proof end;

scheme :: FUNCT_1:sch 4

LambdaB{ F_{1}() -> non empty set , F_{2}( set ) -> set } :

LambdaB{ F

ex f being Function st

( dom f = F_{1}() & ( for d being Element of F_{1}() holds f . d = F_{2}(d) ) )

( dom f = F

proof end;

registration

let f be non-empty Function;

cluster rng f -> with_non-empty_elements ;

coherence

rng f is with_non-empty_elements

end;
cluster rng f -> with_non-empty_elements ;

coherence

rng f is with_non-empty_elements

proof end;

definition

let f be Function;

attr f is constant means :Def16: :: FUNCT_1:def 16

for x, y being set st x in dom f & y in dom f holds

f . x = f . y;

end;
attr f is constant means :Def16: :: FUNCT_1:def 16

for x, y being set st x in dom f & y in dom f holds

f . x = f . y;

:: deftheorem Def16 defines constant FUNCT_1:def 16 :

for f being Function holds

( f is constant iff for x, y being set st x in dom f & y in dom f holds

f . x = f . y );

theorem :: FUNCT_1:163

proof end;

theorem :: FUNCT_1:164

proof end;

definition

let f, g be Function;

redefine pred f = g means :: FUNCT_1:def 17

( dom f = dom g & ( for x being set st x in dom f holds

f . x = g . x ) );

compatibility

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

f . x = g . x ) ) ) by Th9;

end;
redefine pred f = g means :: FUNCT_1:def 17

( dom f = dom g & ( for x being set st x in dom f holds

f . x = g . x ) );

compatibility

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

f . x = g . x ) ) ) by Th9;

:: deftheorem defines = FUNCT_1:def 17 :

for f, g being Function holds

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

f . x = g . x ) ) );

registration

cluster non empty Relation-like non-empty Function-like set ;

existence

ex b_{1} being Function st

( b_{1} is non-empty & not b_{1} is empty )

end;
existence

ex b

( b

proof end;

registration

let a be non empty non-empty Function;

let i be Element of dom a;

cluster a . i -> non empty ;

coherence

not a . i is empty

end;
let i be Element of dom a;

cluster a . i -> non empty ;

coherence

not a . i is empty

proof end;

registration

let f be Function;

cluster -> Function-like Element of bool f;

coherence

for b_{1} being Subset of f holds b_{1} is Function-like

end;
cluster -> Function-like Element of bool f;

coherence

for b

proof end;

theorem :: FUNCT_1:165

for f, g being Function

for D being set st D c= dom f & D c= dom g holds

( f | D = g | D iff for x being set st x in D holds

f . x = g . x )

for D being set st D c= dom f & D c= dom g holds

( f | D = g | D iff for x being set st x in D holds

f . x = g . x )

proof end;

theorem :: FUNCT_1:166

for f, g being Function

for X being set st dom f = dom g & ( for x being set st x in X holds

f . x = g . x ) holds

f | X = g | X

for X being set st dom f = dom g & ( for x being set st x in X holds

f . x = g . x ) holds

f | X = g | X

proof end;

theorem Th167: :: FUNCT_1:167

proof end;

theorem :: FUNCT_1:168

proof end;

registration

cluster empty Relation-like Function-like -> constant set ;

coherence

for b_{1} being Function st b_{1} is empty holds

b_{1} is constant

end;
coherence

for b

b

proof end;

registration

let X be trivial set ;

cluster -> trivial Element of bool X;

coherence

for b_{1} being Subset of X holds b_{1} is trivial

end;
cluster -> trivial Element of bool X;

coherence

for b

proof end;

registration
end;

registration

cluster Relation-like Function-like non constant set ;

existence

not for b_{1} being Function holds b_{1} is constant

end;
existence

not for b

proof end;

registration

let f be non constant Function;

cluster rng f -> non trivial ;

coherence

not rng f is trivial

end;
cluster rng f -> non trivial ;

coherence

not rng f is trivial

proof end;

registration

cluster Relation-like Function-like non constant -> non trivial set ;

coherence

for b_{1} being Function st not b_{1} is constant holds

not b_{1} is trivial

end;
coherence

for b

not b

proof end;

registration

cluster trivial Relation-like Function-like -> constant set ;

coherence

for b_{1} being Function st b_{1} is trivial holds

b_{1} is constant
;

end;
coherence

for b

b

theorem :: FUNCT_1:169

proof end;

theorem :: FUNCT_1:170

proof end;

theorem :: FUNCT_1:171

for F, G being Function

for X being set holds

( X c= dom (G * F) iff ( X c= dom F & F .: X c= dom G ) )

for X being set holds

( X c= dom (G * F) iff ( X c= dom F & F .: X c= dom G ) )

proof end;

definition

let f be Function;

assume A1: ( not f is empty & f is constant ) ;

func the_value_of f -> set means :: FUNCT_1:def 18

ex x being set st

( x in dom f & it = f . x );

existence

ex b_{1} being set ex x being set st

( x in dom f & b_{1} = f . x )

for b_{1}, b_{2} being set st ex x being set st

( x in dom f & b_{1} = f . x ) & ex x being set st

( x in dom f & b_{2} = f . x ) holds

b_{1} = b_{2}
by A1, Def16;

end;
assume A1: ( not f is empty & f is constant ) ;

func the_value_of f -> set means :: FUNCT_1:def 18

ex x being set st

( x in dom f & it = f . x );

existence

ex b

( x in dom f & b

proof end;

uniqueness for b

( x in dom f & b

( x in dom f & b

b

:: deftheorem defines the_value_of FUNCT_1:def 18 :

for f being Function st not f is empty & f is constant holds

for b

( b

( x in dom f & b

registration

let X, Y be set ;

cluster Relation-like X -defined Y -valued Function-like set ;

existence

ex b_{1} being Function st

( b_{1} is X -defined & b_{1} is Y -valued )

end;
cluster Relation-like X -defined Y -valued Function-like set ;

existence

ex b

( b

proof end;

theorem :: FUNCT_1:172

proof end;

definition

let IT be set ;

attr IT is functional means :Def19: :: FUNCT_1:def 19

for x being set st x in IT holds

x is Function;

end;
attr IT is functional means :Def19: :: FUNCT_1:def 19

for x being set st x in IT holds

x is Function;

:: deftheorem Def19 defines functional FUNCT_1:def 19 :

for IT being set holds

( IT is functional iff for x being set st x in IT holds

x is Function );

registration

cluster empty -> functional set ;

coherence

for b_{1} being set st b_{1} is empty holds

b_{1} is functional

cluster {f} -> functional ;

coherence

{f} is functional

cluster {f,g} -> functional ;

coherence

{f,g} is functional

end;
coherence

for b

b

proof end;

let f be Function;cluster {f} -> functional ;

coherence

{f} is functional

proof end;

let g be Function;cluster {f,g} -> functional ;

coherence

{f,g} is functional

proof end;

registration

cluster non empty functional set ;

existence

ex b_{1} being set st

( not b_{1} is empty & b_{1} is functional )

end;
existence

ex b

( not b

proof end;

registration

let P be functional set ;

cluster -> Relation-like Function-like Element of P;

coherence

for b_{1} being Element of P holds

( b_{1} is Function-like & b_{1} is Relation-like )

end;
cluster -> Relation-like Function-like Element of P;

coherence

for b

( b

proof end;

registration

let A be functional set ;

cluster -> functional Element of bool A;

coherence

for b_{1} being Subset of A holds b_{1} is functional

end;
cluster -> functional Element of bool A;

coherence

for b

proof end;

definition

let g, f be Function;

attr f is g -compatible means :Def20: :: FUNCT_1:def 20

for x being set st x in dom f holds

f . x in g . x;

end;
attr f is g -compatible means :Def20: :: FUNCT_1:def 20

for x being set st x in dom f holds

f . x in g . x;

:: deftheorem Def20 defines -compatible FUNCT_1:def 20 :

for g, f being Function holds

( f is g -compatible iff for x being set st x in dom f holds

f . x in g . x );

theorem :: FUNCT_1:173

proof end;

theorem Th174: :: FUNCT_1:174

proof end;

registration

let I be set ;

let f be Function;

cluster empty Relation-like I -defined Function-like f -compatible set ;

existence

ex b_{1} being Function st

( b_{1} is empty & b_{1} is I -defined & b_{1} is f -compatible )

end;
let f be Function;

cluster empty Relation-like I -defined Function-like f -compatible set ;

existence

ex b

( b

proof end;

registration

let X be set ;

let f be Function;

let g be f -compatible Function;

cluster g | X -> f -compatible ;

coherence

g | X is f -compatible

end;
let f be Function;

let g be f -compatible Function;

cluster g | X -> f -compatible ;

coherence

g | X is f -compatible

proof end;

registration

let I be set ;

cluster Relation-like non-empty I -defined Function-like set ;

existence

ex b_{1} being Function st

( b_{1} is non-empty & b_{1} is I -defined )

end;
cluster Relation-like non-empty I -defined Function-like set ;

existence

ex b

( b

proof end;

theorem Th175: :: FUNCT_1:175

proof end;

registration

let X be set ;

let f be X -defined Function;

cluster Relation-like Function-like f -compatible -> X -defined set ;

coherence

for b_{1} being Function st b_{1} is f -compatible holds

b_{1} is X -defined

end;
let f be X -defined Function;

cluster Relation-like Function-like f -compatible -> X -defined set ;

coherence

for b

b

proof end;

theorem :: FUNCT_1:176

proof end;

theorem :: FUNCT_1:177

proof end;

registration

let A be functional set ;

let x be set ;

let F be A -valued Function;

cluster F . x -> Relation-like Function-like ;

coherence

( F . x is Function-like & F . x is Relation-like )

end;
let x be set ;

let F be A -valued Function;

cluster F . x -> Relation-like Function-like ;

coherence

( F . x is Function-like & F . x is Relation-like )

proof end;