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

::

:: Received March 3, 1989

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

:: deftheorem Def1 defines Function-like FUNCT_1:def 1 :

for X being set holds

( X is Function-like iff for x, y1, y2 being object st [x,y1] in X & [x,y2] in X holds

y1 = y2 );

for X being set holds

( X is Function-like iff for x, y1, y2 being object st [x,y1] in X & [x,y2] in X holds

y1 = y2 );

definition

let f be Function;

let x be object ;

existence

( ( x in dom f implies ex b_{1} being set st [x,b_{1}] in f ) & ( not x in dom f implies ex b_{1} being set st b_{1} = {} ) )

for b_{1}, b_{2} being set holds

( ( x in dom f & [x,b_{1}] in f & [x,b_{2}] in f implies b_{1} = b_{2} ) & ( not x in dom f & b_{1} = {} & b_{2} = {} implies b_{1} = b_{2} ) )
by Def1;

consistency

for b_{1} being set holds verum
;

end;
let x be object ;

existence

( ( x in dom f implies ex b

proof end;

uniqueness for b

( ( x in dom f & [x,b

consistency

for b

:: deftheorem Def2 defines . FUNCT_1:def 2 :

for f being Function

for x being object

for b_{3} being set holds

( ( x in dom f implies ( b_{3} = f . x iff [x,b_{3}] in f ) ) & ( not x in dom f implies ( b_{3} = f . x iff b_{3} = {} ) ) );

for f being Function

for x being object

for b

( ( x in dom f implies ( b

theorem Th2: :: FUNCT_1:2

for f, g being Function st dom f = dom g & ( for x being object st x in dom f holds

f . x = g . x ) holds

f = g

f . x = g . x ) holds

f = g

proof end;

definition

let f be Function;

for b_{1} being set holds

( b_{1} = rng f iff for y being object holds

( y in b_{1} iff ex x being object st

( x in dom f & y = f . x ) ) )

end;
redefine func rng f means :Def3: :: FUNCT_1:def 3

for y being object holds

( y in it iff ex x being object st

( x in dom f & y = f . x ) );

compatibility for y being object holds

( y in it iff ex x being object st

( x in dom f & y = f . x ) );

for b

( b

( y in b

( x in dom f & y = f . x ) ) )

proof end;

:: deftheorem Def3 defines rng FUNCT_1:def 3 :

for f being Function

for b_{2} being set holds

( b_{2} = rng f iff for y being object holds

( y in b_{2} iff ex x being object st

( x in dom f & y = f . x ) ) );

for f being Function

for b

( b

( y in b

( x in dom f & y = f . x ) ) );

theorem :: FUNCT_1:3

scheme :: FUNCT_1:sch 2

FuncEx{ F_{1}() -> set , P_{1}[ object , object ] } :

FuncEx{ F

ex f being Function st

( dom f = F_{1}() & ( for x being object st x in F_{1}() holds

P_{1}[x,f . x] ) )

provided( dom f = F

P

A1:
for x, y1, y2 being object st x in F_{1}() & P_{1}[x,y1] & P_{1}[x,y2] holds

y1 = y2 and

A2: for x being object st x in F_{1}() holds

ex y being object st P_{1}[x,y]

y1 = y2 and

A2: for x being object st x in F

ex y being object st P

proof end;

theorem Th5: :: FUNCT_1:5

for X being set st X <> {} holds

for y being object ex f being Function st

( dom f = X & rng f = {y} )

for y being object ex f being Function st

( dom f = X & rng f = {y} )

proof end;

theorem :: FUNCT_1:9

for Y being set

for f being Function st ( for y being object st y in Y holds

ex x being object st

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

Y c= rng f

for f being Function st ( for y being object st y in Y holds

ex x being object st

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

Y c= rng f

proof end;

registration
end;

theorem :: FUNCT_1:10

for f, g, h being Function st ( for x being object holds

( x in dom h iff ( x in dom f & f . x in dom g ) ) ) & ( for x being object st x in dom h holds

h . x = g . (f . x) ) holds

h = g * f

( x in dom h iff ( x in dom f & f . x in dom g ) ) ) & ( for x being object st x in dom h holds

h . x = g . (f . x) ) holds

h = g * f

proof end;

theorem Th11: :: FUNCT_1:11

for x being object

for f, g being Function holds

( x in dom (g * f) iff ( x in dom f & f . x in dom g ) )

for f, g being Function holds

( x in dom (g * f) iff ( x in dom f & f . x in dom g ) )

proof end;

theorem :: FUNCT_1:16

for Y being set

for f being Function st rng f c= Y & ( for g, h being Function st dom g = Y & dom h = Y & g * f = h * f holds

g = h ) holds

Y = rng f

for f being Function st rng f c= Y & ( for g, h being Function st dom g = Y & dom h = Y & g * f = h * f holds

g = h ) holds

Y = rng f

proof end;

registration
end;

theorem Th17: :: FUNCT_1:17

for X being set

for f being Function holds

( f = id X iff ( dom f = X & ( for x being object st x in X holds

f . x = x ) ) )

for f being Function holds

( f = id X iff ( dom f = X & ( for x being object st x in X holds

f . x = x ) ) )

proof end;

theorem :: FUNCT_1:20

for X being set

for x being object

for f being Function st x in (dom f) /\ X holds

f . x = (f * (id X)) . x

for x being object

for f being Function st x in (dom f) /\ X holds

f . x = (f * (id X)) . x

proof end;

theorem :: FUNCT_1:21

for Y being set

for x being object

for f being Function holds

( x in dom ((id Y) * f) iff ( x in dom f & f . x in Y ) )

for x being object

for f being Function holds

( x in dom ((id Y) * f) iff ( x in dom f & f . x in Y ) )

proof end;

:: deftheorem Def4 defines one-to-one FUNCT_1:def 4 :

for f being Function holds

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

x1 = x2 );

for f being Function holds

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

x1 = x2 );

theorem :: FUNCT_1:26

for f, g being Function st g * f is one-to-one & rng f = dom g holds

( f is one-to-one & g is one-to-one )

( f is one-to-one & g is one-to-one )

proof end;

theorem :: FUNCT_1:27

for f being Function holds

( f is one-to-one iff for g, h being Function st rng g c= dom f & rng h c= dom f & dom g = dom h & f * g = f * h holds

g = h )

( f is one-to-one iff for g, h being Function st rng g c= dom f & rng h c= dom f & dom g = dom h & f * g = f * h holds

g = h )

proof end;

theorem :: FUNCT_1:28

for X being set

for f, g being Function st dom f = X & dom g = X & rng g c= X & f is one-to-one & f * g = f holds

g = id X

for f, g being Function st dom f = X & dom g = X & rng g c= X & f is one-to-one & f * g = f holds

g = id X

proof end;

registration
end;

::$CT

:: deftheorem Def5 defines " FUNCT_1:def 5 :

for f being Function st f is one-to-one holds

f " = f ~ ;

for f being Function st f is one-to-one holds

f " = f ~ ;

theorem Th31: :: FUNCT_1:32

for f being Function st f is one-to-one holds

for g being Function holds

( g = f " iff ( dom g = rng f & ( for y, x being object holds

( y in rng f & x = g . y iff ( x in dom f & y = f . x ) ) ) ) )

for g being Function holds

( g = f " iff ( dom g = rng f & ( for y, x being object holds

( y in rng f & x = g . y iff ( x in dom f & y = f . x ) ) ) ) )

proof end;

theorem Th33: :: FUNCT_1:34

for x being object

for f being Function st f is one-to-one & x in dom f holds

( x = (f ") . (f . x) & x = ((f ") * f) . x )

for f being Function st f is one-to-one & x in dom f holds

( x = (f ") . (f . x) & x = ((f ") * f) . x )

proof end;

theorem Th34: :: FUNCT_1:35

for y being object

for f being Function st f is one-to-one & y in rng f holds

( y = f . ((f ") . y) & y = (f * (f ")) . y )

for f being Function st f is one-to-one & y in rng f holds

( y = f . ((f ") . y) & y = (f * (f ")) . y )

proof end;

theorem :: FUNCT_1:38

for f, g being Function st f is one-to-one & dom f = rng g & rng f = dom g & ( for x, y being object st x in dom f & y in dom g holds

( f . x = y iff g . y = x ) ) holds

g = f "

( f . x = y iff g . y = x ) ) holds

g = f "

proof end;

registration

let f be one-to-one Function;

coherence

f " is one-to-one by Th39;

let g be one-to-one Function;

coherence

g * f is one-to-one by Th24;

end;
coherence

f " is one-to-one by Th39;

let g be one-to-one Function;

coherence

g * f is one-to-one by Th24;

Lm1: for X being set

for f, g1, g2 being Function st rng g2 = X & f * g2 = id (dom g1) & g1 * f = id X holds

g1 = g2

proof end;

theorem :: FUNCT_1:46

for X being set

for f, g being Function st dom g = (dom f) /\ X & ( for x being object st x in dom g holds

g . x = f . x ) holds

g = f | X

for f, g being Function st dom g = (dom f) /\ X & ( for x being object st x in dom g holds

g . x = f . x ) holds

g = f | X

proof end;

theorem Th46: :: FUNCT_1:47

for X being set

for x being object

for f being Function st x in dom (f | X) holds

(f | X) . x = f . x

for x being object

for f being Function st x in dom (f | X) holds

(f | X) . x = f . x

proof end;

theorem Th47: :: FUNCT_1:48

for X being set

for x being object

for f being Function st x in (dom f) /\ X holds

(f | X) . x = f . x

for x being object

for f being Function st x in (dom f) /\ X holds

(f | X) . x = f . x

proof end;

theorem :: FUNCT_1:50

for X being set

for x being object

for f being Function st x in dom f & x in X holds

f . x in rng (f | X)

for x being object

for f being Function st x in dom f & x in X holds

f . x in rng (f | X)

proof end;

theorem :: FUNCT_1:51

theorem Th52: :: FUNCT_1:53

for Y being set

for f, g being Function holds

( g = Y |` f iff ( ( for x being object holds

( x in dom g iff ( x in dom f & f . x in Y ) ) ) & ( for x being object st x in dom g holds

g . x = f . x ) ) )

for f, g being Function holds

( g = Y |` f iff ( ( for x being object holds

( x in dom g iff ( x in dom f & f . x in Y ) ) ) & ( for x being object st x in dom g holds

g . x = f . x ) ) )

proof end;

theorem :: FUNCT_1:54

theorem :: FUNCT_1:55

theorem :: FUNCT_1:57

definition

let f be Function;

let X be set ;

for b_{1} being set holds

( b_{1} = f .: X iff for y being object holds

( y in b_{1} iff ex x being object st

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

end;
let X be set ;

redefine func f .: X means :Def6: :: FUNCT_1:def 6

for y being object holds

( y in it iff ex x being object st

( x in dom f & x in X & y = f . x ) );

compatibility for y being object holds

( y in it iff ex x being object st

( x in dom f & x in X & y = f . x ) );

for b

( b

( y in b

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

proof end;

:: deftheorem Def6 defines .: FUNCT_1:def 6 :

for f being Function

for X being set

for b_{3} being set holds

( b_{3} = f .: X iff for y being object holds

( y in b_{3} iff ex x being object st

( x in dom f & x in X & y = f . x ) ) );

for f being Function

for X being set

for b

( b

( y in b

( x in dom f & x in X & y = f . x ) ) );

theorem :: FUNCT_1:60

for x1, x2 being object

for f being Function st x1 in dom f & x2 in dom f holds

f .: {x1,x2} = {(f . x1),(f . x2)}

for f being Function st x1 in dom f & x2 in dom f holds

f .: {x1,x2} = {(f . x1),(f . x2)}

proof end;

theorem Th61: :: FUNCT_1:62

for X1, X2 being set

for f being Function st f is one-to-one holds

f .: (X1 /\ X2) = (f .: X1) /\ (f .: X2)

for f being Function st f is one-to-one holds

f .: (X1 /\ X2) = (f .: X1) /\ (f .: X2)

proof end;

theorem :: FUNCT_1:63

for f being Function st ( for X1, X2 being set holds f .: (X1 /\ X2) = (f .: X1) /\ (f .: X2) ) holds

f is one-to-one

f is one-to-one

proof end;

theorem :: FUNCT_1:64

for X1, X2 being set

for f being Function st f is one-to-one holds

f .: (X1 \ X2) = (f .: X1) \ (f .: X2)

for f being Function st f is one-to-one holds

f .: (X1 \ X2) = (f .: X1) \ (f .: X2)

proof end;

theorem :: FUNCT_1:65

for f being Function st ( for X1, X2 being set holds f .: (X1 \ X2) = (f .: X1) \ (f .: X2) ) holds

f is one-to-one

f is one-to-one

proof end;

definition

let f be Function;

let Y be set ;

for b_{1} being set holds

( b_{1} = f " Y iff for x being object holds

( x in b_{1} iff ( x in dom f & f . x in Y ) ) )

end;
let Y be set ;

redefine func f " Y means :Def7: :: FUNCT_1:def 7

for x being object holds

( x in it iff ( x in dom f & f . x in Y ) );

compatibility for x being object holds

( x in it iff ( x in dom f & f . x in Y ) );

for b

( b

( x in b

proof end;

:: deftheorem Def7 defines " FUNCT_1:def 7 :

for f being Function

for Y being set

for b_{3} being set holds

( b_{3} = f " Y iff for x being object holds

( x in b_{3} iff ( x in dom f & f . x in Y ) ) );

for f being Function

for Y being set

for b

( b

( x in b

theorem :: FUNCT_1:73

for Y being set

for R being Relation st ( for y being object st y in Y holds

R " {y} <> {} ) holds

Y c= rng R

for R being Relation st ( for y being object st y in Y holds

R " {y} <> {} ) holds

Y c= rng R

proof end;

theorem Th73: :: FUNCT_1:74

for f being Function holds

( ( for y being object st y in rng f holds

ex x being object st f " {y} = {x} ) iff f is one-to-one )

( ( for y being object st y in rng f holds

ex x being object st f " {y} = {x} ) iff f is one-to-one )

proof end;

:: SUPLEMENT

theorem :: FUNCT_1:86

for Y being set

for f, g, h being Function st Y = rng f & dom g = Y & dom h = Y & g * f = h * f holds

g = h

for f, g, h being Function st Y = rng f & dom g = Y & dom h = Y & g * f = h * f holds

g = h

proof end;

theorem :: FUNCT_1:87

for X1, X2 being set

for f being Function st f .: X1 c= f .: X2 & X1 c= dom f & f is one-to-one holds

X1 c= X2

for f being Function st f .: X1 c= f .: X2 & X1 c= dom f & f is one-to-one holds

X1 c= X2

proof end;

theorem :: FUNCT_1:89

for f being Function holds

( f is one-to-one iff for y being object ex x being object st f " {y} c= {x} )

( f is one-to-one iff for y being object ex x being object st f " {y} c= {x} )

proof end;

theorem :: FUNCT_1:91

:: from PBOOLE

definition

let f be Function;

( f is empty-yielding iff for x being object st x in dom f holds

f . x is empty )

end;
redefine attr f is empty-yielding means :Def8: :: FUNCT_1:def 8

for x being object st x in dom f holds

f . x is empty ;

compatibility for x being object st x in dom f holds

f . x is empty ;

( f is empty-yielding iff for x being object st x in dom f holds

f . x is empty )

proof end;

:: deftheorem Def8 defines empty-yielding FUNCT_1:def 8 :

for f being Function holds

( f is empty-yielding iff for x being object st x in dom f holds

f . x is empty );

for f being Function holds

( f is empty-yielding iff for x being object st x in dom f holds

f . x is empty );

:: from UNIALG_1

definition

let F be Function;

( F is non-empty iff for n being object st n in dom F holds

not F . n is empty )

end;
redefine attr F is non-empty means :Def9: :: FUNCT_1:def 9

for n being object st n in dom F holds

not F . n is empty ;

compatibility for n being object st n in dom F holds

not F . n is empty ;

( F is non-empty iff for n being object st n in dom F holds

not F . n is empty )

proof end;

:: deftheorem Def9 defines non-empty FUNCT_1:def 9 :

for F being Function holds

( F is non-empty iff for n being object st n in dom F holds

not F . n is empty );

for F being Function holds

( F is non-empty iff for n being object st n in dom F holds

not F . n is empty );

:: new, 2004.08.04

:: from PUA2MSS1, 2005.08.22, A.T.

registration
end;

:: from SEQM_3, 2005.12.17, A.T.

:: deftheorem Def10 defines constant FUNCT_1:def 10 :

for f being Function holds

( f is constant iff for x, y being object st x in dom f & y in dom f holds

f . x = f . y );

for f being Function holds

( f is constant iff for x, y being object st x in dom f & y in dom f holds

f . x = f . y );

:: moved from MSAFREE3:1, AG 1.04.2006

:: added, AK 5.02.2007

definition

let f, g be Function;

( f = g iff ( dom f = dom g & ( for x being object st x in dom f holds

f . x = g . x ) ) ) by Th2;

end;
redefine pred f = g means :: FUNCT_1:def 11

( dom f = dom g & ( for x being object st x in dom f holds

f . x = g . x ) );

compatibility ( dom f = dom g & ( for x being object st x in dom f holds

f . x = g . x ) );

( f = g iff ( dom f = dom g & ( for x being object st x in dom f holds

f . x = g . x ) ) ) by Th2;

:: deftheorem defines = FUNCT_1:def 11 :

for f, g being Function holds

( f = g iff ( dom f = dom g & ( for x being object st x in dom f holds

f . x = g . x ) ) );

for f, g being Function holds

( f = g iff ( dom f = dom g & ( for x being object st x in dom f holds

f . x = g . x ) ) );

:: missing, 2007.03.09, A.T.

registration
end;

:: from PRVECT_1, 2007.03.09, A.T.

registration

let a be non empty non-empty Function;

let i be Element of dom a;

coherence

not a . i is empty

end;
let i be Element of dom a;

coherence

not a . i is empty

proof end;

:: missing, 2007.04.13, A.T.

registration
end;

:: from SCMFSA6A, 2007.07.23, A.T.

theorem :: FUNCT_1:95

for f, g being Function

for D being set st D c= dom f & D c= dom g holds

( f | D = g | D iff for x being set st x in D holds

f . x = g . x )

for D being set st D c= dom f & D c= dom g holds

( f | D = g | D iff for x being set st x in D holds

f . x = g . x )

proof end;

:: from SCMBSORT, 2007.07.26, A.T.

theorem :: FUNCT_1:96

for f, g being Function

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

f . x = g . x ) holds

f | X = g | X

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

f . x = g . x ) holds

f | X = g | X

proof end;

:: missing, 2007.10.28, A.T.

:: from RFUNCT_1, 2008.09.04, A.T.

:: from WAYBEL35, 2008.08.04, A.T.

registration
end;

registration
end;

:: from RFUNCT_2, 2008.09.14, A.T.

theorem :: FUNCT_1:101

for F, G being Function

for X being set holds

( X c= dom (G * F) iff ( X c= dom F & F .: X c= dom G ) )

for X being set holds

( X c= dom (G * F) iff ( X c= dom F & F .: X c= dom G ) )

proof end;

:: from YELLOW_6, 2008.12.26, A.T.

definition

let f be Function;

assume A1: ( not f is empty & f is constant ) ;

ex b_{1} being object ex x being set st

( x in dom f & b_{1} = f . x )

for b_{1}, b_{2} being object st ex x being set st

( x in dom f & b_{1} = f . x ) & ex x being set st

( x in dom f & b_{2} = f . x ) holds

b_{1} = b_{2}
by A1;

end;
assume A1: ( not f is empty & f is constant ) ;

func the_value_of f -> object means :: FUNCT_1:def 12

ex x being set st

( x in dom f & it = f . x );

existence ex x being set st

( x in dom f & it = f . x );

ex b

( x in dom f & b

proof end;

uniqueness for b

( x in dom f & b

( x in dom f & b

b

:: deftheorem defines the_value_of FUNCT_1:def 12 :

for f being Function st not f is empty & f is constant holds

for b_{2} being object holds

( b_{2} = the_value_of f iff ex x being set st

( x in dom f & b_{2} = f . x ) );

for f being Function st not f is empty & f is constant holds

for b

( b

( x in dom f & b

:: from QC_LANG4, 2009.01.23, A.T

registration

let X, Y be set ;

existence

ex b_{1} being Function st

( b_{1} is X -defined & b_{1} is Y -valued )

end;
existence

ex b

( b

proof end;

:: from FRAENKEL, 2009.05.06, A.K.

definition

let IT be set ;

end;
attr IT is functional means :Def13: :: FUNCT_1:def 13

for x being object st x in IT holds

x is Function;

for x being object st x in IT holds

x is Function;

:: deftheorem Def13 defines functional FUNCT_1:def 13 :

for IT being set holds

( IT is functional iff for x being object st x in IT holds

x is Function );

for IT being set holds

( IT is functional iff for x being object st x in IT holds

x is Function );

registration

coherence

for b_{1} being set st b_{1} is empty holds

b_{1} is functional
;

let f be Function;

coherence

{f} is functional by TARSKI:def 1;

let g be Function;

coherence

{f,g} is functional by TARSKI:def 2;

end;
for b

b

let f be Function;

coherence

{f} is functional by TARSKI:def 1;

let g be Function;

coherence

{f,g} is functional by TARSKI:def 2;

registration
end;

registration

let P be functional set ;

coherence

for b_{1} being Element of P holds

( b_{1} is Function-like & b_{1} is Relation-like )

end;
coherence

for b

( b

proof end;

registration
end;

:: new, 2009.09.30, A.T.

definition

let g, f be Function;

end;
attr f is g -compatible means :Def14: :: FUNCT_1:def 14

for x being object st x in dom f holds

f . x in g . x;

for x being object st x in dom f holds

f . x in g . x;

:: deftheorem Def14 defines -compatible FUNCT_1:def 14 :

for g, f being Function holds

( f is g -compatible iff for x being object st x in dom f holds

f . x in g . x );

for g, f being Function holds

( f is g -compatible iff for x being object st x in dom f holds

f . x in g . x );

theorem :: FUNCT_1:103

registration

let I be set ;

let f be Function;

existence

ex b_{1} being Function st

( b_{1} is empty & b_{1} is I -defined & b_{1} is f -compatible )

end;
let f be Function;

existence

ex b

( b

proof end;

registration

let X be set ;

let f be Function;

let g be f -compatible Function;

coherence

g | X is f -compatible

end;
let f be Function;

let g be f -compatible Function;

coherence

g | X is f -compatible

proof end;

registration

let I be set ;

existence

ex b_{1} being Function st

( b_{1} is non-empty & b_{1} is I -defined )

end;
existence

ex b

( b

proof end;

registration

let X be set ;

let f be X -defined Function;

coherence

for b_{1} being Function st b_{1} is f -compatible holds

b_{1} is X -defined

end;
let f be X -defined Function;

coherence

for b

b

proof end;

theorem :: FUNCT_1:106

for X being set

for x being object

for f being b_{1} -valued Function st x in dom f holds

f . x is Element of X

for x being object

for f being b

f . x is Element of X

proof end;

:: from JGRAPH_6, 2010.03.15, A.T.

registration

let A be functional set ;

let x be object ;

let F be A -valued Function;

coherence

( F . x is Function-like & F . x is Relation-like )

end;
let x be object ;

let F be A -valued Function;

coherence

( F . x is Function-like & F . x is Relation-like )

proof end;

:: missing, 2011.03.06, A.T.

theorem Th107: :: FUNCT_1:108

for X being set

for x being object

for f being Function st x in X & x in dom f holds

f . x in f .: X

for x being object

for f being Function st x in X & x in dom f holds

f . x in f .: X

proof end;

:: from HAHNBAN, 2011.04.26, A.T.

theorem :: FUNCT_1:110

for B being non empty functional set

for f being Function st f = union B holds

( dom f = union { (dom g) where g is Element of B : verum } & rng f = union { (rng g) where g is Element of B : verum } )

for f being Function st f = union B holds

( dom f = union { (dom g) where g is Element of B : verum } & rng f = union { (rng g) where g is Element of B : verum } )

proof end;

theorem Th110: :: FUNCT_1:111

for M being set st ( for X being set st X in M holds

X <> {} ) holds

ex f being Function st

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

f . X in X ) )

X <> {} ) holds

ex f being Function st

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

f . X in X ) )

proof end;

registration
end;

:: from PNPROC_1, 2012.02.20, A.T.

registration
end;

theorem :: FUNCT_1:114

for f, g being Function st rng f c= rng g holds

for x being object st x in dom f holds

ex y being object st

( y in dom g & f . x = g . y )

for x being object st x in dom f holds

ex y being object st

( y in dom g & f . x = g . y )

proof end;