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

::

:: Received April 6, 1989

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

:: 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 = {} ) ) );

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

registration

let X, Y be set ;

coherence

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

b_{1} is quasi_total

end;
coherence

for b

b

proof end;

registration

let X be empty set ;

let Y be set ;

coherence

for b_{1} being Relation of X,Y st b_{1} is quasi_total holds

b_{1} is total
;

end;
let Y be set ;

coherence

for b

b

registration

let X be set ;

let Y be non empty set ;

coherence

for b_{1} being Relation of X,Y st b_{1} is quasi_total holds

b_{1} is total

end;
let Y be non empty set ;

coherence

for b

b

proof end;

registration

let X be set ;

coherence

for b_{1} being Relation of X,X st b_{1} is quasi_total holds

b_{1} is total

end;
coherence

for b

b

proof end;

theorem :: FUNCT_2:3

for X, Y being set

for f being Function st dom f = X & ( for x being set st x in X holds

f . x in Y ) holds

f is Function of X,Y

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

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

definition

let X, Y be set ;

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 for x being set holds

( x in it iff ex f being Function st

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

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_{3} being set holds

( b_{3} = Funcs (X,Y) iff for x being set holds

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

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

for X, Y, b

( b

( x in b

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

registration
end;

registration
end;

theorem :: FUNCT_2:10

for X, Y being set

for f being Function of X,Y st ( for y being set st y in Y holds

ex x being set st

( x in X & y = f . x ) ) holds

rng f = Y

for f being Function of X,Y st ( for y being set st y in Y holds

ex x being set st

( x in X & y = f . x ) ) holds

rng f = Y

proof end;

theorem Th11: :: FUNCT_2:11

for X, Y, y being set

for f being Function of X,Y st y in rng f holds

ex x being set st

( x in X & f . x = y )

for f being Function of X,Y st y in rng f holds

ex x being set st

( x in X & f . x = y )

proof end;

theorem Th12: :: FUNCT_2:12

for X, Y being set

for f1, f2 being Function of X,Y st ( for x being set st x in X holds

f1 . x = f2 . x ) holds

f1 = f2

for f1, f2 being Function of X,Y st ( for x being set st x in X holds

f1 . x = f2 . x ) holds

f1 = f2

proof end;

theorem Th13: :: FUNCT_2:13

for X, Y, Z being set

for f being quasi_total Relation of X,Y

for g being quasi_total Relation of Y,Z st ( not Y = {} or Z = {} or X = {} ) holds

f * g is quasi_total

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

for f being Function of X,Y

for g being Function of Y,Z st Z <> {} & rng f = Y & rng g = Z holds

rng (g * f) = Z

proof end;

theorem Th15: :: FUNCT_2:15

for X, Y, x being set

for f being Function of X,Y

for g being Function st Y <> {} & x in X holds

(g * f) . x = g . (f . x)

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 )

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

for f being Function of X,Y

for g being Function of Y,X st f * g = id Y holds

rng f = Y

proof end;

theorem :: FUNCT_2:19

for X, Y being set

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

( f is one-to-one iff for x1, x2 being set st x1 in X & x2 in X & f . x1 = f . x2 holds

x1 = x2 )

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

( f is one-to-one iff for x1, x2 being set st x1 in X & x2 in X & f . x1 = f . x2 holds

x1 = x2 )

proof end;

theorem :: FUNCT_2:20

for X, Y, Z being set

for f being Function of X,Y

for g being Function of Y,Z st ( Z = {} implies Y = {} ) & g * f is one-to-one holds

f is one-to-one

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 )

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

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_{1} -valued Relation holds

( f is onto iff rng f = Y );

for Y being set

for f being b

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

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 )

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

for f being Function of X,Y st f is one-to-one & rng f = Y holds

f " is Function of Y,X

proof end;

theorem :: FUNCT_2:26

for X, Y, x being set

for f being Function of X,Y st Y <> {} & f is one-to-one & x in X holds

(f ") . (f . x) = x

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

for Y, Z being non empty set

for f being Function of X,Y

for g being Function of Y,Z st f is onto & g is onto holds

g * f is onto

proof end;

theorem :: FUNCT_2:28

for X, Y being set

for f being Function of X,Y

for g being Function of Y,X st X <> {} & Y <> {} & rng f = Y & f is one-to-one & ( for y, x being set holds

( y in Y & g . y = x iff ( x in X & f . x = y ) ) ) holds

g = f "

for f being Function of X,Y

for g being Function of Y,X st X <> {} & Y <> {} & rng f = Y & f is one-to-one & ( for y, x being set holds

( y in Y & g . y = x iff ( x in X & f . x = y ) ) ) holds

g = f "

proof end;

theorem :: FUNCT_2:29

for X, Y being set

for f being Function of X,Y st Y <> {} & rng f = Y & f is one-to-one holds

( (f ") * f = id X & f * (f ") = id Y )

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 "

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

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

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

theorem :: FUNCT_2:34

for X, Y, x, Z being set

for f being Function of X,Y st Y <> {} & x in X & f . x in Z holds

(Z |` f) . x = f . x

for f being Function of X,Y st Y <> {} & x in X & f . x in Z holds

(Z |` f) . x = f . x

proof end;

theorem :: FUNCT_2:35

for X, Y, P being set

for f being Function of X,Y st Y <> {} holds

for y being set st ex x being set st

( x in X & x in P & y = f . x ) holds

y in f .: P

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

for X, Y, Q being set

for f being Function of X,Y st Y <> {} holds

for x being set holds

( x in f " Q iff ( x in X & f . x in Q ) )

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

for X, Y being set

for f being Function of X,Y holds

( ( for y being set st y in Y holds

f " {y} <> {} ) iff rng f = Y )

for f being Function of X,Y holds

( ( for y being set st y in Y holds

f " {y} <> {} ) iff rng f = Y )

proof end;

theorem Th42: :: FUNCT_2:42

for X, Y, P being set

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

P c= f " (f .: P)

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

for X, Y, Z, Q being set

for f being Function of X,Y

for g being Function of Y,Z st ( Z = {} implies Y = {} ) holds

f " Q c= (g * f) " (g .: Q)

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;

registration

let X, Y be set ;

let f be quasi_total PartFunc of X,Y;

let g be quasi_total PartFunc of X,X;

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;

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;

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;

coherence

for b

b

proof end;

theorem Th56: :: FUNCT_2:56

for X being set

for f being Function of X,X holds

( f is one-to-one iff for x1, x2 being set st x1 in X & x2 in X & f . x1 = f . x2 holds

x1 = x2 )

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;

:: deftheorem Def4 defines bijective FUNCT_2:def 4 :

for X, Y being set

for f being b_{1} -defined b_{2} -valued Function holds

( f is bijective iff ( f is one-to-one & f is onto ) );

for X, Y being set

for f being b

( f is bijective iff ( f is one-to-one & f is onto ) );

registration

let X, Y be set ;

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;

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

for b

( b

coherence

for b

b

registration

let X be set ;

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

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

existence ex b

proof end;

theorem Th57: :: FUNCT_2:57

for X being set

for f being Function of X,X st f is one-to-one & rng f = X holds

f is Permutation of X

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

registration

let X be set ;

let f, g be 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;

coherence

for b

b

proof end;

registration

let X be set ;

let f, g be 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;

coherence

for b

b

registration

let X be set ;

coherence

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

b_{1} is bijective

end;
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 Th62: :: FUNCT_2:62

for X, P being set

for f being Permutation of X st P c= X holds

( f .: (f " P) = P & f " (f .: P) = P )

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;

coherence

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

b_{1} is quasi_total
by Th13;

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;

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;

theorem Th63: :: FUNCT_2:63

for X, Y being set

for f1, f2 being Function of X,Y st ( for x being Element of X holds f1 . x = f2 . x ) holds

f1 = f2

for f1, f2 being Function of X,Y st ( for x being Element of X holds f1 . x = f2 . x ) holds

f1 = f2

proof end;

theorem Th64: :: FUNCT_2:64

for X, Y, P being set

for f being Function of X,Y

for y being set st y in f .: P holds

ex x being set st

( x in X & x in P & y = f . x )

for f being Function of X,Y

for y being set st y in f .: P holds

ex x being set st

( x in X & x in P & y = f . x )

proof end;

theorem :: FUNCT_2:65

for X, Y, P being set

for f being Function of X,Y

for y being set st y in f .: P holds

ex c being Element of X st

( c in P & y = f . c )

for f being Function of X,Y

for y being set st y in f .: P holds

ex c being Element of X st

( c in P & y = f . c )

proof end;

begin

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

theorem :: FUNCT_2:69

theorem :: FUNCT_2:70

registration
end;

theorem Th71: :: FUNCT_2:71

for X, Y being set

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

ex g being Function of X,Y st

for x being set st x in dom f holds

g . x = f . x

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

theorem :: FUNCT_2:74

theorem Th75: :: FUNCT_2:75

for X, Y being set

for f being PartFunc of X,Y

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

( f tolerates g iff for x being set st x in dom f holds

f . x = g . x )

for f being PartFunc of X,Y

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

( f tolerates g iff for x being set st x in dom f holds

f . x = g . x )

proof end;

theorem :: FUNCT_2:76

for X being set

for f being PartFunc of X,X

for g being Function of X,X holds

( f tolerates g iff for x being set st x in dom f holds

f . x = g . x )

for f being PartFunc of X,X

for g being Function of X,X holds

( f tolerates g iff for x being set st x in dom f holds

f . x = g . x )

proof end;

theorem Th77: :: FUNCT_2:77

for X, Y being set

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

ex g being Function of X,Y st f tolerates g

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

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 )

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

theorem :: FUNCT_2:81

theorem Th82: :: FUNCT_2:82

for X, Y being set

for f being PartFunc of X,Y

for g being set st g in TotFuncs f holds

g is Function of X,Y

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

theorem :: FUNCT_2:86

theorem :: FUNCT_2:87

for X, y being set

for f being PartFunc of X,{y}

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

for f being PartFunc of X,{y}

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

proof end;

theorem Th89: :: FUNCT_2:89

for X, Y being set

for f, g being PartFunc of X,Y st dom g c= dom f & TotFuncs f c= TotFuncs g holds

g c= f

for f, g being PartFunc of X,Y st dom g c= dom f & TotFuncs f c= TotFuncs g holds

g c= f

proof end;

theorem Th90: :: FUNCT_2:90

for X, Y being set

for f, g being PartFunc of X,Y st TotFuncs f c= TotFuncs g & ( for y being set holds Y <> {y} ) holds

g c= f

for f, g being PartFunc of X,Y st TotFuncs f c= TotFuncs g & ( for y being set holds Y <> {y} ) holds

g c= f

proof end;

theorem :: FUNCT_2:91

for X, Y being set

for f, g being PartFunc of X,Y st ( for y being set holds Y <> {y} ) & TotFuncs f = TotFuncs g holds

f = g

for f, g being PartFunc of X,Y st ( for y being set holds Y <> {y} ) & TotFuncs f = TotFuncs g holds

f = g

proof end;

:: from WAYBEL_1

registration

let A, B be non empty set ;

coherence

for b_{1} being Function of A,B holds not b_{1} is empty
by Def1, RELAT_1:38;

end;
coherence

for b

begin

:: from RLVECT_2

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;

:: from ALTCAT_1, PRALG_3

:: from SUPINF_2

:: from YELLOW_2

definition

let A, B, C be non empty set ;

let f be Function of A,[:B,C:];

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 )

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

pr1 f is Function of A,B

proof end;

compatibility for b

( b

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

pr2 f is Function of A,C

proof end;

compatibility for b

( b

proof 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_{5} being Function of A,B holds

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

for A, B, C being non empty set

for f being Function of A,[:B,C:]

for b

( b

:: 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_{5} being Function of A,C holds

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

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;

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

( A1 = A2 & ( for a being Element of A1 holds f1 . a = f2 . a ) );

compatibility redefine pred f1 = f2 means :: FUNCT_2:def 7

( A1 = A2 & ( for a being Element of A1 holds f1 . a = f2 . a ) );

( f1 = f2 iff ( A1 = A2 & ( for a being Element of A1 holds f1 . a = f2 . a ) ) )

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

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;

( f1 = f2 iff for a being Element of A holds f1 . a = f2 . a ) by Th63;

end;
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 redefine pred f1 = f2 means :: FUNCT_2:def 8

for a being Element of A holds f1 . a = f2 . a;

( f1 = f2 iff for a being Element of A holds f1 . a = f2 . a ) by Th63;

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

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

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

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

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;

:: Moved from FINSEQ_4 by AK on 2007.10.09

theorem Th99: :: FUNCT_2:99

for X, D being non empty set

for p being Function of X,D

for i being Element of X holds p /. i = p . i

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;

correctness

compatibility

p /. i = p . i;

by Th99;

end;
let p be Function of X,D;

let i be Element of X;

correctness

compatibility

p /. i = p . i;

by Th99;

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

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

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;

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 :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 for A being Subset of T holds

( A in it iff ex B being Subset of S st

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

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 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_{5} being Subset-Family of T holds

( b_{5} = f " G iff for A being Subset of T holds

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

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

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

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;

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 :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 for A being Subset of S holds

( A in it iff ex B being Subset of T st

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

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 Def10 defines .: FUNCT_2:def 10 :

for T, S being non empty set

for f being Function of T,S

for G being Subset-Family of T

for b_{5} being Subset-Family of S holds

( b_{5} = f .: G iff for A being Subset of S holds

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

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

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

for T, S being non empty set

for f being Function of T,S

for A, B being Subset-Family of T st A c= B holds

f .: A c= f .: B

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

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

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

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

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.

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

coherence

p * f is Function of X,Z

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

coherence

p * f is Function of X,Z

proof 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_{2} -valued Function st rng f c= dom p holds

p /* f = p * f;

for X, Z being set

for Y being non empty set

for f being Function of X,Y

for p being b

p /* f = p * f;

theorem Th108: :: FUNCT_2:108

for Z, X being set

for Y being non empty set

for f being Function of X,Y

for p being PartFunc of Y,Z

for x being Element of X st X <> {} & rng f c= dom p holds

(p /* f) . x = p . (f . x)

for Y being non empty set

for f being Function of X,Y

for p being PartFunc of Y,Z

for x being Element of X st X <> {} & rng f c= dom p holds

(p /* f) . x = p . (f . x)

proof end;

theorem Th109: :: FUNCT_2:109

for Z, X being set

for Y being non empty set

for f being Function of X,Y

for p being PartFunc of Y,Z

for x being Element of X st X <> {} & rng f c= dom p holds

(p /* f) . x = p /. (f . x)

for Y being non empty set

for f being Function of X,Y

for p being PartFunc of Y,Z

for x being Element of X st X <> {} & rng f c= dom p holds

(p /* f) . x = p /. (f . x)

proof end;

theorem :: FUNCT_2:110

for Z, X being set

for Y being non empty set

for f being Function of X,Y

for p being PartFunc of Y,Z

for g being Function of X,X st rng f c= dom p holds

(p /* f) * g = p /* (f * g)

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

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

for x being Element of A

for f being Function of A,B holds f . x in rng f

proof end;

:: missing, 2008.09.14, A.T.

theorem Th113: :: FUNCT_2:113

for y, A, B being set

for f being Function of A,B st y in rng f holds

ex x being Element of A st y = f . x

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

for A, B being non empty set

for f being Function of A,B st ( for x being Element of A holds f . x in Z ) holds

rng f c= Z

proof end;

theorem :: FUNCT_2:115

for Y, X being non empty set

for Z being set

for f being Function of X,Y

for g being PartFunc of Y,Z

for x being Element of X st g is total holds

(g /* f) . x = g . (f . x)

for Z being set

for f being Function of X,Y

for g being PartFunc of Y,Z

for x being Element of X st g is total holds

(g /* f) . x = g . (f . x)

proof end;

theorem :: FUNCT_2:116

for Y, X being non empty set

for Z being set

for f being Function of X,Y

for g being PartFunc of Y,Z

for x being Element of X st g is total holds

(g /* f) . x = g /. (f . x)

for Z being set

for f being Function of X,Y

for g being PartFunc of Y,Z

for x being Element of X st g is total holds

(g /* f) . x = g /. (f . x)

proof end;

theorem Th117: :: FUNCT_2:117

for X, Y being non empty set

for Z, S being set

for f being Function of X,Y

for g being PartFunc of Y,Z st rng f c= dom (g | S) holds

(g | S) /* f = g /* f

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

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

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)

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.

definition

let A, B be set ;

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 :Def12: :: FUNCT_2:def 12

for x being Element of it holds x is Function of A,B;

existence for x being Element of it holds x is Function of A,B;

ex b

for x being Element of b

proof end;

:: deftheorem Def12 defines FUNCTION_DOMAIN FUNCT_2:def 12 :

for A, B being set

for b_{3} being non empty set holds

( b_{3} is FUNCTION_DOMAIN of A,B iff for x being Element of b_{3} holds x is Function of A,B );

for A, B being set

for b

( b

registration

let A, B be set ;

coherence

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

end;
coherence

for b

proof end;

definition

let A be set ;

let B be non empty set ;

:: original: Funcs

redefine func Funcs (A,B) -> FUNCTION_DOMAIN of A,B;

coherence

Funcs (A,B) is FUNCTION_DOMAIN of A,B by Th122;

let F be FUNCTION_DOMAIN of A,B;

:: original: Element

redefine mode Element of F -> Function of A,B;

coherence

for b_{1} being Element of F holds b_{1} is Function of A,B
by Def12;

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

let F be FUNCTION_DOMAIN of A,B;

:: original: Element

redefine mode Element of F -> Function of A,B;

coherence

for b

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

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 ;

compatibility

for b

( b

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

for X, A being non empty set

for F being Function of X,A

for x being set st x in X holds

F /. x = F . x;

theorem :: FUNCT_2:123

for X being non empty set

for f being Function of X,X

for g being 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: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

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

f = id X

proof end;

:: Moved from GROUP_9, AK