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


begin

definition
let X be set ;
attrX 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;

:: 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 for set ;
coherence
 for b1 being set st b1 is empty holds
b1 is Function-like
proofend;
end;

registration
cluster Relation-like Function-like for set ;
existence
 ex b1 being Relation st b1 is Function-like
proofend;
end;

definition
mode Function is Function-like Relation;
end;

registration
let a, b be set ;
cluster{[a,b]} ->  Function-like ;
coherence
 {[a,b]} is Function-like
proofend;
end;

scheme :: FUNCT_1:sch 1
GraphFunc{ F1() ->  set , P1[ set , set ] } :
 ex f being Function st
for x, y being set holds
( [x,y] in f iff ( x in F1() & P1[x,y] ) )
provided
A1: for x, y1, y2 being set st P1[x,y1] & P1[x,y2] holds
y1 = y2
proofend;

definition
let f be Function;
let x be set ;
funcf . 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 b1 being set st [x,b1] in f ) & ( not x in dom f implies ex b1 being set st b1 = {} ) ) by XTUPLE_0:def_12;
uniqueness
 for b1, b2 being set holds
( ( x in dom f & [x,b1] in f & [x,b2] in f implies b1 = b2 ) & ( not x in dom f & b1 = {} & b2 = {} implies b1 = b2 ) ) by Def1;
consistency
 for b1 being set holds verum ;
end;

:: deftheorem Def2 defines . FUNCT_1:def_2_:_
 for f being Function
for x, b3 being set holds
( ( x in dom f implies ( b3 = f . x iff [x,b3] in f ) ) & ( not x in dom f implies ( b3 = f . x iff b3 = {} ) ) );

theorem Th1: :: FUNCT_1:1
for x, y being set
for f being Function holds
( [x,y] in f iff ( x in dom f & y = f . x ) )
proofend;

theorem Th2: :: FUNCT_1:2
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
proofend;

definition
let f be Function;
redefine func rng f means :Def3: :: FUNCT_1:def 3
 for y being set holds
( y in it iff ex x being set st
( x in dom f & y = f . x ) );
compatibility
 for b1 being set holds
( b1 = rng f iff for y being set holds
( y in b1 iff ex x being set st
( x in dom f & y = f . x ) ) )
proofend;
end;

:: deftheorem Def3 defines rng FUNCT_1:def_3_:_
 for f being Function
for b2 being set holds
( b2 = rng f iff for y being set holds
( y in b2 iff ex x being set st
( x in dom f & y = f . x ) ) );

theorem :: FUNCT_1:3
for x being set
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 set
for f being Function st dom f = {x} holds
rng f = {(f . x)}
proofend;

scheme :: FUNCT_1:sch 2
FuncEx{ F1() ->  set , P1[ set , set ] } :
 ex f being Function st
( dom f = F1() & ( for x being set st x in F1() holds
P1[x,f . x] ) )
provided
A1: for x, y1, y2 being set st x in F1() & P1[x,y1] & P1[x,y2] holds
y1 = y2 and
A2: for x being set st x in F1() holds
ex y being set st P1[x,y]
proofend;

scheme :: FUNCT_1:sch 3
Lambda{ F1() ->  set , F2( set ) ->  set } :
 ex f being Function st
( dom f = F1() & ( for x being set st x in F1() holds
f . x = F2(x) ) )
proofend;

theorem Th5: :: FUNCT_1:5
for X being set st X <> {} holds
for y being set ex f being Function st
( dom f = X &amp; rng f = {y} )
proofend;

theorem :: FUNCT_1:6
for X being set st ( for f, g being Function st dom f = X &amp; dom g = X holds
f = g ) holds
X = {}
proofend;

theorem :: FUNCT_1:7
for y being set
for f, g being Function st dom f = dom g &amp; rng f = {y} &amp; rng g = {y} holds
f = g
proofend;

theorem :: FUNCT_1:8
for Y, X being set st ( Y <> {} or X = {} ) holds
ex f being Function st
( X = dom f &amp; rng f c= Y )
proofend;

theorem :: FUNCT_1:9
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 &amp; y = f . x ) ) holds
Y c= rng f
proofend;

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

registration
let f, g be Function;
clusterg * f ->  Function-like ;
coherence
 g * f is Function-like
proofend;
end;

theorem :: FUNCT_1:10
for f, g, h being Function st ( for x being set holds
( x in dom h iff ( x in dom f &amp; f . x in dom g ) ) ) &amp; ( for x being set st x in dom h holds
h . x = g . (f . x) ) holds
h = g * f
proofend;

theorem Th11: :: FUNCT_1:11
for x being set
for g, f being Function holds
( x in dom (g * f) iff ( x in dom f &amp; f . x in dom g ) )
proofend;

theorem Th12: :: FUNCT_1:12
for x being set
for g, f being Function st x in dom (g * f) holds
(g * f) . x = g . (f . x)
proofend;

theorem Th13: :: FUNCT_1:13
for x being set
for f, g being Function st x in dom f holds
(g * f) . x = g . (f . x)
proofend;

theorem :: FUNCT_1:14
for z being set
for g, f being Function st z in rng (g * f) holds
z in rng g
proofend;

theorem Th15: :: FUNCT_1:15
for g, f being Function st dom (g * f) = dom f holds
rng f c= dom g
proofend;

theorem :: FUNCT_1:16
for Y being set
for f being Function st rng f c= Y &amp; ( for g, h being Function st dom g = Y &amp; dom h = Y &amp; g * f = h * f holds
g = h ) holds
Y = rng f
proofend;

registration
let X be set ;
cluster id X ->  Function-like ;
coherence
 id X is Function-like
proofend;
end;

theorem Th17: :: FUNCT_1:17
for X being set
for f being Function holds
( f = id X iff ( dom f = X &amp; ( for x being set st x in X holds
f . x = x ) ) )
proofend;

theorem :: FUNCT_1:18
for x, X being set 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
proofend;

theorem :: FUNCT_1:20
for x, X being set
for f being Function st x in (dom f) /\ X holds
f . x = (f * (id X)) . x
proofend;

theorem :: FUNCT_1:21
for x, Y being set
for f being Function holds
( x in dom ((id Y) * f) iff ( x in dom f &amp; f . x in Y ) )
proofend;

theorem :: FUNCT_1:22
for X, Y being set holds (id X) * (id Y) = id (X /\ Y)
proofend;

theorem Th23: :: FUNCT_1:23
for f, g being Function st rng f = dom g &amp; g * f = f holds
g = id (dom g)
proofend;

definition
let f be Function;
attrf is one-to-one  means :Def4: :: FUNCT_1:def 4
 for x1, x2 being set st x1 in dom f &amp; x2 in dom f &amp; 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 set st x1 in dom f &amp; x2 in dom f &amp; f . x1 = f . x2 holds
x1 = x2 );

theorem Th24: :: FUNCT_1:24
for f, g being Function st f is one-to-one &amp; g is one-to-one holds
g * f is one-to-one
proofend;

theorem Th25: :: FUNCT_1:25
for g, f being Function st g * f is one-to-one &amp; rng f c= dom g holds
f is one-to-one
proofend;

theorem :: FUNCT_1:26
for g, f being Function st g * f is one-to-one &amp; rng f = dom g holds
( f is one-to-one &amp; g is one-to-one )
proofend;

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 &amp; rng h c= dom f &amp; dom g = dom h &amp; f * g = f * h holds
g = h )
proofend;

theorem :: FUNCT_1:28
for X being set
for f, g being Function st dom f = X &amp; dom g = X &amp; rng g c= X &amp; f is one-to-one &amp; f * g = f holds
g = id X
proofend;

theorem :: FUNCT_1:29
for g, f being Function st rng (g * f) = rng g &amp; g is one-to-one holds
dom g c= rng f
proofend;

registration
let X be set ;
cluster id X ->  one-to-one ;
coherence
 id X is one-to-one
proofend;
end;

theorem :: FUNCT_1:30
canceled;

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

registration
cluster empty Relation-like Function-like  ->  one-to-one for set ;
coherence
 for b1 being Function st b1 is empty holds
b1 is one-to-one
proofend;
end;

registration
cluster Relation-like Function-like one-to-one for set ;
existence
 ex b1 being Function st b1 is one-to-one
proofend;
end;

registration
let f be one-to-one Function;
clusterf ~  ->  Function-like ;
coherence
 f ~ is Function-like
proofend;
end;

definition
let f be Function;
assume A1: f is one-to-one ;
funcf "  ->  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 Th32: :: 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 &amp; ( for y, x being set holds
( y in rng f &amp; x = g . y iff ( x in dom f &amp; y = f . x ) ) ) ) )
proofend;

theorem Th33: :: FUNCT_1:33
for f being Function st f is one-to-one holds
( rng f = dom (f ") &amp; dom f = rng (f ") )
proofend;

theorem Th34: :: FUNCT_1:34
for x being set
for f being Function st f is one-to-one &amp; x in dom f holds
( x = (f ") . (f . x) &amp; x = ((f ") * f) . x )
proofend;

theorem Th35: :: FUNCT_1:35
for y being set
for f being Function st f is one-to-one &amp; y in rng f holds
( y = f . ((f ") . y) &amp; y = (f * (f ")) . y )
proofend;

theorem Th36: :: FUNCT_1:36
for f being Function st f is one-to-one holds
( dom ((f ") * f) = dom f &amp; rng ((f ") * f) = dom f )
proofend;

theorem Th37: :: FUNCT_1:37
for f being Function st f is one-to-one holds
( dom (f * (f ")) = rng f &amp; rng (f * (f ")) = rng f )
proofend;

theorem :: FUNCT_1:38
for f, g being Function st f is one-to-one &amp; dom f = rng g &amp; rng f = dom g &amp; ( for x, y being set st x in dom f &amp; y in dom g holds
( f . x = y iff g . y = x ) ) holds
g = f "
proofend;

theorem Th39: :: FUNCT_1:39
for f being Function st f is one-to-one holds
( (f ") * f = id (dom f) &amp; f * (f ") = id (rng f) )
proofend;

theorem Th40: :: FUNCT_1:40
for f being Function st f is one-to-one holds
f " is one-to-one
proofend;

registration
let f be one-to-one Function;
clusterf "  ->  one-to-one ;
coherence
 f " is one-to-one by Th40;
let g be one-to-one Function;
clusterg * f ->  one-to-one ;
coherence
 g * f is one-to-one by Th24;
end;

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

theorem Th41: :: FUNCT_1:41
for f, g being Function st f is one-to-one &amp; rng f = dom g &amp; g * f = id (dom f) holds
g = f "
proofend;

theorem :: FUNCT_1:42
for f, g being Function st f is one-to-one &amp; rng g = dom f &amp; f * g = id (rng f) holds
g = f "
proofend;

theorem :: FUNCT_1:43
for f being Function st f is one-to-one holds
(f ") " = f
proofend;

theorem :: FUNCT_1:44
for f, g being Function st f is one-to-one &amp; g is one-to-one holds
(g * f) " = (f ") * (g ")
proofend;

theorem :: FUNCT_1:45
for X being set holds (id X) " = id X
proofend;

registration
let f be Function;
let X be set ;
clusterf | X ->  Function-like ;
coherence
 f | X is Function-like
proofend;
end;

theorem :: FUNCT_1:46
for X being set
for g, f being Function st dom g = (dom f) /\ X &amp; ( for x being set st x in dom g holds
g . x = f . x ) holds
g = f | X
proofend;

theorem Th47: :: FUNCT_1:47
for x, X being set
for f being Function st x in dom (f | X) holds
(f | X) . x = f . x
proofend;

theorem Th48: :: FUNCT_1:48
for x, X being set
for f being Function st x in (dom f) /\ X holds
(f | X) . x = f . x
proofend;

theorem Th49: :: FUNCT_1:49
for x, X being set
for f being Function st x in X holds
(f | X) . x = f . x
proofend;

theorem :: FUNCT_1:50
for x, X being set
for f being Function st x in dom f &amp; x in X holds
f . x in rng (f | X)
proofend;

theorem :: FUNCT_1:51
for X, Y being set
for f being Function st X c= Y holds
( (f | X) | Y = f | X &amp; (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
proofend;

registration
let Y be set ;
let f be Function;
clusterY |` f ->  Function-like ;
coherence
 Y |` f is Function-like
proofend;
end;

theorem Th53: :: FUNCT_1:53
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 &amp; f . x in Y ) ) ) &amp; ( for x being set st x in dom g holds
g . x = f . x ) ) )
proofend;

theorem :: FUNCT_1:54
for x, Y being set
for f being Function holds
( x in dom (Y |` f) iff ( x in dom f &amp; f . x in Y ) ) by Th53;

theorem :: FUNCT_1:55
for x, Y being set
for f being Function st x in dom (Y |` f) holds
(Y |` f) . x = f . x by Th53;

theorem :: FUNCT_1:56
for Y being set
for f being Function holds dom (Y |` f) c= dom f
proofend;

theorem :: FUNCT_1:57
for X, Y being set
for f being Function st X c= Y holds
( Y |` (X |` f) = X |` f &amp; 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
proofend;

definition
let f be Function;
let X be set ;
redefine func f .: X means :Def6: :: FUNCT_1:def 6
 for y being set holds
( y in it iff ex x being set st
( x in dom f &amp; x in X &amp; y = f . x ) );
compatibility
 for b1 being set holds
( b1 = f .: X iff for y being set holds
( y in b1 iff ex x being set st
( x in dom f &amp; x in X &amp; y = f . x ) ) )
proofend;
end;

:: deftheorem Def6 defines .: FUNCT_1:def_6_:_
 for f being Function
for X being set
for b3 being set holds
( b3 = f .: X iff for y being set holds
( y in b3 iff ex x being set st
( x in dom f &amp; x in X &amp; y = f . x ) ) );

theorem Th59: :: FUNCT_1:59
for x being set
for f being Function st x in dom f holds
Im (f,x) = {(f . x)}
proofend;

theorem :: FUNCT_1:60
for x1, x2 being set
for f being Function st x1 in dom f &amp; x2 in dom f holds
f .: {x1,x2} = {(f . x1),(f . x2)}
proofend;

theorem :: FUNCT_1:61
for Y, X being set
for f being Function holds (Y |` f) .: X c= f .: X
proofend;

theorem Th62: :: 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)
proofend;

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

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

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

theorem :: FUNCT_1:66
for X, Y being set
for f being Function st X misses Y &amp; f is one-to-one holds
f .: X misses f .: Y
proofend;

theorem :: FUNCT_1:67
for Y, X being set
for f being Function holds (Y |` f) .: X = Y /\ (f .: X)
proofend;

definition
let f be Function;
let Y be set ;
redefine func f " Y means :Def7: :: FUNCT_1:def 7
 for x being set holds
( x in it iff ( x in dom f &amp; f . x in Y ) );
compatibility
 for b1 being set holds
( b1 = f " Y iff for x being set holds
( x in b1 iff ( x in dom f &amp; f . x in Y ) ) )
proofend;
end;

:: deftheorem Def7 defines " FUNCT_1:def_7_:_
 for f being Function
for Y being set
for b3 being set holds
( b3 = f " Y iff for x being set holds
( x in b3 iff ( x in dom f &amp; f . x in Y ) ) );

theorem Th68: :: FUNCT_1:68
for Y1, Y2 being set
for f being Function holds f " (Y1 /\ Y2) = (f " Y1) /\ (f " Y2)
proofend;

theorem :: FUNCT_1:69
for Y1, Y2 being set
for f being Function holds f " (Y1 \ Y2) = (f " Y1) \ (f " Y2)
proofend;

theorem :: FUNCT_1:70
for X, Y being set
for R being Relation holds (R | X) " Y = X /\ (R " Y)
proofend;

theorem :: FUNCT_1:71
for f being Function
for A, B being set st A misses B holds
f " A misses f " B
proofend;

theorem Th72: :: FUNCT_1:72
for y being set
for R being Relation holds
( y in rng R iff R " {y} <> {} )
proofend;

theorem :: FUNCT_1:73
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
proofend;

theorem Th74: :: FUNCT_1:74
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 )
proofend;

theorem Th75: :: FUNCT_1:75
for Y being set
for f being Function holds f .: (f " Y) c= Y
proofend;

theorem Th76: :: FUNCT_1:76
for X being set
for R being Relation st X c= dom R holds
X c= R " (R .: X)
proofend;

theorem :: FUNCT_1:77
for Y being set
for f being Function st Y c= rng f holds
f .: (f " Y) = Y
proofend;

theorem :: FUNCT_1:78
for Y being set
for f being Function holds f .: (f " Y) = Y /\ (f .: (dom f))
proofend;

theorem Th79: :: FUNCT_1:79
for X, Y being set
for f being Function holds f .: (X /\ (f " Y)) c= (f .: X) /\ Y
proofend;

theorem :: FUNCT_1:80
for X, Y being set
for f being Function holds f .: (X /\ (f " Y)) = (f .: X) /\ Y
proofend;

theorem :: FUNCT_1:81
for X, Y being set
for R being Relation holds X /\ (R " Y) c= R " ((R .: X) /\ Y)
proofend;

theorem Th82: :: FUNCT_1:82
for X being set
for f being Function st f is one-to-one holds
f " (f .: X) c= X
proofend;

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

theorem :: FUNCT_1:84
for X being set
for f being Function st f is one-to-one holds
f .: X = (f ") " X
proofend;

theorem :: FUNCT_1:85
for Y being set
for f being Function st f is one-to-one holds
f " Y = (f ") .: Y
proofend;

:: SUPLEMENT
theorem :: FUNCT_1:86
for Y being set
for f, g, h being Function st Y = rng f &amp; dom g = Y &amp; dom h = Y &amp; g * f = h * f holds
g = h
proofend;

theorem :: FUNCT_1:87
for X1, X2 being set
for f being Function st f .: X1 c= f .: X2 &amp; X1 c= dom f &amp; f is one-to-one holds
X1 c= X2
proofend;

theorem Th88: :: FUNCT_1:88
for Y1, Y2 being set
for f being Function st f " Y1 c= f " Y2 &amp; Y1 c= rng f holds
Y1 c= Y2
proofend;

theorem :: FUNCT_1:89
for f being Function holds
( f is one-to-one iff for y being set ex x being set st f " {y} c= {x} )
proofend;

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

theorem :: FUNCT_1:91
for X, Y being set
for f being Function st f " X = f " Y &amp; X c= rng f &amp; Y c= rng f holds
X = Y
proofend;

begin

theorem :: FUNCT_1:92
for X being set
for A being Subset of X holds (id X) .: A = A
proofend;

:: from PBOOLE
definition
let f be Function;
redefine attr f is empty-yielding  means :Def8: :: FUNCT_1:def 8
 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 )
proofend;
end;

:: deftheorem Def8 defines empty-yielding FUNCT_1:def_8_:_
 for f being Function holds
( f is empty-yielding iff for x being set 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 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 )
proofend;
end;

:: deftheorem Def9 defines non-empty FUNCT_1:def_9_:_
 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 );

:: new, 2004.08.04
registration
cluster Relation-like non-empty Function-like for set ;
existence
 ex b1 being Function st b1 is non-empty
proofend;
end;

scheme :: FUNCT_1:sch 4
LambdaB{ F1() ->  non empty set , F2( set ) ->  set } :
 ex f being Function st
( dom f = F1() &amp; ( for d being Element of F1() holds f . d = F2(d) ) )
proofend;

:: 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
proofend;
end;

:: from SEQM_3, 2005.12.17, A.T.
definition
let f be Function;
attrf is constant  means :Def10: :: FUNCT_1:def 10
 for x, y being set st x in dom f &amp; 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 set st x in dom f &amp; 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 &amp; f .: A c= B holds
A c= f " B
proofend;

:: 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 &amp; f is one-to-one holds
f " (f .: X) = X
proofend;

:: added, AK 5.02.2007
definition
let f, g be Function;
redefine pred f = g means :: FUNCT_1:def 11
( dom f = dom g &amp; ( for x being set st x in dom f holds
f . x = g . x ) );
compatibility
 ( f = g iff ( dom f = dom g &amp; ( for x being set 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 &amp; ( for x being set 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 b1 being Function st
( b1 is non-empty &amp; not b1 is empty )
proofend;
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;
clustera . i ->  non empty ;
coherence
 not a . i is empty
proofend;
end;

:: missing, 2007.04.13, A.T.
registration
let f be Function;
cluster  ->  Function-like for Element of bool f;
coherence
 for b1 being Subset of f holds b1 is Function-like
proofend;
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 &amp; D c= dom g holds
( f | D = g | D iff for x being set st x in D holds
f . x = g . x )
proofend;

:: 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 &amp; ( for x being set st x in X holds
f . x = g . x ) holds
f | X = g | X
proofend;

:: missing, 2007.10.28, A.T.
theorem Th97: :: FUNCT_1:97
for X being set
for f being Function holds rng (f | {X}) c= {(f . X)}
proofend;

theorem :: FUNCT_1:98
for X being set
for f being Function st X in dom f holds
rng (f | {X}) = {(f . X)}
proofend;

:: from RFUNCT_1, 2008.09.04, A.T.
registration
cluster empty Relation-like Function-like  ->  constant for set ;
coherence
 for b1 being Function st b1 is empty holds
b1 is constant
proofend;
end;

:: from WAYBEL35, 2008.08.04, A.T.
registration
let f be constant Function;
cluster rng f ->  trivial ;
coherence
 rng f is trivial
proofend;
end;

registration
cluster Relation-like Function-like non constant for set ;
existence
 not for b1 being Function holds b1 is constant
proofend;
end;

registration
let f be non constant Function;
cluster rng f ->  non trivial ;
coherence
 not rng f is trivial
proofend;
end;

registration
cluster Relation-like Function-like non constant  ->  non trivial for set ;
coherence
 for b1 being Function st not b1 is constant holds
not b1 is trivial
proofend;
end;

registration
cluster trivial Relation-like Function-like  ->  constant for set ;
coherence
 for b1 being Function st b1 is trivial holds
b1 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
proofend;

theorem :: FUNCT_1:100
for F, G being Function
for X, X1 being set holds (G | X1) * (F | X) = (G * F) | (X /\ (F " X1))
proofend;

theorem :: FUNCT_1:101
for F, G being Function
for X being set holds
( X c= dom (G * F) iff ( X c= dom F &amp; F .: X c= dom G ) )
proofend;

:: from YELLOW_6, 2008.12.26, A.T.
definition
let f be Function;
assume A1: ( not f is empty &amp; f is constant ) ;
func the_value_of f ->  set  means :: FUNCT_1:def 12
 ex x being set st
( x in dom f &amp; it = f . x );
existence
 ex b1 being set ex x being set st
( x in dom f &amp; b1 = f . x )
proofend;
uniqueness
 for b1, b2 being set st ex x being set st
( x in dom f &amp; b1 = f . x ) &amp; ex x being set st
( x in dom f &amp; b2 = f . x ) holds
b1 = b2 by A1, Def10;
end;

:: deftheorem  defines the_value_of FUNCT_1:def_12_:_
 for f being Function st not f is empty &amp; f is constant holds
for b2 being set holds
( b2 = the_value_of f iff ex x being set st
( x in dom f &amp; b2 = 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 b1 being Function st
( b1 is X -defined &amp; b1 is Y -valued )
proofend;
end;

theorem :: FUNCT_1:102
for X being set
for f being b1 -valued Function
for x being set st x in dom f holds
f . x in X
proofend;

:: from FRAENKEL, 2009.05.06, A.K.
definition
let IT be set ;
attrIT is functional  means :Def13: :: FUNCT_1:def 13
 for x being set 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 set st x in IT holds
x is Function );

registration
cluster empty  ->  functional for set ;
coherence
 for b1 being set st b1 is empty holds
b1 is functional
proofend;
let f be Function;
cluster{f} ->  functional ;
coherence
 {f} is functional
proofend;
let g be Function;
cluster{f,g} ->  functional ;
coherence
 {f,g} is functional
proofend;
end;

registration
cluster non empty functional for set ;
existence
 ex b1 being set st
( not b1 is empty &amp; b1 is functional )
proofend;
end;

registration
let P be functional set ;
cluster  ->  Relation-like Function-like for Element of P;
coherence
 for b1 being Element of P holds
( b1 is Function-like &amp; b1 is Relation-like )
proofend;
end;

registration
let A be functional set ;
cluster  ->  functional for Element of bool A;
coherence
 for b1 being Subset of A holds b1 is functional
proofend;
end;

:: new, 2009.09.30, A.T.
definition
let g, f be Function;
attrf is g -compatible  means :Def14: :: FUNCT_1:def 14
 for x being set 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 set 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 &amp; dom f = dom g holds
g is non-empty
proofend;

theorem Th104: :: FUNCT_1:104
for f being Function holds {} is f -compatible
proofend;

registration
let I be set ;
let f be Function;
cluster empty Relation-like I -defined Function-like f -compatible for set ;
existence
 ex b1 being Function st
( b1 is empty &amp; b1 is I -defined &amp; b1 is f -compatible )
proofend;
end;

registration
let X be set ;
let f be Function;
let g be f -compatible Function;
clusterg | X -> f -compatible ;
coherence
 g | X is f -compatible
proofend;
end;

registration
let I be set ;
cluster Relation-like non-empty I -defined Function-like for set ;
existence
 ex b1 being Function st
( b1 is non-empty &amp; b1 is I -defined )
proofend;
end;

theorem Th105: :: FUNCT_1:105
for f being Function
for g being b1 -compatible Function holds dom g c= dom f
proofend;

registration
let X be set ;
let f be X -defined Function;
cluster Relation-like Function-like f -compatible  -> X -defined for set ;
coherence
 for b1 being Function st b1 is f -compatible holds
b1 is X -defined
proofend;
end;

theorem :: FUNCT_1:106
for X, x being set
for f being b1 -valued Function st x in dom f holds
f . x is Element of X
proofend;

:: 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 &amp; A c= dom f holds
(f ") .: (f .: A) = A
proofend;

registration
let A be functional set ;
let x be set ;
let F be A -valued Function;
clusterF . x ->  Relation-like Function-like ;
coherence
 ( F . x is Function-like &amp; F . x is Relation-like )
proofend;
end;

:: missing, 2011.03.06, A.T.
theorem Th108: :: FUNCT_1:108
for x, X being set
for f being Function st x in X &amp; x in dom f holds
f . x in f .: X
proofend;

theorem :: FUNCT_1:109
for X being set
for f being Function st X <> {} &amp; X c= dom f holds
f .: X <> {}
proofend;

registration
let f be non trivial Function;
cluster dom f ->  non trivial ;
coherence
 not dom f is trivial
proofend;
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  }  &amp; rng f = union  {  (rng g) where g is Element of B : verum  }  )
proofend;

theorem Th111: :: 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 &amp; ( for X being set st X in M holds
f . X in X ) )
proofend;

scheme :: FUNCT_1:sch 5
NonUniqBoundFuncEx{ F1() ->  set , F2() ->  set , P1[ set , set ] } :
 ex f being Function st
( dom f = F1() &amp; rng f c= F2() &amp; ( for x being set st x in F1() holds
P1[x,f . x] ) )
provided
A1: for x being set st x in F1() holds
ex y being set st
( y in F2() &amp; P1[x,y] )
proofend;

registration
let f be empty-yielding Function;
let x be set ;
clusterf . x ->  empty ;
coherence
 f . x is empty
proofend;
end;