:: Functions from a Set to a Set
:: by Czes{\l}aw Byli\'nski
::
:: Received April 6, 1989
:: 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 ;

cluster Relation-like X -defined Y -valued Function-like quasi_total for Element of bool [:X,Y:];

existence
ex b₁ being PartFunc of X,Y st b₁ is quasi_total

proof end;

end;

registration

let X, Y be set ;

cluster total -> quasi_total for Element of bool [:X,Y:];

coherence
for b₁ being Relation of X,Y st b₁ is total holds
b₁ 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 b₁ being Relation of X,Y st b₁ is quasi_total holds
b₁ 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 b₁ being Relation of X,Y st b₁ is quasi_total holds
b₁ is total by Def1;

end;

registration

let X be set ;

cluster quasi_total -> total for Element of bool [:X,X:];

coherence
for b₁ being Relation of X,X st b₁ is quasi_total holds
b₁ is total

proof end;

end;

registration

let X be set ;

cluster quasi_total -> total for Element of bool [:[:X,X:],X:];

coherence
for b₁ being Relation of [:X,X:],X st b₁ is quasi_total holds
b₁ 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{ F₁() -> set , F₂() -> set , P₁[ object , object ] } :

ex f being Function of F₁(),F₂() st
for x being object st x in F₁() holds
P₁[x,f . x]

provided

A1: for x being object st x in F₁() holds
ex y being object st
( y in F₂() & P₁[x,y] )

proof end;

scheme :: FUNCT_2:sch 2
Lambda1{ F₁() -> set , F₂() -> set , F₃( object ) -> object } :

ex f being Function of F₁(),F₂() st
for x being object st x in F₁() holds
f . x = F₃(x)

provided

A1: for x being object st x in F₁() holds
F₃(x) in F₂()

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 b₁ being set st
for x being object holds
( x in b₁ iff ex f being Function st
( x = f & dom f = X & rng f c= Y ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being object holds
( x in b₁ iff ex f being Function st
( x = f & dom f = X & rng f c= Y ) ) ) & ( for x being object holds
( x in b₂ iff ex f being Function st
( x = f & dom f = X & rng f c= Y ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines Funcs FUNCT_2:def 2 :
for X, Y, b₃ being set holds
( b₃ = Funcs (X,Y) iff for x being object holds
( x in b₃ 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 b₁ -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 FUNCT_1:73, FUNCT_1:72;

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 b₁ being PartFunc of X,Y st b₁ = f * g holds
b₁ 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 b₁ being PartFunc of X,Y st b₁ = f * g holds
b₁ 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 b₁ -defined b₂ -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 b₁ being PartFunc of X,Y st b₁ is bijective holds
( b₁ is one-to-one & b₁ is onto ) ;

cluster Function-like one-to-one onto -> bijective for Element of bool [:X,Y:];

coherence
for b₁ being PartFunc of X,Y st b₁ is one-to-one & b₁ is onto holds
b₁ is bijective ;

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 b₁ being Function of X,X st b₁ 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 b₁ being PartFunc of X,X st b₁ = f * g holds
b₁ 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 b₁ being Function of X,X st b₁ = g * f holds
b₁ is bijective ;

end;

registration

let X be set ;

cluster reflexive Function-like total quasi_total -> bijective for Element of bool [:X,X:];

coherence
for b₁ being Function of X,X st b₁ is reflexive & b₁ is total holds
b₁ 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 b₁ being PartFunc of X,Z st b₁ = g * f holds
b₁ 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{ F₁() -> non empty set , F₂() -> non empty set , P₁[ object , object ] } :

ex f being Function of F₁(),F₂() st
for x being Element of F₁() holds P₁[x,f . x]

provided

A1: for x being Element of F₁() ex y being Element of F₂() st P₁[x,y]

proof end;

scheme :: FUNCT_2:sch 4
LambdaD{ F₁() -> non empty set , F₂() -> non empty set , F₃( Element of F₁()) -> Element of F₂() } :

ex f being Function of F₁(),F₂() st
for x being Element of F₁() holds f . x = F₃(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{ F₁() -> set , F₂() -> set , P₁[ object ], F₃( object ) -> object , F₄( object ) -> object } :

ex f being Function of F₁(),F₂() st
for x being object st x in F₁() holds
( ( P₁[x] implies f . x = F₃(x) ) & ( P₁[x] implies f . x = F₄(x) ) )

provided

A1: for x being object st x in F₁() holds
( ( P₁[x] implies F₃(x) in F₂() ) & ( P₁[x] implies F₄(x) in F₂() ) )

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 b₁ being Function of A,B holds not b₁ is empty by Def1, RELAT_1:38;

end;

:: from RLVECT_2

scheme :: FUNCT_2:sch 6
LambdaSep1{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> Element of F₁(), F₄() -> Element of F₂(), F₅( object ) -> Element of F₂() } :

ex f being Function of F₁(),F₂() st
( f . F₃() = F₄() & ( for x being Element of F₁() st x <> F₃() holds
f . x = F₅(x) ) )

proof end;

scheme :: FUNCT_2:sch 7
LambdaSep2{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> Element of F₁(), F₄() -> Element of F₁(), F₅() -> Element of F₂(), F₆() -> Element of F₂(), F₇( object ) -> Element of F₂() } :

ex f being Function of F₁(),F₂() st
( f . F₃() = F₅() & f . F₄() = F₆() & ( for x being Element of F₁() st x <> F₃() & x <> F₄() holds
f . x = F₇(x) ) )

provided

A1: F₃() <> F₄()

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{ F₁() -> non empty set , F₂() -> set , F₃( object ) -> object } :

ex f being Function of F₁(),F₂() st
for x being Element of F₁() holds f . x = F₃(x)

provided

A1: for x being Element of F₁() holds F₃(x) in F₂()

proof end;

:: from YELLOW_2

scheme :: FUNCT_2:sch 9
KappaMD{ F₁() -> non empty set , F₂() -> non empty set , F₃( object ) -> object } :

ex f being Function of F₁(),F₂() st
for x being Element of F₁() holds f . x = F₃(x)

provided

A1: for x being Element of F₁() holds F₃(x) is Element of F₂()

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 b₁ being Function of A,B holds
( b₁ = pr1 f iff for x being Element of A holds b₁ . 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 b₁ being Function of A,C holds
( b₁ = pr2 f iff for x being Element of A holds b₁ . 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 b₅ being Function of A,B holds
( b₅ = pr1 f iff for x being Element of A holds b₅ . 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 b₅ being Function of A,C holds
( b₅ = pr2 f iff for x being Element of A holds b₅ . 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{ F₁() -> non empty set , F₂() -> non empty set , F₃( object ) -> set } :

ex t being Function of F₁(),F₂() st
for a being Element of F₁() holds t . a in F₃(a)

provided

A1: for a being Element of F₁() holds F₂() meets F₃(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 b₁ being Subset-Family of T st
for A being Subset of T holds
( A in b₁ iff ex B being Subset of S st
( B in G & A = f " B ) )

proof end;

uniqueness
for b₁, b₂ being Subset-Family of T st ( for A being Subset of T holds
( A in b₁ iff ex B being Subset of S st
( B in G & A = f " B ) ) ) & ( for A being Subset of T holds
( A in b₂ iff ex B being Subset of S st
( B in G & A = f " B ) ) ) holds
b₁ = b₂

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 b₅ being Subset-Family of T holds
( b₅ = f " G iff for A being Subset of T holds
( A in b₅ 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 b₁ being Subset-Family of S st
for A being Subset of S holds
( A in b₁ iff ex B being Subset of T st
( B in G & A = f .: B ) )

proof end;

uniqueness
for b₁, b₂ being Subset-Family of S st ( for A being Subset of S holds
( A in b₁ iff ex B being Subset of T st
( B in G & A = f .: B ) ) ) & ( for A being Subset of S holds
( A in b₂ iff ex B being Subset of T st
( B in G & A = f .: B ) ) ) holds
b₁ = b₂

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 b₅ being Subset-Family of S holds
( b₅ = f .: G iff for A being Subset of S holds
( A in b₅ 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 b₂ -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 b₁ being non empty set st
for x being Element of b₁ 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 b₃ being non empty set holds
( b₃ is FUNCTION_DOMAIN of A,B iff for x being Element of b₃ holds x is Function of A,B );

registration

let A, B be set ;

cluster -> functional for FUNCTION_DOMAIN of A,B;

coherence
for b₁ being FUNCTION_DOMAIN of A,B holds b₁ 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 b₁ being Element of F holds b₁ 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 b₁ being I -defined Function st b₁ = id I holds
b₁ 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 b₁ being Element of A holds
( b₁ = F /. x iff b₁ = 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 b₁ -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 ({},{}) = {(id {})}

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 Def1, RELSET_1:12;

scheme :: FUNCT_2:sch 11
Lambda1{ F₁() -> set , F₂() -> set , F₃( object ) -> object } :

ex f being Function of F₁(),F₂() st
for x being set st x in F₁() holds
f . x = F₃(x)

provided

A1: for x being set st x in F₁() holds
F₃(x) in F₂()

proof end;