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


begin

definition
let X, Y be set ;
let R be Relation of X,Y;
attrR is quasi_total  means :Def1: :: FUNCT_2:def 1
X = dom R if Y <> {}
otherwise R = {} ;
consistency
 verum ;
end;

:: deftheorem Def1 defines quasi_total FUNCT_2:def_1_:_
 for X, Y being set
for R being Relation of X,Y holds
( ( Y <> {} implies ( R is quasi_total iff X = dom R ) ) &amp; ( not Y <> {} implies ( R is quasi_total iff R = {} ) ) );

registration
let X, Y be set ;
cluster Relation-like X -defined Y -valued Function-like quasi_total for Element of bool [:X,Y:];
existence
 ex b1 being PartFunc of X,Y st b1 is quasi_total
proofend;
end;

registration
let X, Y be set ;
cluster total  ->  quasi_total for Element of bool [:X,Y:];
coherence
 for b1 being Relation of X,Y st b1 is total holds
b1 is quasi_total
proofend;
end;

definition
let X, Y be set ;
mode Function of X,Y is quasi_total PartFunc of X,Y;
end;

registration
let X be empty set ;
let Y be set ;
cluster quasi_total  ->  total for Element of bool [:X,Y:];
coherence
 for b1 being Relation of X,Y st b1 is quasi_total holds
b1 is total ;
end;

registration
let X be set ;
let Y be non empty set ;
cluster quasi_total  ->  total for Element of bool [:X,Y:];
coherence
 for b1 being Relation of X,Y st b1 is quasi_total holds
b1 is total
proofend;
end;

registration
let X be set ;
cluster quasi_total  ->  total for Element of bool [:X,X:];
coherence
 for b1 being Relation of X,X st b1 is quasi_total holds
b1 is total
proofend;
end;

theorem :: FUNCT_2:1
for f being Function holds f is Function of (dom f),(rng f)
proofend;

theorem Th2: :: FUNCT_2:2
for Y being set
for f being Function st rng f c= Y holds
f is Function of (dom f),Y
proofend;

theorem :: FUNCT_2:3
for X, Y being set
for f being Function st dom f = X &amp; ( for x being set st x in X holds
f . x in Y ) holds
f is Function of X,Y
proofend;

theorem Th4: :: FUNCT_2:4
for X, Y, x being set
for f being Function of X,Y st Y <> {} &amp; x in X holds
f . x in rng f
proofend;

theorem Th5: :: FUNCT_2:5
for X, Y, x being set
for f being Function of X,Y st Y <> {} &amp; x in X holds
f . x in Y
proofend;

theorem :: FUNCT_2:6
for X, Y, Z being set
for f being Function of X,Y st ( Y = {} implies X = {} ) &amp; rng f c= Z holds
f is Function of X,Z
proofend;

theorem :: FUNCT_2:7
for X, Y, Z being set
for f being Function of X,Y st ( Y = {} implies X = {} ) &amp; Y c= Z holds
f is Function of X,Z by RELSET_1:7;

scheme :: FUNCT_2:sch 1
FuncEx1{ F1() ->  set , F2() ->  set , P1[ set , set ] } :
 ex f being Function of F1(),F2() st
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;

scheme :: FUNCT_2:sch 2
Lambda1{ F1() ->  set , F2() ->  set , F3( set ) ->  set } :
 ex f being Function of F1(),F2() st
for x being set st x in F1() holds
f . x = F3(x)
provided
A1: for x being set st x in F1() holds
F3(x) in F2()
proofend;

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 &amp; dom f = X &amp; rng f c= Y ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ex f being Function st
( x = f &amp; dom f = X &amp; rng f c= Y ) )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ex f being Function st
( x = f &amp; dom f = X &amp; rng f c= Y ) ) ) &amp; ( for x being set holds
( x in b2 iff ex f being Function st
( x = f &amp; dom f = X &amp; rng f c= Y ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines Funcs FUNCT_2:def_2_:_
 for X, Y, b3 being set holds
( b3 = Funcs (X,Y) iff for x being set holds
( x in b3 iff ex f being Function st
( x = f &amp; dom f = X &amp; rng f c= Y ) ) );

theorem Th8: :: FUNCT_2:8
for X, Y being set
for f being Function of X,Y st ( Y = {} implies X = {} ) holds
f in Funcs (X,Y)
proofend;

theorem :: FUNCT_2:9
for X being set
for f being Function of X,X holds f in Funcs (X,X) by Th8;

registration
let X be set ;
let Y be non empty set ;
cluster Funcs (X,Y) ->  non empty ;
coherence
 not Funcs (X,Y) is empty by Th8;
end;

registration
let X be set ;
cluster Funcs (X,X) ->  non empty ;
coherence
 not Funcs (X,X) is empty by Th8;
end;

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

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

theorem Th11: :: FUNCT_2:11
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 &amp; f . x = y )
proofend;

theorem Th12: :: FUNCT_2:12
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
proofend;

theorem Th13: :: FUNCT_2:13
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
proofend;

theorem :: FUNCT_2:14
for X, Y, Z being set
for f being Function of X,Y
for g being Function of Y,Z st Z <> {} &amp; rng f = Y &amp; rng g = Z holds
rng (g * f) = Z
proofend;

theorem Th15: :: FUNCT_2:15
for X, Y, x being set
for f being Function of X,Y
for g being Function st Y <> {} &amp; x in X holds
(g * f) . x = g . (f . x)
proofend;

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

theorem :: FUNCT_2:17
for X, Y being set
for f being Relation of X,Y holds
( (id X) * f = f &amp; f * (id Y) = f )
proofend;

theorem :: FUNCT_2:18
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
proofend;

theorem :: FUNCT_2:19
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 &amp; x2 in X &amp; f . x1 = f . x2 holds
x1 = x2 )
proofend;

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 = {} implies Y = {} ) &amp; g * f is one-to-one holds
f is one-to-one
proofend;

theorem :: FUNCT_2:21
for X, Y being set
for f being Function of X,Y st X <> {} &amp; 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 )
proofend;

theorem :: FUNCT_2:22
for X, Y, Z being set
for f being Function of X,Y
for g being Function of Y,Z st Z <> {} &amp; rng (g * f) = Z &amp; g is one-to-one holds
rng f = Y
proofend;

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

:: deftheorem Def3 defines onto FUNCT_2:def_3_:_
 for Y being set
for f being b1 -valued Relation holds
( f is onto iff rng f = Y );

theorem :: FUNCT_2:23
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 &amp; g is onto )
proofend;

theorem :: FUNCT_2:24
for X, Y, Z being set
for f being Function of X,Y
for g being Function of Y,Z st ( Z = {} implies Y = {} ) &amp; g * f is one-to-one &amp; rng f = Y holds
( f is one-to-one &amp; g is one-to-one )
proofend;

theorem Th25: :: FUNCT_2:25
for X, Y being set
for f being Function of X,Y st f is one-to-one &amp; rng f = Y holds
f " is Function of Y,X
proofend;

theorem :: FUNCT_2:26
for X, Y, x being set
for f being Function of X,Y st Y <> {} &amp; f is one-to-one &amp; x in X holds
(f ") . (f . x) = x
proofend;

theorem :: FUNCT_2:27
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 &amp; g is onto holds
g * f is onto
proofend;

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

theorem :: FUNCT_2:29
for X, Y being set
for f being Function of X,Y st Y <> {} &amp; rng f = Y &amp; f is one-to-one holds
( (f ") * f = id X &amp; f * (f ") = id Y )
proofend;

theorem :: FUNCT_2:30
for X, Y being set
for f being Function of X,Y
for g being Function of Y,X st X <> {} &amp; Y <> {} &amp; rng f = Y &amp; g * f = id X &amp; f is one-to-one holds
g = f "
proofend;

theorem :: FUNCT_2:31
for X, Y being set
for f being Function of X,Y st Y <> {} &amp; ex g being Function of Y,X st g * f = id X holds
f is one-to-one
proofend;

theorem Th32: :: FUNCT_2:32
for X, Y, Z being set
for f being Function of X,Y st ( Y = {} implies X = {} ) &amp; Z c= X holds
f | Z is Function of Z,Y
proofend;

theorem :: FUNCT_2:33
for X, Y, Z being set
for f being Function of X,Y st X c= Z holds
f | Z = f by RELSET_1:19;

theorem :: FUNCT_2:34
for X, Y, x, Z being set
for f being Function of X,Y st Y <> {} &amp; x in X &amp; f . x in Z holds
(Z |` f) . x = f . x
proofend;

theorem :: FUNCT_2:35
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 &amp; x in P &amp; y = f . x ) holds
y in f .: P
proofend;

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

theorem :: FUNCT_2:37
canceled;

theorem :: FUNCT_2:38
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 &amp; f . x in Q ) )
proofend;

theorem :: FUNCT_2:39
for X, Y, Q being set
for f being PartFunc of X,Y holds f " Q c= X ;

theorem Th40: :: FUNCT_2:40
for X, Y being set
for f being Function of X,Y st ( Y = {} implies X = {} ) holds
f " Y = X
proofend;

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

theorem Th42: :: FUNCT_2:42
for X, Y, P being set
for f being Function of X,Y st ( Y = {} implies X = {} ) &amp; P c= X holds
P c= f " (f .: P)
proofend;

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

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

theorem :: FUNCT_2:45
for Y, P being set
for f being Function of {},Y holds f .: P = {} ;

theorem :: FUNCT_2:46
for Y, Q being set
for f being Function of {},Y holds f " Q = {} ;

theorem :: FUNCT_2:47
for x, Y being set
for f being Function of {x},Y st Y <> {} holds
f . x in Y
proofend;

theorem Th48: :: FUNCT_2:48
for x, Y being set
for f being Function of {x},Y st Y <> {} holds
rng f = {(f . x)}
proofend;

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

theorem Th50: :: FUNCT_2:50
for X, y, x being set
for f being Function of X,{y} st x in X holds
f . x = y
proofend;

theorem Th51: :: FUNCT_2:51
for X, y being set
for f1, f2 being Function of X,{y} holds f1 = f2
proofend;

theorem Th52: :: FUNCT_2:52
for X being set
for f being Function of X,X holds dom f = X
proofend;

registration
let X, Y be set ;
let f be quasi_total PartFunc of X,Y;
let g be quasi_total PartFunc of X,X;
clusterg * f ->  quasi_total for PartFunc of X,Y;
coherence
 for b1 being PartFunc of X,Y st b1 = f * g holds
b1 is quasi_total
proofend;
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;
clusterg * f ->  quasi_total for PartFunc of X,Y;
coherence
 for b1 being PartFunc of X,Y st b1 = f * g holds
b1 is quasi_total
proofend;
end;

theorem Th53: :: FUNCT_2:53
for X being set
for f, g being Relation of X,X st rng f = X &amp; rng g = X holds
rng (g * f) = X
proofend;

theorem :: FUNCT_2:54
for X being set
for f, g being Function of X,X st g * f = f &amp; rng f = X holds
g = id X
proofend;

theorem :: FUNCT_2:55
for X being set
for f, g being Function of X,X st f * g = f &amp; f is one-to-one holds
g = id X
proofend;

theorem Th56: :: FUNCT_2:56
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 &amp; x2 in X &amp; f . x1 = f . x2 holds
x1 = x2 )
proofend;

definition
let X, Y be set ;
let f be X -defined Y -valued Function;
attrf is bijective  means :Def4: :: FUNCT_2:def 4
( f is one-to-one &amp; f is onto );
end;

:: deftheorem Def4 defines bijective FUNCT_2:def_4_:_
 for X, Y being set
for f being b1 -defined b2 -valued Function holds
( f is bijective iff ( f is one-to-one &amp; f is onto ) );

registration
let X, Y be set ;
cluster Function-like bijective  ->  one-to-one onto for Element of bool [:X,Y:];
coherence
 for b1 being PartFunc of X,Y st b1 is bijective holds
( b1 is one-to-one &amp; b1 is onto ) by Def4;
cluster Function-like one-to-one onto  ->  bijective for Element of bool [:X,Y:];
coherence
 for b1 being PartFunc of X,Y st b1 is one-to-one &amp; b1 is onto holds
b1 is bijective by Def4;
end;

registration
let X be set ;
cluster Relation-like X -defined X -valued Function-like total quasi_total bijective for Element of bool [:X,X:];
existence
 ex b1 being Function of X,X st b1 is bijective
proofend;
end;

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

theorem Th57: :: FUNCT_2:57
for X being set
for f being Function of X,X st f is one-to-one &amp; rng f = X holds
f is Permutation of X
proofend;

theorem :: FUNCT_2:58
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 &amp; x2 in X &amp; f . x1 = f . x2 holds
x1 = x2 by Th56;

registration
let X be set ;
let f, g be onto PartFunc of X,X;
clusterg * f ->  onto for PartFunc of X,X;
coherence
 for b1 being PartFunc of X,X st b1 = f * g holds
b1 is onto
proofend;
end;

registration
let X be set ;
let f, g be bijective Function of X,X;
clusterf * g ->  bijective for Function of X,X;
coherence
 for b1 being Function of X,X st b1 = g * f holds
b1 is bijective ;
end;

registration
let X be set ;
cluster reflexive Function-like total quasi_total  ->  bijective for Element of bool [:X,X:];
coherence
 for b1 being Function of X,X st b1 is reflexive &amp; b1 is total holds
b1 is bijective
proofend;
end;

definition
let X be set ;
let f be Permutation of X;
:: original:"
redefine funcf "  ->  Permutation of X;
coherence
 f " is Permutation of X
proofend;
end;

theorem :: FUNCT_2:59
for X being set
for f, g being Permutation of X st g * f = g holds
f = id X
proofend;

theorem :: FUNCT_2:60
for X being set
for f, g being Permutation of X st g * f = id X holds
g = f "
proofend;

theorem :: FUNCT_2:61
for X being set
for f being Permutation of X holds
( (f ") * f = id X &amp; f * (f ") = id X )
proofend;

theorem Th62: :: FUNCT_2:62
for X, P being set
for f being Permutation of X st P c= X holds
( f .: (f " P) = P &amp; f " (f .: P) = P )
proofend;

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;
clusterf * g ->  quasi_total for PartFunc of X,Z;
coherence
 for b1 being PartFunc of X,Z st b1 = g * f holds
b1 is quasi_total by Th13;
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 funcf . c ->  Element of D;
coherence
 f . c is Element of D
proofend;
end;

scheme :: FUNCT_2:sch 3
FuncExD{ F1() ->  non empty set , F2() ->  non empty set , P1[ set , set ] } :
 ex f being Function of F1(),F2() st
for x being Element of F1() holds P1[x,f . x]
provided
A1: for x being Element of F1() ex y being Element of F2() st P1[x,y]
proofend;

scheme :: FUNCT_2:sch 4
LambdaD{ F1() ->  non empty set , F2() ->  non empty set , F3( Element of F1()) ->  Element of F2() } :
 ex f being Function of F1(),F2() st
for x being Element of F1() holds f . x = F3(x)
proofend;

theorem Th63: :: FUNCT_2:63
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
proofend;

theorem Th64: :: FUNCT_2:64
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 &amp; x in P &amp; y = f . x )
proofend;

theorem :: FUNCT_2:65
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 &amp; y = f . c )
proofend;

begin

theorem Th66: :: FUNCT_2:66
for X, Y, f being set st f in Funcs (X,Y) holds
f is Function of X,Y
proofend;

scheme :: FUNCT_2:sch 5
Lambda1C{ F1() ->  set , F2() ->  set , P1[ set ], F3( set ) ->  set , F4( set ) ->  set } :
 ex f being Function of F1(),F2() st
for x being set st x in F1() holds
( ( P1[x] implies f . x = F3(x) ) &amp; ( P1[x] implies f . x = F4(x) ) )
provided
A1: for x being set st x in F1() holds
( ( P1[x] implies F3(x) in F2() ) &amp; ( P1[x] implies F4(x) in F2() ) )
proofend;

theorem :: FUNCT_2:67
for X, Y being set
for f being PartFunc of X,Y st dom f = X holds
f is Function of X,Y
proofend;

theorem :: FUNCT_2:68
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:69
for X, Y being set
for f being PartFunc of X,Y st ( Y = {} implies X = {} ) &amp; f is Function of X,Y holds
f is total ;

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

registration
let X be set ;
let f be Function of X,X;
cluster<:f,X,X:> ->  total ;
coherence
 <:f,X,X:> is total ;
end;

theorem Th71: :: FUNCT_2:71
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
proofend;

theorem :: FUNCT_2:72
for X, Y being set holds Funcs (X,Y) c= PFuncs (X,Y)
proofend;

theorem :: FUNCT_2:73
for X, Y being set
for f, g being Function of X,Y st ( Y = {} implies X = {} ) &amp; f tolerates g holds
f = g by PARTFUN1:66;

theorem :: FUNCT_2:74
for X being set
for f, g being Function of X,X st f tolerates g holds
f = g by PARTFUN1:66;

theorem Th75: :: FUNCT_2:75
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 )
proofend;

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

theorem Th77: :: FUNCT_2:77
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
proofend;

theorem :: FUNCT_2:78
for X being set
for f, g being PartFunc of X,X
for h being Function of X,X st f tolerates h &amp; g tolerates h holds
f tolerates g by PARTFUN1:67;

theorem :: FUNCT_2:79
for X, Y being set
for f, g being PartFunc of X,Y st ( Y = {} implies X = {} ) &amp; f tolerates g holds
ex h being Function of X,Y st
( f tolerates h &amp; g tolerates h )
proofend;

theorem :: FUNCT_2:80
for X, Y being set
for f being PartFunc of X,Y
for g being Function of X,Y st ( Y = {} implies X = {} ) &amp; f tolerates g holds
g in TotFuncs f by PARTFUN1:def_5;

theorem :: FUNCT_2:81
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 PARTFUN1:def_5;

theorem Th82: :: FUNCT_2:82
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
proofend;

theorem :: FUNCT_2:83
for X, Y being set
for f being PartFunc of X,Y holds TotFuncs f c= Funcs (X,Y)
proofend;

theorem :: FUNCT_2:84
for X, Y being set holds TotFuncs <:{},X,Y:> = Funcs (X,Y)
proofend;

theorem :: FUNCT_2:85
for X, Y being set
for f being Function of X,Y st ( Y = {} implies X = {} ) holds
TotFuncs <:f,X,Y:> = {f} by PARTFUN1:72;

theorem :: FUNCT_2:86
for X being set
for f being Function of X,X holds TotFuncs <:f,X,X:> = {f} by PARTFUN1:72;

theorem :: FUNCT_2:87
for X, y being set
for f being PartFunc of X,{y}
for g being Function of X,{y} holds TotFuncs f = {g}
proofend;

theorem :: FUNCT_2:88
for X, Y being set
for f, g being PartFunc of X,Y st g c= f holds
TotFuncs f c= TotFuncs g
proofend;

theorem Th89: :: FUNCT_2:89
for X, Y being set
for f, g being PartFunc of X,Y st dom g c= dom f &amp; TotFuncs f c= TotFuncs g holds
g c= f
proofend;

theorem Th90: :: FUNCT_2:90
for X, Y being set
for f, g being PartFunc of X,Y st TotFuncs f c= TotFuncs g &amp; ( for y being set holds Y <> {y} ) holds
g c= f
proofend;

theorem :: FUNCT_2:91
for X, Y being set
for f, g being PartFunc of X,Y st ( for y being set holds Y <> {y} ) &amp; TotFuncs f = TotFuncs g holds
f = g
proofend;

:: from WAYBEL_1
registration
let A, B be non empty set ;
cluster Function-like quasi_total  ->  non empty for Element of bool [:A,B:];
coherence
 for b1 being Function of A,B holds not b1 is empty by Def1, RELAT_1:38;
end;

begin

scheme :: FUNCT_2:sch 6
LambdaSep1{ F1() ->  non empty set , F2() ->  non empty set , F3() ->  Element of F1(), F4() ->  Element of F2(), F5( set ) ->  Element of F2() } :
 ex f being Function of F1(),F2() st
( f . F3() = F4() &amp; ( for x being Element of F1() st x <> F3() holds
f . x = F5(x) ) )
proofend;

scheme :: FUNCT_2:sch 7
LambdaSep2{ F1() ->  non empty set , F2() ->  non empty set , F3() ->  Element of F1(), F4() ->  Element of F1(), F5() ->  Element of F2(), F6() ->  Element of F2(), F7( set ) ->  Element of F2() } :
 ex f being Function of F1(),F2() st
( f . F3() = F5() &amp; f . F4() = F6() &amp; ( for x being Element of F1() st x <> F3() &amp; x <> F4() holds
f . x = F7(x) ) )
provided
A1: F3() <> F4()
proofend;

:: from ALTCAT_1, PRALG_3
theorem :: FUNCT_2:92
for A, B being set
for f being Function st f in Funcs (A,B) holds
( dom f = A &amp; rng f c= B )
proofend;

scheme :: FUNCT_2:sch 8
FunctRealEx{ F1() ->  non empty set , F2() ->  set , F3( set ) ->  set } :
 ex f being Function of F1(),F2() st
for x being Element of F1() holds f . x = F3(x)
provided
A1: for x being Element of F1() holds F3(x) in F2()
proofend;

scheme :: FUNCT_2:sch 9
KappaMD{ F1() ->  non empty set , F2() ->  non empty set , F3( set ) ->  set } :
 ex f being Function of F1(),F2() st
for x being Element of F1() holds f . x = F3(x)
provided
A1: for x being Element of F1() holds F3(x) is Element of F2()
proofend;

definition
let A, B, C be non empty set ;
let f be Function of A,[:B,C:];
:: original:pr1
redefine func pr1 f ->  Function of A,B means :Def5: :: FUNCT_2:def 5
 for x being Element of A holds it . x = (f . x) `1 ;
coherence
 pr1 f is Function of A,B
proofend;
compatibility
 for b1 being Function of A,B holds
( b1 = pr1 f iff for x being Element of A holds b1 . x = (f . x) `1 )
proofend;
:: original:pr2
redefine func pr2 f ->  Function of A,C means :Def6: :: FUNCT_2:def 6
 for x being Element of A holds it . x = (f . x) `2 ;
coherence
 pr2 f is Function of A,C
proofend;
compatibility
 for b1 being Function of A,C holds
( b1 = pr2 f iff for x being Element of A holds b1 . x = (f . x) `2 )
proofend;
end;

:: deftheorem Def5 defines pr1 FUNCT_2:def_5_:_
 for A, B, C being non empty set
for f being Function of A,[:B,C:]
for b5 being Function of A,B holds
( b5 = pr1 f iff for x being Element of A holds b5 . x = (f . x) `1 );

:: deftheorem Def6 defines pr2 FUNCT_2:def_6_:_
 for A, B, C being non empty set
for f being Function of A,[:B,C:]
for b5 being Function of A,C holds
( b5 = pr2 f iff for x being Element of A holds b5 . x = (f . x) `2 );

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 predf1 = f2 means :: FUNCT_2:def 7
( A1 = A2 &amp; ( for a being Element of A1 holds f1 . a = f2 . a ) );
compatibility
 ( f1 = f2 iff ( A1 = A2 &amp; ( for a being Element of A1 holds f1 . a = f2 . a ) ) )
proofend;
end;

:: deftheorem  defines = FUNCT_2:def_7_:_
 for A1 being set
for B1 being non empty set
for A2 being set
for B2 being non empty set
for f1 being Function of A1,B1
for f2 being Function of A2,B2 holds
( f1 = f2 iff ( A1 = A2 &amp; ( for a being Element of A1 holds f1 . a = f2 . a ) ) );

definition
let A, B be set ;
let f1, f2 be Function of A,B;
:: original:=
redefine predf1 = f2 means :: FUNCT_2:def 8
 for a being Element of A holds f1 . a = f2 . a;
compatibility
 ( f1 = f2 iff for a being Element of A holds f1 . a = f2 . a ) by Th63;
end;

:: deftheorem  defines = FUNCT_2:def_8_:_
 for A, B being set
for f1, f2 being Function of A,B holds
( f1 = f2 iff for a being Element of A holds f1 . a = f2 . a );

:: missing, 2006.11.05, A.T.
theorem :: FUNCT_2:93
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
proofend;

:: Moved from BORSUK_1 by AK on 27.12.2006
theorem Th94: :: FUNCT_2:94
for X being set
for A being Subset of X holds (id X) " A = A
proofend;

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

theorem :: FUNCT_2:96
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
proofend;

theorem :: FUNCT_2:97
for f being Function
for A0, C being set st C c= A0 holds
f .: C = (f | A0) .: C
proofend;

theorem :: FUNCT_2:98
for f being Function
for A0, D being set st f " D c= A0 holds
f " D = (f | A0) " D
proofend;

scheme :: FUNCT_2:sch 10
MChoice{ F1() ->  non empty set , F2() ->  non empty set , F3( set ) ->  set } :
 ex t being Function of F1(),F2() st
for a being Element of F1() holds t . a in F3(a)
provided
A1: for a being Element of F1() holds F2() meets F3(a)
proofend;

:: Moved from FINSEQ_4 by AK on 2007.10.09
theorem Th99: :: FUNCT_2:99
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
proofend;

registration
let X, D be non empty set ;
let p be Function of X,D;
let i be Element of X;
identifyp /. i with p . i;
correctness
compatibility
p /. i = p . i;
by Th99;
end;

:: from JCT_MISC, 2008.06.01, A.T.
theorem :: FUNCT_2:100
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 `)
proofend;

:: from CAT_1, 2008.07.01, A.T.
theorem :: FUNCT_2:101
for X, Y, Z being set
for D being non empty set
for f being Function of X,D st Y c= X &amp; f .: Y c= Z holds
f | Y is Function of Y,Z
proofend;

:: from WEIERSTR, 2008.07.07, A.T.
definition
let T, S be non empty set ;
let f be Function of T,S;
let G be Subset-Family of S;
funcf " G ->  Subset-Family of T means :Def9: :: FUNCT_2:def 9
 for A being Subset of T holds
( A in it iff ex B being Subset of S st
( B in G &amp; A = f " B ) );
existence
 ex b1 being Subset-Family of T st
for A being Subset of T holds
( A in b1 iff ex B being Subset of S st
( B in G &amp; A = f " B ) )
proofend;
uniqueness
 for b1, b2 being Subset-Family of T st ( for A being Subset of T holds
( A in b1 iff ex B being Subset of S st
( B in G &amp; A = f " B ) ) ) &amp; ( for A being Subset of T holds
( A in b2 iff ex B being Subset of S st
( B in G &amp; A = f " B ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def9 defines " FUNCT_2:def_9_:_
 for T, S being non empty set
for f being Function of T,S
for G being Subset-Family of S
for b5 being Subset-Family of T holds
( b5 = f " G iff for A being Subset of T holds
( A in b5 iff ex B being Subset of S st
( B in G &amp; A = f " B ) ) );

theorem :: FUNCT_2:102
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
proofend;

definition
let T, S be non empty set ;
let f be Function of T,S;
let G be Subset-Family of T;
funcf .: G ->  Subset-Family of S means :Def10: :: FUNCT_2:def 10
 for A being Subset of S holds
( A in it iff ex B being Subset of T st
( B in G &amp; A = f .: B ) );
existence
 ex b1 being Subset-Family of S st
for A being Subset of S holds
( A in b1 iff ex B being Subset of T st
( B in G &amp; A = f .: B ) )
proofend;
uniqueness
 for b1, b2 being Subset-Family of S st ( for A being Subset of S holds
( A in b1 iff ex B being Subset of T st
( B in G &amp; A = f .: B ) ) ) &amp; ( for A being Subset of S holds
( A in b2 iff ex B being Subset of T st
( B in G &amp; A = f .: B ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def10 defines .: FUNCT_2:def_10_:_
 for T, S being non empty set
for f being Function of T,S
for G being Subset-Family of T
for b5 being Subset-Family of S holds
( b5 = f .: G iff for A being Subset of S holds
( A in b5 iff ex B being Subset of T st
( B in G &amp; A = f .: B ) ) );

theorem :: FUNCT_2:103
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
proofend;

theorem :: FUNCT_2:104
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
proofend;

theorem :: FUNCT_2:105
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
proofend;

theorem :: FUNCT_2:106
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
proofend;

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

:: Generalized RFUNCT_2:def 1,CFCONT_1:def 1,NFCONT_1:def 7,def 8
:: NCFCONT1:def 9,def 10,def 11,def 12,def 13,def 14
:: 2008.08.15, A.T.
definition
let X, Z be set ;
let Y be non empty set ;
let f be Function of X,Y;
let p be Z -valued Function;
assume A1: rng f c= dom p ;
funcp /* f ->  Function of X,Z equals :Def11: :: FUNCT_2:def 11
p * f;
coherence
 p * f is Function of X,Z
proofend;
end;

:: deftheorem Def11 defines /* FUNCT_2:def_11_:_
 for X, Z being set
for Y being non empty set
for f being Function of X,Y
for p being b2 -valued Function st rng f c= dom p holds
p /* f = p * f;

theorem Th108: :: FUNCT_2:108
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 <> {} &amp; rng f c= dom p holds
(p /* f) . x = p . (f . x)
proofend;

theorem Th109: :: FUNCT_2:109
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 <> {} &amp; rng f c= dom p holds
(p /* f) . x = p /. (f . x)
proofend;

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

:: from RAMSEY_1, 2008.09.12,A.T.
theorem :: FUNCT_2:111
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} )
proofend;

:: from ISOCAT_2, 2008.09.14, A.T.
theorem :: FUNCT_2:112
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
proofend;

:: missing, 2008.09.14, A.T.
theorem Th113: :: FUNCT_2:113
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
proofend;

:: from RFUNCT_2, 2008.09.14, A.T.
theorem :: FUNCT_2:114
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
proofend;

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

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

theorem Th117: :: FUNCT_2:117
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
proofend;

theorem :: FUNCT_2:118
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) &amp; S c= T holds
(g | S) /* f = (g | T) /* f
proofend;

:: missing, 2009.01.09, A.T.
theorem :: FUNCT_2:119
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)]
proofend;

:: from YELLOW20, 2009.01.21, A.T.
theorem :: FUNCT_2:120
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)
proofend;

:: from FRAENKEL, 2009.05.06, A.K.
registration
let A, B be set ;
cluster Funcs (A,B) ->  functional ;
coherence
 Funcs (A,B) is functional
proofend;
end;

definition
let A, B be set ;
mode FUNCTION_DOMAIN of A,B ->  non empty set  means :Def12: :: FUNCT_2:def 12
 for x being Element of it holds x is Function of A,B;
existence
 ex b1 being non empty set st
for x being Element of b1 holds x is Function of A,B
proofend;
end;

:: deftheorem Def12 defines FUNCTION_DOMAIN FUNCT_2:def_12_:_
 for A, B being set
for b3 being non empty set holds
( b3 is FUNCTION_DOMAIN of A,B iff for x being Element of b3 holds x is Function of A,B );

registration
let A, B be set ;
cluster  ->  functional for FUNCTION_DOMAIN of A,B;
coherence
 for b1 being FUNCTION_DOMAIN of A,B holds b1 is functional
proofend;
end;

theorem :: FUNCT_2:121
for P, Q being set
for f being Function of P,Q holds {f} is FUNCTION_DOMAIN of P,Q
proofend;

theorem Th122: :: FUNCT_2:122
for P being set
for B being non empty set holds Funcs (P,B) is FUNCTION_DOMAIN of P,B
proofend;

definition
let A be set ;
let B be non empty set ;
:: original:Funcs
redefine func Funcs (A,B) ->  FUNCTION_DOMAIN of A,B;
coherence
 Funcs (A,B) is FUNCTION_DOMAIN of A,B by Th122;
let F be FUNCTION_DOMAIN of A,B;
:: original:Element
redefine mode Element of F ->  Function of A,B;
coherence
 for b1 being Element of F holds b1 is Function of A,B by Def12;
end;

registration
let I be set ;
cluster id I -> I -defined total for I -defined Function;
coherence
 for b1 being I -defined Function st b1 = id I holds
b1 is total ;
end;

:: from CAT_3, 2009.09.14
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 funcF /. x ->  Element of A equals :: FUNCT_2:def 13
F . x;
compatibility
 for b1 being Element of A holds
( b1 = F /. x iff b1 = F . x )
proofend;
end;

:: deftheorem  defines /. FUNCT_2:def_13_:_
 for X, A being non empty set
for F being Function of X,A
for x being set st x in X holds
F /. x = F . x;

theorem :: FUNCT_2:123
for X being non empty set
for f being Function of X,X
for g being b1 -valued Function holds dom (f * g) = dom g
proofend;

theorem :: FUNCT_2:124
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
proofend;

:: Moved from GROUP_9, AK
definition
let O, E be set ;
mode Action of O,E is Function of O,(Funcs (E,E));
end;

theorem :: FUNCT_2:125
for x, A being set
for f, g being Function of {x},A st f . x = g . x holds
f = g
proofend;