:: Functions and Their Basic Properties
:: by Czes{\l}aw Byli\'nski
::
:: Received March 3, 1989
:: Copyright (c) 1990-2021 Association of Mizar Users

definition

let X be set ;

attr X is Function-like means :Def1: :: FUNCT_1:def 1
for x, y1, y2 being object st [x,y1] in X & [x,y2] in X holds
y1 = y2;

end;

:: deftheorem Def1 defines Function-like FUNCT_1:def 1 :
for X being set holds
( X is Function-like iff for x, y1, y2 being object st [x,y1] in X & [x,y2] in X holds
y1 = y2 );

registration

cluster empty -> Function-like for set ;

coherence
for b₁ being set st b₁ is empty holds
b₁ is Function-like ;

end;

registration

cluster Relation-like Function-like for set ;

existence
ex b₁ being Relation st b₁ is Function-like

proof end;

end;

definition

mode Function is Function-like Relation;

end;

registration

let a, b be object ;

cluster {[a,b]} -> Function-like ;

coherence
{[a,b]} is Function-like

proof end;

end;

scheme :: FUNCT_1:sch 1
GraphFunc{ F₁() -> set , P₁[ object , object ] } :

ex f being Function st
for x, y being object holds
( [x,y] in f iff ( x in F₁() & P₁[x,y] ) )

provided

A1: for x, y1, y2 being object st P₁[x,y1] & P₁[x,y2] holds
y1 = y2

proof end;

definition

let f be Function;
let x be object ;

func f . x -> set means :Def2: :: FUNCT_1:def 2
[x,it] in f if x in dom f
otherwise it = {} ;

existence
( ( x in dom f implies ex b₁ being set st [x,b₁] in f ) & ( not x in dom f implies ex b₁ being set st b₁ = {} ) )

proof end;

uniqueness
for b₁, b₂ being set holds
( ( x in dom f & [x,b₁] in f & [x,b₂] in f implies b₁ = b₂ ) & ( not x in dom f & b₁ = {} & b₂ = {} implies b₁ = b₂ ) ) by Def1;
consistency
for b₁ being set holds verum ;

end;

:: deftheorem Def2 defines . FUNCT_1:def 2 :
for f being Function
for x being object
for b₃ being set holds
( ( x in dom f implies ( b₃ = f . x iff [x,b₃] in f ) ) & ( not x in dom f implies ( b₃ = f . x iff b₃ = {} ) ) );

theorem Th1: :: FUNCT_1:1

for x, y being object
for f being Function holds
( [x,y] in f iff ( x in dom f & y = f . x ) )

proof end;

theorem Th2: :: FUNCT_1:2

for f, g being Function st dom f = dom g & ( for x being object st x in dom f holds
f . x = g . x ) holds
f = g

proof end;

definition

let f be Function;

redefine func rng f means :Def3: :: FUNCT_1:def 3
for y being object holds
( y in it iff ex x being object st
( x in dom f & y = f . x ) );

compatibility
for b₁ being set holds
( b₁ = rng f iff for y being object holds
( y in b₁ iff ex x being object st
( x in dom f & y = f . x ) ) )

proof end;

end;

:: deftheorem Def3 defines rng FUNCT_1:def 3 :
for f being Function
for b₂ being set holds
( b₂ = rng f iff for y being object holds
( y in b₂ iff ex x being object st
( x in dom f & y = f . x ) ) );

theorem :: FUNCT_1:3

for x being object
for f being Function st x in dom f holds
f . x in rng f by Def3;

theorem Th4: :: FUNCT_1:4

for x being object
for f being Function st dom f = {x} holds
rng f = {(f . x)}

proof end;

scheme :: FUNCT_1:sch 2
FuncEx{ F₁() -> set , P₁[ object , object ] } :

ex f being Function st
( dom f = F₁() & ( for x being object st x in F₁() holds
P₁[x,f . x] ) )

provided

A1: for x, y1, y2 being object st x in F₁() & P₁[x,y1] & P₁[x,y2] holds
y1 = y2 and
A2: for x being object st x in F₁() holds
ex y being object st P₁[x,y]

proof end;

scheme :: FUNCT_1:sch 3
Lambda{ F₁() -> set , F₂( object ) -> object } :

ex f being Function st
( dom f = F₁() & ( for x being object st x in F₁() holds
f . x = F₂(x) ) )

proof end;

theorem Th5: :: FUNCT_1:5

for X being set st X <> {} holds
for y being object ex f being Function st
( dom f = X & rng f = {y} )

proof end;

theorem :: FUNCT_1:6

for X being set st ( for f, g being Function st dom f = X & dom g = X holds
f = g ) holds
X = {}

proof end;

theorem :: FUNCT_1:7

for y being object
for f, g being Function st dom f = dom g & rng f = {y} & rng g = {y} holds
f = g

proof end;

theorem :: FUNCT_1:8

for X, Y being set st ( Y <> {} or X = {} ) holds
ex f being Function st
( X = dom f & rng f c= Y )

proof end;

theorem :: FUNCT_1:9

for Y being set
for f being Function st ( for y being object st y in Y holds
ex x being object st
( x in dom f & y = f . x ) ) holds
Y c= rng f

proof end;

notation

let f, g be Function;
synonym g * f for f * g;

end;

registration

let f, g be Function;

cluster g * f -> Function-like ;

coherence
g * f is Function-like

proof end;

end;

theorem :: FUNCT_1:10

for f, g, h being Function st ( for x being object holds
( x in dom h iff ( x in dom f & f . x in dom g ) ) ) & ( for x being object st x in dom h holds
h . x = g . (f . x) ) holds
h = g * f

proof end;

theorem Th11: :: FUNCT_1:11

for x being object
for f, g being Function holds
( x in dom (g * f) iff ( x in dom f & f . x in dom g ) )

proof end;

theorem Th12: :: FUNCT_1:12

for x being object
for f, g being Function st x in dom (g * f) holds
(g * f) . x = g . (f . x)

proof end;

theorem Th13: :: FUNCT_1:13

for x being object
for f, g being Function st x in dom f holds
(g * f) . x = g . (f . x)

proof end;

theorem :: FUNCT_1:14

for z being object
for f, g being Function st z in rng (g * f) holds
z in rng g

proof end;

theorem Th15: :: FUNCT_1:15

for f, g being Function st dom (g * f) = dom f holds
rng f c= dom g

proof end;

theorem :: FUNCT_1:16

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

proof end;

registration

let X be set ;

cluster id X -> Function-like ;

coherence
id X is Function-like

proof end;

end;

theorem Th17: :: FUNCT_1:17

for X being set
for f being Function holds
( f = id X iff ( dom f = X & ( for x being object st x in X holds
f . x = x ) ) )

proof end;

theorem Th18: :: FUNCT_1:18

for X being set
for x being object st x in X holds
(id X) . x = x by Th17;

theorem Th19: :: FUNCT_1:19

for X being set
for f being Function holds dom (f * (id X)) = (dom f) /\ X

proof end;

theorem :: FUNCT_1:20

for X being set
for x being object
for f being Function st x in (dom f) /\ X holds
f . x = (f * (id X)) . x

proof end;

theorem :: FUNCT_1:21

for Y being set
for x being object
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:22

for X, Y being set holds (id X) * (id Y) = id (X /\ Y)

proof end;

theorem Th23: :: FUNCT_1:23

for f, g being Function st rng f = dom g & g * f = f holds
g = id (dom g)

proof end;

definition

let f be Function;

attr f is one-to-one means :Def4: :: FUNCT_1:def 4
for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2;

end;

:: deftheorem Def4 defines one-to-one FUNCT_1:def 4 :
for f being Function holds
( f is one-to-one iff for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2 );

theorem Th24: :: FUNCT_1:24

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

proof end;

theorem Th25: :: FUNCT_1:25

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

proof end;

theorem :: FUNCT_1:26

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

proof end;

theorem :: FUNCT_1:27

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 )

proof end;

theorem :: FUNCT_1:28

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

proof end;

theorem :: FUNCT_1:29

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

proof end;

registration

let X be set ;

cluster id X -> one-to-one ;

coherence
id X is one-to-one

proof end;

end;

theorem :: FUNCT_1:30

canceled;

::$CT

theorem :: FUNCT_1:31

for f being Function st ex g being Function st g * f = id (dom f) holds
f is one-to-one

proof end;

registration

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

coherence
for b₁ being Function st b₁ is empty holds
b₁ is one-to-one ;

end;

registration

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

existence
ex b₁ being Function st b₁ is one-to-one

proof end;

end;

registration

let f be one-to-one Function;

cluster f ~ -> Function-like ;

coherence
f ~ is Function-like

proof end;

end;

definition

let f be Function;
assume A1: f is one-to-one ;

func f " -> Function equals :Def5: :: FUNCT_1:def 5
f ~ ;

coherence
f ~ is Function by A1;

end;

:: deftheorem Def5 defines " FUNCT_1:def 5 :
for f being Function st f is one-to-one holds
f " = f ~ ;

theorem Th31: :: FUNCT_1:32

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 object holds
( y in rng f & x = g . y iff ( x in dom f & y = f . x ) ) ) ) )

proof end;

theorem Th32: :: FUNCT_1:33

for f being Function st f is one-to-one holds
( rng f = dom (f ") & dom f = rng (f ") )

proof end;

theorem Th33: :: FUNCT_1:34

for x being object
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 Th34: :: FUNCT_1:35

for y being object
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 Th35: :: FUNCT_1:36

for f being Function st f is one-to-one holds
( dom ((f ") * f) = dom f & rng ((f ") * f) = dom f )

proof end;

theorem Th36: :: FUNCT_1:37

for f being Function st f is one-to-one holds
( dom (f * (f ")) = rng f & rng (f * (f ")) = rng f )

proof end;

theorem :: FUNCT_1:38

for f, g being Function st f is one-to-one & dom f = rng g & rng f = dom g & ( for x, y being object st x in dom f & y in dom g holds
( f . x = y iff g . y = x ) ) holds
g = f "

proof end;

theorem Th38: :: FUNCT_1:39

for f being Function st f is one-to-one holds
( (f ") * f = id (dom f) & f * (f ") = id (rng f) )

proof end;

theorem Th39: :: FUNCT_1:40

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

proof end;

registration

let f be one-to-one Function;

cluster f " -> one-to-one ;

coherence
f " is one-to-one by Th39;
let g be one-to-one Function;

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

coherence
g * f is one-to-one by Th24;

end;

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

proof end;

theorem Th40: :: FUNCT_1:41

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

proof end;

theorem :: FUNCT_1:42

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

proof end;

theorem :: FUNCT_1:43

for f being Function st f is one-to-one holds
(f ") " = f

proof end;

theorem :: FUNCT_1:44

for f, g being Function st f is one-to-one & g is one-to-one holds
(g * f) " = (f ") * (g ")

proof end;

theorem :: FUNCT_1:45

for X being set holds (id X) " = id X

proof end;

registration

let f be Function;
let X be set ;

cluster f | X -> Function-like ;

coherence
f | X is Function-like

proof end;

end;

theorem :: FUNCT_1:46

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

proof end;

theorem Th46: :: FUNCT_1:47

for X being set
for x being object
for f being Function st x in dom (f | X) holds
(f | X) . x = f . x

proof end;

theorem Th47: :: FUNCT_1:48

for X being set
for x being object
for f being Function st x in (dom f) /\ X holds
(f | X) . x = f . x

proof end;

theorem Th48: :: FUNCT_1:49

for X being set
for x being object
for f being Function st x in X holds
(f | X) . x = f . x

proof end;

theorem :: FUNCT_1:50

for X being set
for x being object
for f being Function st x in dom f & x in X holds
f . x in rng (f | X)

proof end;

theorem :: FUNCT_1:51

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:73, RELAT_1:74;

theorem :: FUNCT_1:52

for X being set
for f being Function st f is one-to-one holds
f | X is one-to-one

proof end;

registration

let Y be set ;
let f be Function;

cluster Y |` f -> Function-like ;

coherence
Y |` f is Function-like

proof end;

end;

theorem Th52: :: FUNCT_1:53

for Y being set
for f, g being Function holds
( g = Y |` f iff ( ( for x being object holds
( x in dom g iff ( x in dom f & f . x in Y ) ) ) & ( for x being object st x in dom g holds
g . x = f . x ) ) )

proof end;

theorem :: FUNCT_1:54

for Y being set
for x being object
for f being Function holds
( x in dom (Y |` f) iff ( x in dom f & f . x in Y ) ) by Th52;

theorem :: FUNCT_1:55

for Y being set
for x being object
for f being Function st x in dom (Y |` f) holds
(Y |` f) . x = f . x by Th52;

theorem :: FUNCT_1:56

for Y being set
for f being Function holds dom (Y |` f) c= dom f by Th52;

theorem :: FUNCT_1:57

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:98, RELAT_1:99;

theorem :: FUNCT_1:58

for Y being set
for f being Function st f is one-to-one holds
Y |` f is one-to-one

proof end;

definition

let f be Function;
let X be set ;

redefine func f .: X means :Def6: :: FUNCT_1:def 6
for y being object holds
( y in it iff ex x being object st
( x in dom f & x in X & y = f . x ) );

compatibility
for b₁ being set holds
( b₁ = f .: X iff for y being object holds
( y in b₁ iff ex x being object st
( x in dom f & x in X & y = f . x ) ) )

proof end;

end;

:: deftheorem Def6 defines .: FUNCT_1:def 6 :
for f being Function
for X being set
for b₃ being set holds
( b₃ = f .: X iff for y being object holds
( y in b₃ iff ex x being object st
( x in dom f & x in X & y = f . x ) ) );

theorem Th58: :: FUNCT_1:59

for x being object
for f being Function st x in dom f holds
Im (f,x) = {(f . x)}

proof end;

theorem :: FUNCT_1:60

for x1, x2 being object
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:61

for X, Y being set
for f being Function holds (Y |` f) .: X c= f .: X

proof end;

theorem Th61: :: FUNCT_1:62

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

proof end;

theorem :: FUNCT_1:63

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

proof end;

theorem :: FUNCT_1:64

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

proof end;

theorem :: FUNCT_1:65

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

proof end;

theorem :: FUNCT_1:66

for X, Y being set
for f being Function st X misses Y & f is one-to-one holds
f .: X misses f .: Y

proof end;

theorem :: FUNCT_1:67

for X, Y being set
for f being Function holds (Y |` f) .: X = Y /\ (f .: X)

proof end;

definition

let f be Function;
let Y be set ;

redefine func f " Y means :Def7: :: FUNCT_1:def 7
for x being object holds
( x in it iff ( x in dom f & f . x in Y ) );

compatibility
for b₁ being set holds
( b₁ = f " Y iff for x being object holds
( x in b₁ iff ( x in dom f & f . x in Y ) ) )

proof end;

end;

:: deftheorem Def7 defines " FUNCT_1:def 7 :
for f being Function
for Y being set
for b₃ being set holds
( b₃ = f " Y iff for x being object holds
( x in b₃ iff ( x in dom f & f . x in Y ) ) );

theorem Th67: :: FUNCT_1:68

for Y1, Y2 being set
for f being Function holds f " (Y1 /\ Y2) = (f " Y1) /\ (f " Y2)

proof end;

theorem :: FUNCT_1:69

for Y1, Y2 being set
for f being Function holds f " (Y1 \ Y2) = (f " Y1) \ (f " Y2)

proof end;

theorem :: FUNCT_1:70

for X, Y being set
for R being Relation holds (R | X) " Y = X /\ (R " Y)

proof end;

theorem :: FUNCT_1:71

for f being Function
for A, B being set st A misses B holds
f " A misses f " B

proof end;

theorem Th71: :: FUNCT_1:72

for y being object
for R being Relation holds
( y in rng R iff R " {y} <> {} )

proof end;

theorem :: FUNCT_1:73

for Y being set
for R being Relation st ( for y being object st y in Y holds
R " {y} <> {} ) holds
Y c= rng R

proof end;

theorem Th73: :: FUNCT_1:74

for f being Function holds
( ( for y being object st y in rng f holds
ex x being object st f " {y} = {x} ) iff f is one-to-one )

proof end;

theorem Th74: :: FUNCT_1:75

for Y being set
for f being Function holds f .: (f " Y) c= Y

proof end;

theorem Th75: :: FUNCT_1:76

for X being set
for R being Relation st X c= dom R holds
X c= R " (R .: X)

proof end;

theorem :: FUNCT_1:77

for Y being set
for f being Function st Y c= rng f holds
f .: (f " Y) = Y

proof end;

theorem :: FUNCT_1:78

for Y being set
for f being Function holds f .: (f " Y) = Y /\ (f .: (dom f))

proof end;

theorem Th78: :: FUNCT_1:79

for X, Y being set
for f being Function holds f .: (X /\ (f " Y)) c= (f .: X) /\ Y

proof end;

theorem :: FUNCT_1:80

for X, Y being set
for f being Function holds f .: (X /\ (f " Y)) = (f .: X) /\ Y

proof end;

theorem :: FUNCT_1:81

for X, Y being set
for R being Relation holds X /\ (R " Y) c= R " ((R .: X) /\ Y)

proof end;

theorem Th81: :: FUNCT_1:82

for X being set
for f being Function st f is one-to-one holds
f " (f .: X) c= X

proof end;

theorem :: FUNCT_1:83

for f being Function st ( for X being set holds f " (f .: X) c= X ) holds
f is one-to-one

proof end;

theorem :: FUNCT_1:84

for X being set
for f being Function st f is one-to-one holds
f .: X = (f ") " X

proof end;

theorem :: FUNCT_1:85

for Y being set
for f being Function st f is one-to-one holds
f " Y = (f ") .: Y

proof end;

:: SUPLEMENT

theorem :: FUNCT_1:86

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

proof end;

theorem :: FUNCT_1:87

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

proof end;

theorem Th87: :: FUNCT_1:88

for Y1, Y2 being set
for f being Function st f " Y1 c= f " Y2 & Y1 c= rng f holds
Y1 c= Y2

proof end;

theorem :: FUNCT_1:89

for f being Function holds
( f is one-to-one iff for y being object ex x being object st f " {y} c= {x} )

proof end;

theorem :: FUNCT_1:90

for X being set
for R, S being Relation st rng R c= dom S holds
R " X c= (R * S) " (S .: X)

proof end;

theorem :: FUNCT_1:91

for X, Y being set
for f being Function st f " X = f " Y & X c= rng f & Y c= rng f holds
X = Y by Th87;

theorem :: FUNCT_1:92

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

proof end;

:: from PBOOLE

definition

let f be Function;

redefine attr f is empty-yielding means :Def8: :: FUNCT_1:def 8
for x being object st x in dom f holds
f . x is empty ;

compatibility
( f is empty-yielding iff for x being object st x in dom f holds
f . x is empty )

proof end;

end;

:: deftheorem Def8 defines empty-yielding FUNCT_1:def 8 :
for f being Function holds
( f is empty-yielding iff for x being object st x in dom f holds
f . x is empty );

:: from UNIALG_1

definition

let F be Function;

redefine attr F is non-empty means :Def9: :: FUNCT_1:def 9
for n being object st n in dom F holds
not F . n is empty ;

compatibility
( F is non-empty iff for n being object st n in dom F holds
not F . n is empty )

proof end;

end;

:: deftheorem Def9 defines non-empty FUNCT_1:def 9 :
for F being Function holds
( F is non-empty iff for n being object st n in dom F holds
not F . n is empty );

:: new, 2004.08.04

registration

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

existence
ex b₁ being Function st b₁ is non-empty

proof end;

end;

:: from MSUALG_2

scheme :: FUNCT_1:sch 4
LambdaB{ F₁() -> non empty set , F₂( object ) -> object } :

ex f being Function st
( dom f = F₁() & ( for d being Element of F₁() holds f . d = F₂(d) ) )

proof end;

:: from PUA2MSS1, 2005.08.22, A.T.

registration

let f be non-empty Function;

cluster rng f -> with_non-empty_elements ;

coherence
rng f is with_non-empty_elements

proof end;

end;

:: from SEQM_3, 2005.12.17, A.T.

definition

let f be Function;

attr f is constant means :Def10: :: FUNCT_1:def 10
for x, y being object st x in dom f & y in dom f holds
f . x = f . y;

end;

:: deftheorem Def10 defines constant FUNCT_1:def 10 :
for f being Function holds
( f is constant iff for x, y being object st x in dom f & y in dom f holds
f . x = f . y );

theorem :: FUNCT_1:93

for A, B being set
for f being Function st A c= dom f & f .: A c= B holds
A c= f " B

proof end;

:: moved from MSAFREE3:1, AG 1.04.2006

theorem :: FUNCT_1:94

for X being set
for f being Function st X c= dom f & f is one-to-one holds
f " (f .: X) = X

proof end;

:: added, AK 5.02.2007

definition

let f, g be Function;

redefine pred f = g means :: FUNCT_1:def 11
( dom f = dom g & ( for x being object st x in dom f holds
f . x = g . x ) );

compatibility
( f = g iff ( dom f = dom g & ( for x being object st x in dom f holds
f . x = g . x ) ) ) by Th2;

end;

:: deftheorem defines = FUNCT_1:def 11 :
for f, g being Function holds
( f = g iff ( dom f = dom g & ( for x being object st x in dom f holds
f . x = g . x ) ) );

:: missing, 2007.03.09, A.T.

registration

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

existence
ex b₁ being Function st
( b₁ is non-empty & not b₁ is empty )

proof end;

end;

:: from PRVECT_1, 2007.03.09, A.T.

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

proof end;

end;

:: missing, 2007.04.13, A.T.

registration

let f be Function;

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

coherence
for b₁ being Subset of f holds b₁ is Function-like by Def1;

end;

:: from SCMFSA6A, 2007.07.23, A.T.

theorem :: FUNCT_1:95

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 )

proof end;

:: from SCMBSORT, 2007.07.26, A.T.

theorem :: FUNCT_1:96

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

proof end;

:: missing, 2007.10.28, A.T.

theorem Th96: :: FUNCT_1:97

for X being set
for f being Function holds rng (f | {X}) c= {(f . X)}

proof end;

theorem :: FUNCT_1:98

for X being set
for f being Function st X in dom f holds
rng (f | {X}) = {(f . X)}

proof end;

:: from RFUNCT_1, 2008.09.04, A.T.

registration

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

coherence
for b₁ being Function st b₁ is empty holds
b₁ is constant ;

end;

:: from WAYBEL35, 2008.08.04, A.T.

registration

let f be constant Function;

cluster rng f -> trivial ;

coherence
rng f is trivial

proof end;

end;

registration

cluster Relation-like Function-like non constant for set ;

existence
not for b₁ being Function holds b₁ is constant

proof end;

end;

registration

let f be non constant Function;

cluster rng f -> non trivial ;

coherence
not rng f is trivial

proof end;

end;

registration

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

coherence
for b₁ being Function st not b₁ is constant holds
not b₁ is trivial

proof end;

end;

registration

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

coherence
for b₁ being Function st b₁ is trivial holds
b₁ is constant ;

end;

:: from RFUNCT_2, 2008.09.14, A.T.

theorem :: FUNCT_1:99

for F, G being Function
for X being set holds (G | (F .: X)) * (F | X) = (G * F) | X

proof end;

theorem :: FUNCT_1:100

for F, G being Function
for X, X1 being set holds (G | X1) * (F | X) = (G * F) | (X /\ (F " X1))

proof end;

theorem :: FUNCT_1:101

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 ) )

proof end;

:: from YELLOW_6, 2008.12.26, A.T.

definition

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

func the_value_of f -> object means :: FUNCT_1:def 12
ex x being set st
( x in dom f & it = f . x );

existence
ex b₁ being object ex x being set st
( x in dom f & b₁ = f . x )

proof end;

uniqueness
for b₁, b₂ being object st ex x being set st
( x in dom f & b₁ = f . x ) & ex x being set st
( x in dom f & b₂ = f . x ) holds
b₁ = b₂ by A1;

end;

:: deftheorem defines the_value_of FUNCT_1:def 12 :
for f being Function st not f is empty & f is constant holds
for b₂ being object holds
( b₂ = the_value_of f iff ex x being set st
( x in dom f & b₂ = f . x ) );

:: from QC_LANG4, 2009.01.23, A.T

registration

let X, Y be set ;

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

existence
ex b₁ being Function st
( b₁ is X -defined & b₁ is Y -valued )

proof end;

end;

theorem :: FUNCT_1:102

for X being set
for f being b₁ -valued Function
for x being set st x in dom f holds
f . x in X

proof end;

:: from FRAENKEL, 2009.05.06, A.K.

definition

let IT be set ;

attr IT is functional means :Def13: :: FUNCT_1:def 13
for x being object st x in IT holds
x is Function;

end;

:: deftheorem Def13 defines functional FUNCT_1:def 13 :
for IT being set holds
( IT is functional iff for x being object st x in IT holds
x is Function );

registration

cluster empty -> functional for set ;

coherence
for b₁ being set st b₁ is empty holds
b₁ is functional ;
let f be Function;

cluster {f} -> functional ;

coherence
{f} is functional by TARSKI:def 1;
let g be Function;

cluster {f,g} -> functional ;

coherence
{f,g} is functional by TARSKI:def 2;

end;

registration

cluster non empty functional for set ;

existence
ex b₁ being set st
( not b₁ is empty & b₁ is functional )

proof end;

end;

registration

let P be functional set ;

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

coherence
for b₁ being Element of P holds
( b₁ is Function-like & b₁ is Relation-like )

proof end;

end;

registration

let A be functional set ;

cluster -> functional for Element of bool A;

coherence
for b₁ being Subset of A holds b₁ is functional ;

end;

:: new, 2009.09.30, A.T.

definition

let g, f be Function;

attr f is g -compatible means :Def14: :: FUNCT_1:def 14
for x being object st x in dom f holds
f . x in g . x;

end;

:: deftheorem Def14 defines -compatible FUNCT_1:def 14 :
for g, f being Function holds
( f is g -compatible iff for x being object st x in dom f holds
f . x in g . x );

theorem :: FUNCT_1:103

for f, g being Function st f is g -compatible & dom f = dom g holds
g is non-empty ;

theorem :: FUNCT_1:104

for f being Function holds {} is f -compatible ;

registration

let I be set ;
let f be Function;

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

existence
ex b₁ being Function st
( b₁ is empty & b₁ is I -defined & b₁ is f -compatible )

proof end;

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

proof end;

end;

registration

let I be set ;

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

existence
ex b₁ being Function st
( b₁ is non-empty & b₁ is I -defined )

proof end;

end;

theorem Th104: :: FUNCT_1:105

for f being Function
for g being b₁ -compatible Function holds dom g c= dom f

proof end;

registration

let X be set ;
let f be X -defined Function;

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

coherence
for b₁ being Function st b₁ is f -compatible holds
b₁ is X -defined

proof end;

end;

theorem :: FUNCT_1:106

for X being set
for x being object
for f being b₁ -valued Function st x in dom f holds
f . x is Element of X

proof end;

:: from JGRAPH_6, 2010.03.15, A.T.

theorem :: FUNCT_1:107

for f being Function
for A being set st f is one-to-one & A c= dom f holds
(f ") .: (f .: A) = A

proof end;

registration

let A be functional set ;
let x be object ;
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;

end;

:: missing, 2011.03.06, A.T.

theorem Th107: :: FUNCT_1:108

for X being set
for x being object
for f being Function st x in X & x in dom f holds
f . x in f .: X

proof end;

theorem :: FUNCT_1:109

for X being set
for f being Function st X <> {} & X c= dom f holds
f .: X <> {}

proof end;

registration

let f be non trivial Function;

cluster dom f -> non trivial ;

coherence
not dom f is trivial

proof end;

end;

:: from HAHNBAN, 2011.04.26, A.T.

theorem :: FUNCT_1:110

for B being non empty functional set
for f being Function st f = union B holds
( dom f = union { (dom g) where g is Element of B : verum } & rng f = union { (rng g) where g is Element of B : verum } )

proof end;

scheme :: FUNCT_1:sch 5
LambdaS{ F₁() -> set , F₂( object ) -> object } :

ex f being Function st
( dom f = F₁() & ( for X being set st X in F₁() holds
f . X = F₂(X) ) )

proof end;

theorem Th110: :: FUNCT_1:111

for M being set st ( for X being set st X in M holds
X <> {} ) holds
ex f being Function st
( dom f = M & ( for X being set st X in M holds
f . X in X ) )

proof end;

scheme :: FUNCT_1:sch 6
NonUniqBoundFuncEx{ F₁() -> set , F₂() -> set , P₁[ object , object ] } :

ex f being Function st
( dom f = F₁() & rng f c= F₂() & ( for x being object st x in F₁() holds
P₁[x,f . x] ) )

provided

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

proof end;

registration

let f be empty-yielding Function;
let x be object ;

cluster f . x -> empty ;

coherence
f . x is empty

proof end;

end;

:: from PNPROC_1, 2012.02.20, A.T.

theorem :: FUNCT_1:112

for f, g, h being Function st f c= h & g c= h & f misses g holds
dom f misses dom g

proof end;

theorem :: FUNCT_1:113

for Y being set
for f being Function holds Y |` f = f | (f " Y)

proof end;

registration

let X be set ;
let x be Element of X;

reduce (id X) . x to x;

reducibility
(id X) . x = x

proof end;

end;

theorem :: FUNCT_1:114

for f, g being Function st rng f c= rng g holds
for x being object st x in dom f holds
ex y being object st
( y in dom g & f . x = g . y )

proof end;