:: Functions from a Set to a Set
:: by Czes{\l}aw Byli\'nski
::
:: Received April 6, 1989
:: Copyright (c) 1990-2011 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 = {} implies X = {} )
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 X = {} ) implies ( R is quasi_total iff X = dom R ) ) & ( Y = {} implies X = {} ( R is quasi_total iff R = {} ) ) );

registration
let X, Y be set ;
cluster Relation-like X -defined Y -valued Function-like quasi_total 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 Function-like total -> quasi_total Element of bool [:X,Y:];
coherence
for b1 being PartFunc 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;

theorem :: FUNCT_2:1
canceled;

theorem :: FUNCT_2:2
canceled;

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

theorem Th4: :: FUNCT_2:4
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:5
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 Th6: :: FUNCT_2:6
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 Th7: :: FUNCT_2:7
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:8
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:9
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
proof end;

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 :: FUNCT_2:10
canceled;

theorem Th11: :: FUNCT_2:11
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:12
for X being set
for f being Function of X,X holds f in Funcs (X,X) by Th11;

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

registration
let X be set ;
cluster Funcs (X,X) -> non empty ;
coherence
not Funcs (X,X) is empty by Th11;
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:13
canceled;

theorem :: FUNCT_2:14
canceled;

theorem :: FUNCT_2:15
canceled;

theorem :: FUNCT_2:16
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 Th17: :: FUNCT_2:17
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 Th18: :: FUNCT_2:18
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 Th19: :: FUNCT_2:19
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:20
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 Th21: :: FUNCT_2:21
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:22
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:23
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:24
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:25
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:26
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:27
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:28
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:29
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:30
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 Th31: :: FUNCT_2:31
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:32
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:33
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:34
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:35
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:36
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:37
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 Th38: :: FUNCT_2:38
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:39
canceled;

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

theorem :: FUNCT_2:41
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:42
canceled;

theorem :: FUNCT_2:43
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:44
for X, Y, P being set
for f being Function of X,Y holds f .: P c= Y ;

theorem :: FUNCT_2:45
for X, Y being set
for f being Function of X,Y st ( Y = {} implies X = {} ) holds
f .: X = rng f by RELSET_1:38;

theorem :: FUNCT_2:46
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:47
for X, Y, Q being set
for f being PartFunc of X,Y holds f " Q c= X ;

theorem Th48: :: FUNCT_2:48
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:49
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 Th50: :: FUNCT_2:50
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:51
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:52
canceled;

theorem :: FUNCT_2:53
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:54
canceled;

theorem :: FUNCT_2:55
canceled;

theorem :: FUNCT_2:56
canceled;

theorem :: FUNCT_2:57
canceled;

theorem :: FUNCT_2:58
canceled;

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

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

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

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

theorem :: FUNCT_2:63
canceled;

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

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

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

theorem Th67: :: FUNCT_2:67
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 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 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 :: FUNCT_2:68
canceled;

theorem :: FUNCT_2:69
canceled;

theorem :: FUNCT_2:70
canceled;

theorem :: FUNCT_2:71
canceled;

theorem :: FUNCT_2:72
canceled;

theorem Th73: :: FUNCT_2:73
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:74
canceled;

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

theorem :: FUNCT_2:78
canceled;

theorem :: FUNCT_2:79
canceled;

theorem :: FUNCT_2:80
canceled;

theorem :: FUNCT_2:81
canceled;

theorem :: FUNCT_2:82
canceled;

definition
let X, Y be set ;
let f be PartFunc of X,Y;
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 PartFunc of X,Y 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 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 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 quasi_total bijective 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 Th83: :: FUNCT_2:83
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:84
canceled;

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

registration
let X be set ;
let f, g be onto PartFunc of X,X;
cluster g * f -> onto 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 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 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:86
for X being set
for f, g being Permutation of X st g * f = g holds
f = id X
proof end;

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

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

theorem :: FUNCT_2:89
canceled;

theorem :: FUNCT_2:90
canceled;

theorem :: FUNCT_2:91
canceled;

theorem Th92: :: FUNCT_2:92
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 ;
cluster Function-like quasi_total -> total Element of bool [:X,D:];
coherence
for b1 being PartFunc of X,D st b1 is quasi_total holds
b1 is total
proof end;
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 PartFunc of X,Z;
coherence
for b1 being PartFunc of X,Z st b1 = g * f holds
b1 is quasi_total by Th19;
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 :: FUNCT_2:93
canceled;

theorem :: FUNCT_2:94
canceled;

theorem :: FUNCT_2:95
canceled;

theorem :: FUNCT_2:96
canceled;

theorem :: FUNCT_2:97
canceled;

theorem :: FUNCT_2:98
canceled;

theorem :: FUNCT_2:99
canceled;

theorem :: FUNCT_2:100
canceled;

theorem :: FUNCT_2:101
canceled;

theorem :: FUNCT_2:102
canceled;

theorem :: FUNCT_2:103
canceled;

theorem :: FUNCT_2:104
canceled;

theorem :: FUNCT_2:105
canceled;

theorem :: FUNCT_2:106
canceled;

theorem :: FUNCT_2:107
canceled;

theorem :: FUNCT_2:108
canceled;

theorem :: FUNCT_2:109
canceled;

theorem :: FUNCT_2:110
canceled;

theorem :: FUNCT_2:111
canceled;

theorem :: FUNCT_2:112
canceled;

theorem Th113: :: FUNCT_2:113
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 :: FUNCT_2:114
canceled;

theorem Th115: :: FUNCT_2:115
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:116
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;

theorem :: FUNCT_2:117
canceled;

theorem :: FUNCT_2:118
canceled;

theorem :: FUNCT_2:119
canceled;

theorem :: FUNCT_2:120
canceled;

begin

theorem Th121: :: FUNCT_2:121
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:122
canceled;

theorem :: FUNCT_2:123
canceled;

theorem :: FUNCT_2:124
canceled;

theorem :: FUNCT_2:125
canceled;

theorem :: FUNCT_2:126
canceled;

theorem :: FUNCT_2:127
canceled;

theorem :: FUNCT_2:128
canceled;

theorem :: FUNCT_2:129
canceled;

theorem :: FUNCT_2:130
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:131
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:132
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 Th133: :: FUNCT_2:133
for X, Y being set
for f being Function of X,Y st ( Y = {} implies X = {} ) holds
<:f,X,Y:> is total by PARTFUN1:87;

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

theorem :: FUNCT_2:134
canceled;

theorem :: FUNCT_2:135
canceled;

theorem Th136: :: FUNCT_2:136
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:137
canceled;

theorem :: FUNCT_2:138
canceled;

theorem :: FUNCT_2:139
canceled;

theorem :: FUNCT_2:140
canceled;

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

theorem Th142: :: FUNCT_2:142
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:148;

theorem :: FUNCT_2:143
for X being set
for f, g being Function of X,X st f tolerates g holds
f = g by Th142;

theorem :: FUNCT_2:144
canceled;

theorem Th145: :: FUNCT_2:145
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:146
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 :: FUNCT_2:147
canceled;

theorem Th148: :: FUNCT_2:148
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:149
canceled;

theorem :: FUNCT_2:150
canceled;

theorem :: FUNCT_2:151
canceled;

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

theorem :: FUNCT_2:153
canceled;

theorem :: FUNCT_2:154
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 Th155: :: FUNCT_2:155
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 7;

theorem :: FUNCT_2:156
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 Th155;

theorem :: FUNCT_2:157
canceled;

theorem Th158: :: FUNCT_2:158
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:159
for X, Y being set
for f being PartFunc of X,Y holds TotFuncs f c= Funcs (X,Y)
proof end;

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

theorem Th161: :: FUNCT_2:161
for X, Y being set
for f being Function of X,Y st ( Y = {} implies X = {} ) holds
TotFuncs <:f,X,Y:> = {f}
proof end;

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

theorem :: FUNCT_2:163
canceled;

theorem :: FUNCT_2:164
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:165
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 Th166: :: FUNCT_2:166
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 Th167: :: FUNCT_2:167
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:168
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;

registration
let A, B be non empty set ;
cluster Function-like quasi_total -> non empty Element of bool [:A,B:];
coherence
for b1 being Function of A,B holds not b1 is empty by Def1, RELAT_1:60;
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() & ( 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;

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

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;

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;

scheme :: FUNCT_2:sch 10
NonUniqExMD{ 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;

definition
let A, B, C be non empty set ;
canceled;
let f be Function of A,[:B,C:];
:: original: pr1
redefine func pr1 f -> Function of A,B means :Def6: :: FUNCT_2:def 6
 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 :Def7: :: FUNCT_2:def 7
 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 FUNCT_2:def 5 :
canceled;

:: deftheorem Def6 defines pr1 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,B holds
( b5 = pr1 f iff for x being Element of A holds b5 . x = (f . x) `1 );

:: deftheorem Def7 defines pr2 FUNCT_2:def 7 :
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 8
( 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 8 :
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 9
 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 Th113;
end;

:: deftheorem defines = FUNCT_2:def 9 :
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 );

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

theorem Th171: :: FUNCT_2:171
for X being set
for A being Subset of X holds (id X) " A = A
proof end;

theorem :: FUNCT_2:172
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:173
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:174
for f being Function
for A0, C being set st C c= A0 holds
f .: C = (f | A0) .: C
proof end;

theorem :: FUNCT_2:175
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 11
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;

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

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

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

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 :Def10: :: FUNCT_2:def 10
 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 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 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:179
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 :Def11: :: FUNCT_2:def 11
 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 Def11 defines .: FUNCT_2:def 11 :
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:180
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:181
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:182
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:183
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:184
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;

definition
let X, Y, Z be set ;
let f be Function of X,Y;
let p be PartFunc of Y,Z;
assume that
A1: Y <> {} and
A2: rng f c= dom p ;
func p /* f -> Function of X,Z equals :Def12: :: FUNCT_2:def 12
p * f;
coherence
p * f is Function of X,Z
proof end;
end;

:: deftheorem Def12 defines /* FUNCT_2:def 12 :
for X, Y, Z being set
for f being Function of X,Y
for p being PartFunc of Y,Z st Y <> {} & rng f c= dom p holds
p /* f = p * f;

theorem Th185: :: FUNCT_2:185
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 Th186: :: FUNCT_2:186
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:187
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;

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

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

theorem Th190: :: FUNCT_2:190
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;

theorem :: FUNCT_2:191
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:192
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:193
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 Th194: :: FUNCT_2:194
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:195
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;

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

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

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 :Def13: :: FUNCT_2:def 13
 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 Def13 defines FUNCTION_DOMAIN FUNCT_2:def 13 :
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 FUNCTION_DOMAIN of A,B;
coherence
for b1 being FUNCTION_DOMAIN of A,B holds b1 is functional
proof end;
end;

theorem :: FUNCT_2:198
for P, Q being set
for f being Function of P,Q holds {f} is FUNCTION_DOMAIN of P,Q
proof end;

theorem Th199: :: FUNCT_2:199
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 Th199;
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 Def13;
end;

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

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 14
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 14 :
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:200
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:201
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;

definition
let O, E be set ;
mode Action of O,E is Function of O,(Funcs (E,E));
end;