:: Functions from a Set to a Set
:: by Czes{\l}aw Byli\'nski
::
:: Copyright (c) 1990-2021 Association of Mizar Users

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 ;
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
by Def1;
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;

registration
let X be set ;
cluster quasi_total -> total for Element of bool [:[:X,X:],X:];
coherence
for b1 being Relation of [:X,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 object 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 being set
for x being object
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 being set
for x being object
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[ object , object ] } :
ex f being Function of F1(),F2() st
for x being object st x in F1() holds
P1[x,f . x]
provided
A1: for x being object st x in F1() holds
ex y being object st
( y in F2() & P1[x,y] )
proof end;

scheme :: FUNCT_2:sch 2
Lambda1{ F1() -> set , F2() -> set , F3( object ) -> object } :
ex f being Function of F1(),F2() st
for x being object st x in F1() holds
f . x = F3(x)
provided
A1: for x being object 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 object 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 object 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 object holds
( x in b1 iff ex f being Function st
( x = f & dom f = X & rng f c= Y ) ) ) & ( for x being object 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 object 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 object st y in Y holds
ex x being object st
( x in X & y = f . x ) ) holds
rng f = Y
proof end;

theorem Th11: :: FUNCT_2:11
for X, Y being set
for y being object
for f being Function of X,Y st y in rng f holds
ex x being object 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 object 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 being set
for x being object
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 object 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 being set
for x being object
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 object 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, Z being set
for x being object
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 P, X, Y being set
for f being Function of X,Y st Y <> {} holds
for y being object st ex x being object st
( x in X & x in P & y = f . x ) holds
y in f .: P
proof end;

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

theorem :: FUNCT_2:37
canceled;

::\$CT
theorem :: FUNCT_2:38
for Q, X, Y being set
for f being Function of X,Y st Y <> {} holds
for x being object holds
( x in f " Q iff ( x in X & f . x in Q ) )
proof end;

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

theorem Th39: :: 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 object st y in Y holds
f " {y} <> {} ) iff rng f = Y ) by ;

theorem Th41: :: FUNCT_2:42
for P, X, Y 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 Q, X, Y, Z 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 P, Y being set
for f being Function of {},Y holds f .: P = {} ;

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

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

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

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

theorem Th49: :: FUNCT_2:50
for X being set
for x, y being object
for f being Function of X,{y} st x in X holds
f . x = y
proof end;

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

theorem Th51: :: 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 Th52: :: 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 Th55: :: 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 object 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 :: FUNCT_2:def 4
( f is one-to-one & f is onto );
end;

:: deftheorem 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 ;
coherence
for b1 being PartFunc of X,Y st b1 is bijective holds
( b1 is one-to-one & b1 is onto )
;
coherence
for b1 being PartFunc of X,Y st b1 is one-to-one & b1 is onto holds
b1 is bijective
;
end;

registration
let X be set ;
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 Th56: :: 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 object st x1 in X & x2 in X & f . x1 = f . x2 holds
x1 = x2 by Th55;

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 ;
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 Th61: :: FUNCT_2:62
for P, X 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[ object , object ] } :
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 Th62: :: 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 Th63: :: FUNCT_2:64
for X, Y, P being set
for f being Function of X,Y
for y being object st y in f .: P holds
ex x being object st
( x in X & x in P & y = f . x )
proof end;

theorem :: FUNCT_2:65
for P, X, Y being set
for f being Function of X,Y
for y being object st y in f .: P holds
ex c being Element of X st
( c in P & y = f . c )
proof end;

theorem Th65: :: 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[ object ], F3( object ) -> object , F4( object ) -> object } :
ex f being Function of F1(),F2() st
for x being object st x in F1() holds
( ( P1[x] implies f . x = F3(x) ) & ( P1[x] implies f . x = F4(x) ) )
provided
A1: for x being object 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 Th70: :: 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 object 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 Th74: :: 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 object 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 object st x in dom f holds
f . x = g . x )
proof end;

theorem Th76: :: 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 Th81: :: 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 being set
for y being object
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 Th88: :: 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 Th89: :: 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 object 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 object holds Y <> {y} ) & TotFuncs f = TotFuncs g holds
f = g by Th89;

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

:: 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( object ) -> 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( object ) -> 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( object ) -> object } :
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( object ) -> object } :
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 Th62;
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 Th93: :: 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( object ) -> 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 Th98: :: 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 Th98;
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 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 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 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 Th107: :: FUNCT_2:108
for X, Z 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 Th108: :: FUNCT_2:109
for X, Z 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 X, Z 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 Th112: :: FUNCT_2:113
for y being object
for 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 X, Y 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 X, Y 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 Th116: :: 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
by Def12;
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 Th121: :: 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 Th121;
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 ;
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 set
for Y being non empty set
for f being Function of X,Y
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 ;

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

theorem Th125: :: FUNCT_2:126
for A being set holds id A in Funcs (A,A)
proof end;

theorem :: FUNCT_2:127
Funcs ({},{}) = {()}
proof end;

theorem Th127: :: FUNCT_2:128
for A, B, C being set
for f, g being Function st f in Funcs (A,B) & g in Funcs (B,C) holds
g * f in Funcs (A,C)
proof end;

theorem :: FUNCT_2:129
for A, B, C being set st Funcs (A,B) <> {} & Funcs (B,C) <> {} holds
Funcs (A,C) <> {}
proof end;

theorem :: FUNCT_2:130
for A being set holds {} is Function of A,{} by ;

scheme :: FUNCT_2:sch 11
Lambda1{ F1() -> set , F2() -> set , F3( object ) -> object } :
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;