:: 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;
attr R 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 ) ) & ( 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
proof end;
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
proof end;
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
proof end;
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
proof end;
end;

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

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
proof end;

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

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

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

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

theorem :: FUNCT_2:7
for X, Y, Z being set
for f being Function of X,Y st ( Y = {} implies X = {} ) & Y c= Z holds
f is Function of X,Z 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() & P1[x,y] )
proof end;

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()
proof end;

definition
let X, Y be set ;
func Funcs (X,Y) -> set means :Def2: :: FUNCT_2:def 2
 for x being set holds
( x in it iff ex f being Function st
( x = f & dom f = X & rng f c= Y ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ex f being Function st
( x = f & dom f = X & rng f c= Y ) )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ex f being Function st
( x = f & dom f = X & rng f c= Y ) ) ) & ( for x being set holds
( x in b2 iff ex f being Function st
( x = f & dom f = X & rng f c= Y ) ) ) holds
b1 = b2
proof end;
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 & dom f = X & 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)
proof end;

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
proof end;
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 & y = f . x ) ) holds
rng f = Y
proof end;

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 & f . x = y )
proof end;

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
proof end;

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
proof end;

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

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

theorem :: FUNCT_2: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 )
proof end;

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

theorem :: FUNCT_2: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
proof end;

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 & x2 in X & f . x1 = f . x2 holds
x1 = x2 )
proof end;

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

theorem :: FUNCT_2:21
for X, Y being set
for f being Function of X,Y st X <> {} & Y <> {} holds
( f is one-to-one iff for Z being set
for g, h being Function of Z,X st f * g = f * h holds
g = h )
proof end;

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

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

:: deftheorem Def3 defines onto FUNCT_2:def 3 :
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 & g is onto )
proof end;

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 = {} ) & g * f is one-to-one & rng f = Y holds
( f is one-to-one & g is one-to-one )
proof end;

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

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

theorem :: 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 & g is onto holds
g * f is onto
proof end;

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 <> {} & Y <> {} & rng f = Y & f is one-to-one & ( for y, x being set holds
( y in Y & g . y = x iff ( x in X & f . x = y ) ) ) holds
g = f "
proof end;

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

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

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

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

theorem :: FUNCT_2: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 <> {} & x in X & f . x in Z holds
(Z |` f) . x = f . x
proof end;

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 & x in P & y = f . x ) holds
y in f .: P
proof end;

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 & f . x in Q ) )
proof end;

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
proof end;

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 )
proof end;

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

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

theorem :: FUNCT_2: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)
proof end;

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
proof end;

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

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)}
proof end;

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
proof end;

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

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

registration
let X, Y be set ;
let f be quasi_total PartFunc of X,Y;
let g be quasi_total PartFunc of X,X;
cluster g * f -> quasi_total for PartFunc of X,Y;
coherence
for b1 being PartFunc of X,Y st b1 = f * g holds
b1 is quasi_total
proof end;
end;

registration
let X, Y be set ;
let f be quasi_total PartFunc of Y,Y;
let g be quasi_total PartFunc of X,Y;
cluster g * f -> quasi_total for PartFunc of X,Y;
coherence
for b1 being PartFunc of X,Y st b1 = f * g holds
b1 is quasi_total
proof end;
end;

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

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

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

theorem 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 & x2 in X & f . x1 = f . x2 holds
x1 = x2 )
proof end;

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

:: deftheorem Def4 defines bijective FUNCT_2:def 4 :
for X, Y being set
for f being b1 -defined b2 -valued Function holds
( f is bijective iff ( f is one-to-one & 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 & 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 & 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
proof end;
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 & rng f = X holds
f is Permutation of X
proof end;

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

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

registration
let X be set ;
let f, g be bijective Function of X,X;
cluster f * 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 & b1 is total holds
b1 is bijective
proof end;
end;

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

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

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

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

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 & f " (f .: P) = P )
proof end;

registration
let X be set ;
let D be non empty set ;
let Z be set ;
let f be Function of X,D;
let g be Function of D,Z;
cluster f * g -> quasi_total 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 func f . c -> Element of D;
coherence
f . c is Element of D
proof end;
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]
proof end;

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)
proof end;

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
proof end;

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 & x in P & y = f . x )
proof end;

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 & y = f . c )
proof end;

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
proof end;

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) ) & ( 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() ) & ( P1[x] implies F4(x) in F2() ) )
proof end;

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
proof end;

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 = {} ) & 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
proof end;

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

theorem :: FUNCT_2:73
for X, Y being set
for f, g being Function of X,Y st ( Y = {} implies X = {} ) & f tolerates g holds
f = g by PARTFUN1: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 )
proof end;

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 )
proof end;

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
proof end;

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 & 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 = {} ) & f tolerates g holds
ex h being Function of X,Y st
( f tolerates h & g tolerates h )
proof end;

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 = {} ) & 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
proof end;

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

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

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}
proof end;

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
proof end;

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

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

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

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

:: from RLVECT_2
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() & ( for x being Element of F1() st x <> F3() holds
f . x = F5(x) ) )
proof end;

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() & f . F4() = F6() & ( for x being Element of F1() st x <> F3() & x <> F4() holds
f . x = F7(x) ) )
provided
A1: F3() <> F4()
proof end;

:: 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 & rng f c= B )
proof end;

:: from SUPINF_2
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()
proof end;

:: from YELLOW_2
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()
proof end;

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

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

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 )
proof end;

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
proof end;

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

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

scheme :: FUNCT_2:sch 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)
proof end;

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

registration
let X, D be non empty set ;
let p be Function of X,D;
let i be Element of X;
identify p /. i with p . i;
correctness
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 `)
proof end;

:: 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 & f .: Y c= Z holds
f | Y is Function of Y,Z
proof end;

:: 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;
func f " 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 & 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 & A = f " B ) )
proof end;
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 & A = f " B ) ) ) & ( for A being Subset of T holds
( A in b2 iff ex B being Subset of S st
( B in G & A = f " B ) ) ) holds
b1 = b2
proof end;
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 & 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
proof end;

definition
let T, S be non empty set ;
let f be Function of T,S;
let G be Subset-Family of T;
func f .: G -> Subset-Family of S means :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 & 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 & A = f .: B ) )
proof end;
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 & A = f .: B ) ) ) & ( for A being Subset of S holds
( A in b2 iff ex B being Subset of T st
( B in G & A = f .: B ) ) ) holds
b1 = b2
proof end;
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 & 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
proof end;

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
proof end;

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
proof end;

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
proof end;

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))
proof end;

:: 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 ;
func p /* f -> Function of X,Z equals :Def11: :: FUNCT_2:def 11
p * f;
coherence
p * f is Function of X,Z
proof end;
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 <> {} & rng f c= dom p holds
(p /* f) . x = p . (f . x)
proof end;

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 <> {} & rng f c= dom p holds
(p /* f) . x = p /. (f . x)
proof end;

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)
proof end;

:: 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} )
proof end;

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

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

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

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)
proof end;

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)
proof end;

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
proof end;

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) & S c= T holds
(g | S) /* f = (g | T) /* f
proof end;

:: 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)]
proof end;

:: 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)
proof end;

:: from FRAENKEL, 2009.05.06, A.K.
registration
let A, B be set ;
cluster Funcs (A,B) -> functional ;
coherence
Funcs (A,B) is functional
proof end;
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
proof end;
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
proof end;
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
proof end;

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
proof end;

definition
let A be set ;
let B be non empty set ;
:: original: Funcs
redefine func Funcs (A,B) -> FUNCTION_DOMAIN of A,B;
coherence
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 func F /. 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 )
proof end;
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
proof end;

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
proof end;

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