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

::

:: Received April 14, 1989

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

theorem Th2: :: GRFUNC_1:2

for f, g being Function holds

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

f . x = g . x ) ) )

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

f . x = g . x ) ) )

proof end;

Lm1: for x, y being object

for f, h being Function st (rng f) /\ (rng h) = {} & x in dom f & y in dom h holds

f . x <> h . y

proof end;

theorem :: GRFUNC_1:4

for x, z being object

for f, g being Function st [x,z] in g * f holds

( [x,(f . x)] in f & [(f . x),z] in g )

for f, g being Function st [x,z] in g * f holds

( [x,(f . x)] in f & [(f . x),z] in g )

proof end;

Lm2: for x, x1, y, y1 being object st [x,y] in {[x1,y1]} holds

( x = x1 & y = y1 )

proof end;

theorem :: GRFUNC_1:8

for x1, x2, y1, y2 being object holds

( {[x1,y1],[x2,y2]} is Function iff ( x1 = x2 implies y1 = y2 ) )

( {[x1,y1],[x2,y2]} is Function iff ( x1 = x2 implies y1 = y2 ) )

proof end;

theorem Th9: :: GRFUNC_1:9

for f being Function holds

( f is one-to-one iff for x1, x2, y being object st [x1,y] in f & [x2,y] in f holds

x1 = x2 )

( f is one-to-one iff for x1, x2, y being object st [x1,y] in f & [x2,y] in f holds

x1 = x2 )

proof end;

registration
end;

theorem :: GRFUNC_1:12

theorem :: GRFUNC_1:14

Lm3: for x being object

for f, g, h being Function st h = f \/ g holds

( x in dom h iff ( x in dom f or x in dom g ) )

proof end;

theorem :: GRFUNC_1:16

for x being object

for f, g, h being Function st x in dom h & h = f \/ g & not h . x = f . x holds

h . x = g . x

for f, g, h being Function st x in dom h & h = f \/ g & not h . x = f . x holds

h . x = g . x

proof end;

theorem :: GRFUNC_1:17

for f, g, h being Function st f is one-to-one & g is one-to-one & h = f \/ g & rng f misses rng g holds

h is one-to-one

h is one-to-one

proof end;

::$CT 2

theorem :: GRFUNC_1:20

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

for x, y being object holds

( [y,x] in f " iff [x,y] in f )

for x, y being object holds

( [y,x] in f " iff [x,y] in f )

proof end;

theorem :: GRFUNC_1:22

for X being set

for x being object

for f being Function holds

( ( x in dom f & x in X ) iff [x,(f . x)] in f | X )

for x being object

for f being Function holds

( ( x in dom f & x in X ) iff [x,(f . x)] in f | X )

proof end;

theorem :: GRFUNC_1:24

for Y being set

for x being object

for f being Function holds

( ( x in dom f & f . x in Y ) iff [x,(f . x)] in Y |` f )

for x being object

for f being Function holds

( ( x in dom f & f . x in Y ) iff [x,(f . x)] in Y |` f )

proof end;

theorem :: GRFUNC_1:26

for Y being set

for x being object

for f being Function holds

( x in f " Y iff ( [x,(f . x)] in f & f . x in Y ) )

for x being object

for f being Function holds

( x in f " Y iff ( [x,(f . x)] in f & f . x in Y ) )

proof end;

:: from HAHNBAN

:: from AMI_3

:: from AMI_3, 2007.06.14, A.T.

theorem Th28: :: GRFUNC_1:30

for f, g being Function

for x, y being set st dom f = dom g & f . x = g . x & f . y = g . y holds

f | {x,y} = g | {x,y}

for x, y being set st dom f = dom g & f . x = g . x & f . y = g . y holds

f | {x,y} = g | {x,y}

proof end;

theorem :: GRFUNC_1:31

for f, g being Function

for x, y, z being set st dom f = dom g & f . x = g . x & f . y = g . y & f . z = g . z holds

f | {x,y,z} = g | {x,y,z}

for x, y, z being set st dom f = dom g & f . x = g . x & f . y = g . y & f . z = g . z holds

f | {x,y,z} = g | {x,y,z}

proof end;

:: from AMISTD_2, 2007.07.26, A.T.

:: missing, 2007.06.19, A.T.

:: new, 2009.09.30, A.T.

registration

let f be Function;

let g be Subset of f;

coherence

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

b_{1} is f -compatible

end;
let g be Subset of f;

coherence

for b

b

proof end;

:: 2009.10.17, A.T.

registration

let f be Function;

let g be f -compatible Function;

coherence

for b_{1} being Subset of g holds b_{1} is f -compatible

end;
let g be f -compatible Function;

coherence

for b

proof end;

theorem :: GRFUNC_1:35

for X being set

for x being object

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

f . x = g . x

for x being object

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

f . x = g . x

proof end;