:: by Czes{\l}aw Byli\'nski

::

:: Received April 6, 1989

:: Copyright (c) 1990 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;
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 ;

:: 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 b_{1} being PartFunc of X,Y st b_{1} is quasi_total

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

existence

ex b

proof end;

registration

let X, Y be set ;

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

coherence

for b_{1} being PartFunc of X,Y st b_{1} is total holds

b_{1} is quasi_total

end;
cluster Function-like total -> quasi_total Element of bool [:X,Y:];

coherence

for b

b

proof end;

theorem :: FUNCT_2:1

canceled;

theorem :: FUNCT_2:2

canceled;

theorem :: FUNCT_2:3

proof end;

theorem Th4: :: FUNCT_2:4

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

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

proof end;

theorem Th7: :: FUNCT_2:7

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

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

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{ F_{1}() -> set , F_{2}() -> set , P_{1}[ set , set ] } :

provided

FuncEx1{ F

provided

proof end;

scheme :: FUNCT_2:sch 2

Lambda1{ F_{1}() -> set , F_{2}() -> set , F_{3}( set ) -> set } :

provided

Lambda1{ F

provided

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 b_{1} being set st

for x being set holds

( x in b_{1} iff ex f being Function st

( x = f & dom f = X & rng f c= Y ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ex f being Function st

( x = f & dom f = X & rng f c= Y ) ) ) & ( for x being set holds

( x in b_{2} iff ex f being Function st

( x = f & dom f = X & rng f c= Y ) ) ) holds

b_{1} = b_{2}

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

for x being set holds

( x in b

( x = f & dom f = X & rng f c= Y ) )

proof end;

uniqueness for b

( x in b

( x = f & dom f = X & rng f c= Y ) ) ) & ( for x being set holds

( x in b

( x = f & dom f = X & rng f c= Y ) ) ) holds

b

proof end;

:: deftheorem Def2 defines Funcs FUNCT_2:def 2 :

for X, Y, b

( b

( x in b

( x = f & dom f = X & rng f c= Y ) ) );

theorem :: FUNCT_2:10

canceled;

theorem Th11: :: FUNCT_2:11

proof end;

theorem :: FUNCT_2:12

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;
let Y be non empty set ;

cluster Funcs (X,Y) -> non empty ;

coherence

not Funcs (X,Y) is empty by Th11;

registration
end;

registration

let X be non empty set ;

let Y be empty set ;

cluster Funcs (X,Y) -> empty ;

coherence

Funcs (X,Y) is empty

end;
let Y be empty set ;

cluster Funcs (X,Y) -> empty ;

coherence

Funcs (X,Y) is empty

proof 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

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 )

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

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

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

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)

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 )

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

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

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 )

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

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 )

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

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

:: deftheorem Def3 defines onto FUNCT_2:def 3 :

for Y being set

for f being b

( 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 )

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 )

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

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

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

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 "

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 )

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 "

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

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

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

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

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

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

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;

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

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

theorem Th48: :: FUNCT_2:48

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 )

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)

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

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)

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

proof end;

theorem :: FUNCT_2:60

theorem :: FUNCT_2:61

proof end;

theorem Th62: :: FUNCT_2:62

proof end;

theorem :: FUNCT_2:63

canceled;

theorem :: FUNCT_2:64

proof end;

theorem Th65: :: FUNCT_2:65

proof end;

theorem Th66: :: FUNCT_2:66

proof end;

theorem Th67: :: FUNCT_2:67

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 b_{1} being PartFunc of X,Y st b_{1} = f * g holds

b_{1} is quasi_total

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

b

proof 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 b_{1} being PartFunc of X,Y st b_{1} = f * g holds

b_{1} is quasi_total

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

b

proof 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

proof end;

theorem :: FUNCT_2:74

canceled;

theorem :: FUNCT_2:75

proof end;

theorem :: FUNCT_2:76

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 )

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

:: 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 b_{1} being PartFunc of X,Y st b_{1} is bijective holds

( b_{1} is one-to-one & b_{1} is onto )
by Def4;

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

coherence

for b_{1} being PartFunc of X,Y st b_{1} is one-to-one & b_{1} is onto holds

b_{1} is bijective
by Def4;

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

coherence

for b

( b

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

coherence

for b

b

registration

let X be set ;

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

existence

ex b_{1} being Function of X,X st b_{1} is bijective

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

existence

ex b

proof 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

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;

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 b_{1} being PartFunc of X,X st b_{1} = f * g holds

b_{1} is onto

end;
let f, g be onto PartFunc of X,X;

cluster g * f -> onto PartFunc of X,X;

coherence

for b

b

proof 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 b_{1} being Function of X,X st b_{1} = g * f holds

b_{1} is bijective
;

end;
let f, g be bijective Function of X,X;

cluster f * g -> bijective Function of X,X;

coherence

for b

b

registration

let X be set ;

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

coherence

for b_{1} being Function of X,X st b_{1} is reflexive & b_{1} is total holds

b_{1} is bijective

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

coherence

for b

b

proof 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

end;
let f be Permutation of X;

:: original: "

redefine func f " -> Permutation of X;

coherence

f " is Permutation of X

proof end;

theorem :: FUNCT_2:86

proof end;

theorem :: FUNCT_2:87

proof end;

theorem :: FUNCT_2:88

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 )

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 b_{1} being PartFunc of X,D st b_{1} is quasi_total holds

b_{1} is total

end;
let D be non empty set ;

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

coherence

for b

b

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 PartFunc of X,Z;

coherence

for b_{1} being PartFunc of X,Z st b_{1} = g * f holds

b_{1} is quasi_total
by Th19;

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

b

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

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

scheme :: FUNCT_2:sch 3

FuncExD{ F_{1}() -> non empty set , F_{2}() -> non empty set , P_{1}[ set , set ] } :

provided

FuncExD{ F

provided

proof end;

scheme :: FUNCT_2:sch 4

LambdaD{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}( Element of F_{1}()) -> Element of F_{2}() } :

LambdaD{ F

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

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 )

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 )

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

proof end;

scheme :: FUNCT_2:sch 5

Lambda1C{ F_{1}() -> set , F_{2}() -> set , P_{1}[ set ], F_{3}( set ) -> set , F_{4}( set ) -> set } :

Lambda1C{ F

ex f being Function of F_{1}(),F_{2}() st

for x being set st x in F_{1}() holds

( ( P_{1}[x] implies f . x = F_{3}(x) ) & ( P_{1}[x] implies f . x = F_{4}(x) ) )

providedfor x being set st x in F

( ( P

A1:
for x being set st x in F_{1}() holds

( ( P_{1}[x] implies F_{3}(x) in F_{2}() ) & ( P_{1}[x] implies F_{4}(x) in F_{2}() ) )

( ( P

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

proof end;

theorem :: FUNCT_2:131

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 ;

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;

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;
let f be Function of X,X;

cluster <:f,X,X:> -> total ;

coherence

<:f,X,X:> is total by Th133;

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

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

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;

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

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 )

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 )

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

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

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 )

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;

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;

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

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

proof end;

theorem :: FUNCT_2:160

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}

for f being Function of X,Y st ( Y = {} implies X = {} ) holds

TotFuncs <:f,X,Y:> = {f}

proof end;

theorem :: FUNCT_2:162

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}

for f being PartFunc of X,{y}

for g being Function of X,{y} holds TotFuncs f = {g}

proof end;

theorem :: FUNCT_2:165

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

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

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

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 b_{1} being Function of A,B holds not b_{1} is empty
by Def1, RELAT_1:60;

end;
cluster Function-like quasi_total -> non empty Element of bool [:A,B:];

coherence

for b

begin

scheme :: FUNCT_2:sch 6

LambdaSep1{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}() -> Element of F_{1}(), F_{4}() -> Element of F_{2}(), F_{5}( set ) -> Element of F_{2}() } :

LambdaSep1{ F

ex f being Function of F_{1}(),F_{2}() st

( f . F_{3}() = F_{4}() & ( for x being Element of F_{1}() st x <> F_{3}() holds

f . x = F_{5}(x) ) )

( f . F

f . x = F

proof end;

scheme :: FUNCT_2:sch 7

LambdaSep2{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}() -> Element of F_{1}(), F_{4}() -> Element of F_{1}(), F_{5}() -> Element of F_{2}(), F_{6}() -> Element of F_{2}(), F_{7}( set ) -> Element of F_{2}() } :

LambdaSep2{ F

ex f being Function of F_{1}(),F_{2}() st

( f . F_{3}() = F_{5}() & f . F_{4}() = F_{6}() & ( for x being Element of F_{1}() st x <> F_{3}() & x <> F_{4}() holds

f . x = F_{7}(x) ) )

provided
( f . F

f . x = F

proof end;

theorem :: FUNCT_2:169

proof end;

scheme :: FUNCT_2:sch 8

FunctRealEx{ F_{1}() -> non empty set , F_{2}() -> set , F_{3}( set ) -> set } :

provided

FunctRealEx{ F

provided

proof end;

scheme :: FUNCT_2:sch 9

KappaMD{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}( set ) -> set } :

provided

KappaMD{ F

provided

proof end;

scheme :: FUNCT_2:sch 10

NonUniqExMD{ F_{1}() -> non empty set , F_{2}() -> non empty set , P_{1}[ set , set ] } :

provided

NonUniqExMD{ F

provided

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

for b_{1} being Function of A,B holds

( b_{1} = pr1 f iff for x being Element of A holds b_{1} . x = (f . x) `1 )

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

for b_{1} being Function of A,C holds

( b_{1} = pr2 f iff for x being Element of A holds b_{1} . x = (f . x) `2 )

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

( b

proof end;

:: original: pr2redefine 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 b

( b

proof 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 b

( b

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

( b

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

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

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

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

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

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 )

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

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

proof end;

theorem :: FUNCT_2:175

proof end;

scheme :: FUNCT_2:sch 11

MChoice{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}( set ) -> set } :

provided

MChoice{ F

provided

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

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

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 `)

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

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 b_{1} being Subset-Family of T st

for A being Subset of T holds

( A in b_{1} iff ex B being Subset of S st

( B in G & A = f " B ) )

for b_{1}, b_{2} being Subset-Family of T st ( for A being Subset of T holds

( A in b_{1} iff ex B being Subset of S st

( B in G & A = f " B ) ) ) & ( for A being Subset of T holds

( A in b_{2} iff ex B being Subset of S st

( B in G & A = f " B ) ) ) holds

b_{1} = b_{2}

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

for A being Subset of T holds

( A in b

( B in G & A = f " B ) )

proof end;

uniqueness for b

( A in b

( B in G & A = f " B ) ) ) & ( for A being Subset of T holds

( A in b

( B in G & A = f " B ) ) ) holds

b

proof 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 b

( b

( A in b

( 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

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 b_{1} being Subset-Family of S st

for A being Subset of S holds

( A in b_{1} iff ex B being Subset of T st

( B in G & A = f .: B ) )

for b_{1}, b_{2} being Subset-Family of S st ( for A being Subset of S holds

( A in b_{1} iff ex B being Subset of T st

( B in G & A = f .: B ) ) ) & ( for A being Subset of S holds

( A in b_{2} iff ex B being Subset of T st

( B in G & A = f .: B ) ) ) holds

b_{1} = b_{2}

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

for A being Subset of S holds

( A in b

( B in G & A = f .: B ) )

proof end;

uniqueness for b

( A in b

( B in G & A = f .: B ) ) ) & ( for A being Subset of S holds

( A in b

( B in G & A = f .: B ) ) ) holds

b

proof 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 b

( b

( A in b

( 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

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

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

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

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

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

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

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

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)

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)

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} )

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

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

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

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)

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)

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

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

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)]

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)

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

end;
cluster Funcs (A,B) -> functional ;

coherence

Funcs (A,B) is functional

proof 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 b_{1} being non empty set st

for x being Element of b_{1} holds x is Function of A,B

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

for x being Element of b

proof end;

:: deftheorem Def13 defines FUNCTION_DOMAIN FUNCT_2:def 13 :

for A, B being set

for b

( b

registration

let A, B be set ;

cluster -> functional FUNCTION_DOMAIN of A,B;

coherence

for b_{1} being FUNCTION_DOMAIN of A,B holds b_{1} is functional

end;
cluster -> functional FUNCTION_DOMAIN of A,B;

coherence

for b

proof end;

theorem :: FUNCT_2:198

proof end;

theorem Th199: :: FUNCT_2:199

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 b_{1} being Element of F holds b_{1} is Function of A,B
by Def13;

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

registration

let I be set ;

cluster id I -> I -defined total I -defined Function;

coherence

for b_{1} being I -defined Function st b_{1} = id I holds

b_{1} is total
;

end;
cluster id I -> I -defined total I -defined Function;

coherence

for b

b

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 b_{1} being Element of A holds

( b_{1} = F /. x iff b_{1} = F . x )

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

( b

proof 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 b_{1} -valued Function holds dom (f * g) = dom g

for f being Function of X,X

for g being b

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

for f being Function of X,X st ( for x being Element of X holds f . x = x ) holds

f = id X

proof end;