:: GRFUNC_1 semantic presentation

theorem :: GRFUNC_1:1

canceled;

theorem :: GRFUNC_1:2

canceled;

theorem :: GRFUNC_1:3

canceled;

theorem :: GRFUNC_1:4

canceled;

theorem :: GRFUNC_1:5

canceled;

theorem Th6: :: GRFUNC_1:6

for f being Function
for G being set st G c= f holds
G is Function

proof end;

theorem :: GRFUNC_1:7

canceled;

theorem :: GRFUNC_1:8

for f, g being Function holds
( f c= g iff ( dom f c= dom g & ( for x being set st x in dom f holds
f . x = g . x ) ) )

proof end;

theorem :: GRFUNC_1:9

for f, g being Function st dom f = dom g & f c= g holds
f = g

proof end;

Lm1: for x, y being set
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:10

canceled;

theorem :: GRFUNC_1:11

canceled;

theorem :: GRFUNC_1:12

for x, z being set
for g, f being Function st [x,z] in g * f holds
( [x,(f . x)] in f & [(f . x),z] in g )

proof end;

theorem :: GRFUNC_1:13

for h, f, g being Function st h c= f holds
( g * h c= g * f & h * g c= f * g ) by RELAT_1:48, RELAT_1:49;

theorem :: GRFUNC_1:14

canceled;

theorem Th15: :: GRFUNC_1:15

for x, y being set holds {[x,y]} is Function

proof end;

Lm2: for x, y, x1, y1 being set st [x,y] in {[x1,y1]} holds
( x = x1 & y = y1 )

proof end;

theorem :: GRFUNC_1:16

for x, y being set
for f being Function st f = {[x,y]} holds
f . x = y

proof end;

theorem :: GRFUNC_1:17

canceled;

theorem Th18: :: GRFUNC_1:18

for x being set
for f being Function st dom f = {x} holds
f = {[x,(f . x)]}

proof end;

theorem :: GRFUNC_1:19

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

proof end;

theorem :: GRFUNC_1:20

canceled;

theorem :: GRFUNC_1:21

canceled;

theorem :: GRFUNC_1:22

canceled;

theorem :: GRFUNC_1:23

canceled;

theorem :: GRFUNC_1:24

canceled;

theorem Th25: :: GRFUNC_1:25

for f being Function holds
( f is one-to-one iff for x1, x2, y being set st [x1,y] in f & [x2,y] in f holds
x1 = x2 )

proof end;

theorem Th26: :: GRFUNC_1:26

for g, f being Function st g c= f & f is one-to-one holds
g is one-to-one

proof end;

theorem Th27: :: GRFUNC_1:27

for X being set
for f being Function holds f /\ X is Function

proof end;

theorem :: GRFUNC_1:28

for h, f, g being Function st h = f /\ g holds
( dom h c= (dom f) /\ (dom g) & rng h c= (rng f) /\ (rng g) ) by RELAT_1:14, RELAT_1:27;

theorem :: GRFUNC_1:29

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

proof end;

theorem :: GRFUNC_1:30

for f, g, h being Function st ( f is one-to-one or g is one-to-one ) & h = f /\ g holds
h is one-to-one

proof end;

theorem :: GRFUNC_1:31

for f, g being Function st dom f misses dom g holds
f \/ g is Function

proof end;

theorem :: GRFUNC_1:32

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

proof end;

Lm3: for x being set
for h, f, g 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:33

for h, f, g being Function st h = f \/ g holds
( dom h = (dom f) \/ (dom g) & rng h = (rng f) \/ (rng g) ) by RELAT_1:13, RELAT_1:26;

theorem Th34: :: GRFUNC_1:34

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

proof end;

theorem :: GRFUNC_1:35

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

proof end;

theorem :: GRFUNC_1:36

for x being set
for h, f, g 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:37

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

proof end;

theorem :: GRFUNC_1:38

for X being set
for f being Function holds f \ X is Function

proof end;

theorem :: GRFUNC_1:39

canceled;

theorem :: GRFUNC_1:40

canceled;

theorem :: GRFUNC_1:41

canceled;

theorem :: GRFUNC_1:42

canceled;

theorem :: GRFUNC_1:43

canceled;

theorem :: GRFUNC_1:44

canceled;

theorem :: GRFUNC_1:45

canceled;

theorem Th46: :: GRFUNC_1:46

for f being Function st f = {} holds
f is one-to-one

proof end;

theorem :: GRFUNC_1:47

for f being Function st f is one-to-one holds
for x, y being set holds
( [y,x] in f " iff [x,y] in f )

proof end;

theorem :: GRFUNC_1:48

canceled;

theorem :: GRFUNC_1:49

for f being Function st f = {} holds
f " = {}

proof end;

theorem :: GRFUNC_1:50

canceled;

theorem :: GRFUNC_1:51

canceled;

theorem :: GRFUNC_1:52

for x, X being set
for f being Function holds
( ( x in dom f & x in X ) iff [x,(f . x)] in f | X )

proof end;

theorem :: GRFUNC_1:53

canceled;

theorem :: GRFUNC_1:54

for X being set
for f, h, g being Function holds
( (f | X) * h c= f * h & g * (f | X) c= g * f ) by RELAT_1:92, RELAT_1:93;

theorem :: GRFUNC_1:55

canceled;

theorem :: GRFUNC_1:56

canceled;

theorem :: GRFUNC_1:57

canceled;

theorem :: GRFUNC_1:58

canceled;

theorem :: GRFUNC_1:59

canceled;

theorem :: GRFUNC_1:60

canceled;

theorem :: GRFUNC_1:61

canceled;

theorem :: GRFUNC_1:62

canceled;

theorem :: GRFUNC_1:63

canceled;

theorem Th64: :: GRFUNC_1:64

for g, f being Function st g c= f holds
f | (dom g) = g

proof end;

theorem :: GRFUNC_1:65

canceled;

theorem :: GRFUNC_1:66

canceled;

theorem :: GRFUNC_1:67

for x, Y being set
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:68

canceled;

theorem :: GRFUNC_1:69

for Y being set
for f, h, g being Function holds
( (Y | f) * h c= f * h & g * (Y | f) c= g * f ) by RELAT_1:121, RELAT_1:122;

theorem :: GRFUNC_1:70

canceled;

theorem :: GRFUNC_1:71

canceled;

theorem :: GRFUNC_1:72

canceled;

theorem :: GRFUNC_1:73

canceled;

theorem :: GRFUNC_1:74

canceled;

theorem :: GRFUNC_1:75

canceled;

theorem :: GRFUNC_1:76

canceled;

theorem :: GRFUNC_1:77

canceled;

theorem :: GRFUNC_1:78

canceled;

theorem :: GRFUNC_1:79

for g, f being Function st g c= f & f is one-to-one holds
(rng g) | f = g

proof end;

theorem :: GRFUNC_1:80

canceled;

theorem :: GRFUNC_1:81

canceled;

theorem :: GRFUNC_1:82

canceled;

theorem :: GRFUNC_1:83

canceled;

theorem :: GRFUNC_1:84

canceled;

theorem :: GRFUNC_1:85

canceled;

theorem :: GRFUNC_1:86

canceled;

theorem :: GRFUNC_1:87

for x, Y being set
for f being Function holds
( x in f " Y iff ( [x,(f . x)] in f & f . x in Y ) )

proof end;

theorem :: GRFUNC_1:88

for X being set
for f, g being Function st X c= dom f & f c= g holds
f | X = g | X

proof end;

theorem :: GRFUNC_1:89

for f being Function
for x being set st x in dom f holds
f | {x} = {[x,(f . x)]}

proof end;