:: GRFUNC_1 semantic presentation

theorem Th1: :: GRFUNC_1:1

canceled;

theorem Th2: :: GRFUNC_1:2

canceled;

theorem Th3: :: GRFUNC_1:3

canceled;

theorem Th4: :: GRFUNC_1:4

canceled;

theorem Th5: :: GRFUNC_1:5

canceled;

theorem Th6: :: GRFUNC_1:6

for b₁ being Function
for b₂ being set st b₂ c= b₁ holds
b₂ is Function

proof end;

theorem Th7: :: GRFUNC_1:7

canceled;

theorem Th8: :: GRFUNC_1:8

for b₁, b₂ being Function holds
( b₁ c= b₂ iff ( dom b₁ c= dom b₂ & ( for b₃ being set st b₃ in dom b₁ holds
b₁ . b₃ = b₂ . b₃ ) ) )

proof end;

theorem Th9: :: GRFUNC_1:9

for b₁, b₂ being Function st dom b₁ = dom b₂ & b₁ c= b₂ holds
b₁ = b₂

proof end;

Lemma2: for b₁, b₂ being set
for b₃, b₄ being Function st (rng b₃) /\ (rng b₄) = {} & b₁ in dom b₃ & b₂ in dom b₄ holds
b₃ . b₁ <> b₄ . b₂

proof end;

theorem Th10: :: GRFUNC_1:10

canceled;

theorem Th11: :: GRFUNC_1:11

canceled;

theorem Th12: :: GRFUNC_1:12

for b₁, b₂ being set
for b₃, b₄ being Function st [b₁,b₂] in b₃ * b₄ holds
( [b₁,(b₄ . b₁)] in b₄ & [(b₄ . b₁),b₂] in b₃ )

proof end;

theorem Th13: :: GRFUNC_1:13

for b₁, b₂, b₃ being Function st b₁ c= b₂ holds
( b₃ * b₁ c= b₃ * b₂ & b₁ * b₃ c= b₂ * b₃ ) by RELAT_1:48, RELAT_1:49;

theorem Th14: :: GRFUNC_1:14

canceled;

theorem Th15: :: GRFUNC_1:15

for b₁, b₂ being set holds {[b₁,b₂]} is Function

proof end;

Lemma4: for b₁, b₂, b₃, b₄ being set st [b₁,b₂] in {[b₃,b₄]} holds
( b₁ = b₃ & b₂ = b₄ )

proof end;

theorem Th16: :: GRFUNC_1:16

for b₁, b₂ being set
for b₃ being Function st b₃ = {[b₁,b₂]} holds
b₃ . b₁ = b₂

proof end;

theorem Th17: :: GRFUNC_1:17

canceled;

theorem Th18: :: GRFUNC_1:18

for b₁ being set
for b₂ being Function st dom b₂ = {b₁} holds
b₂ = {[b₁,(b₂ . b₁)]}

proof end;

theorem Th19: :: GRFUNC_1:19

for b₁, b₂, b₃, b₄ being set holds
( {[b₁,b₂],[b₃,b₄]} is Function iff ( b₁ = b₃ implies b₂ = b₄ ) )

proof end;

theorem Th20: :: GRFUNC_1:20

canceled;

theorem Th21: :: GRFUNC_1:21

canceled;

theorem Th22: :: GRFUNC_1:22

canceled;

theorem Th23: :: GRFUNC_1:23

canceled;

theorem Th24: :: GRFUNC_1:24

canceled;

theorem Th25: :: GRFUNC_1:25

for b₁ being Function holds
( b₁ is one-to-one iff for b₂, b₃, b₄ being set st [b₂,b₄] in b₁ & [b₃,b₄] in b₁ holds
b₂ = b₃ )

proof end;

theorem Th26: :: GRFUNC_1:26

for b₁, b₂ being Function st b₁ c= b₂ & b₂ is one-to-one holds
b₁ is one-to-one

proof end;

theorem Th27: :: GRFUNC_1:27

for b₁ being set
for b₂ being Function holds b₂ /\ b₁ is Function

proof end;

theorem Th28: :: GRFUNC_1:28

for b₁, b₂, b₃ being Function st b₁ = b₂ /\ b₃ holds
( dom b₁ c= (dom b₂) /\ (dom b₃) & rng b₁ c= (rng b₂) /\ (rng b₃) ) by RELAT_1:14, RELAT_1:27;

theorem Th29: :: GRFUNC_1:29

for b₁ being set
for b₂, b₃, b₄ being Function st b₂ = b₃ /\ b₄ & b₁ in dom b₂ holds
( b₂ . b₁ = b₃ . b₁ & b₂ . b₁ = b₄ . b₁ )

proof end;

theorem Th30: :: GRFUNC_1:30

for b₁, b₂, b₃ being Function st ( b₁ is one-to-one or b₂ is one-to-one ) & b₃ = b₁ /\ b₂ holds
b₃ is one-to-one

proof end;

theorem Th31: :: GRFUNC_1:31

for b₁, b₂ being Function st dom b₁ misses dom b₂ holds
b₁ \/ b₂ is Function

proof end;

theorem Th32: :: GRFUNC_1:32

for b₁, b₂, b₃ being Function st b₁ c= b₂ & b₃ c= b₂ holds
b₁ \/ b₃ is Function

proof end;

Lemma9: for b₁ being set
for b₂, b₃, b₄ being Function st b₂ = b₃ \/ b₄ holds
( b₁ in dom b₂ iff ( b₁ in dom b₃ or b₁ in dom b₄ ) )

proof end;

theorem Th33: :: GRFUNC_1:33

for b₁, b₂, b₃ being Function st b₁ = b₂ \/ b₃ holds
( dom b₁ = (dom b₂) \/ (dom b₃) & rng b₁ = (rng b₂) \/ (rng b₃) ) by RELAT_1:13, RELAT_1:26;

theorem Th34: :: GRFUNC_1:34

for b₁ being set
for b₂, b₃, b₄ being Function st b₁ in dom b₂ & b₃ = b₂ \/ b₄ holds
b₃ . b₁ = b₂ . b₁

proof end;

theorem Th35: :: GRFUNC_1:35

for b₁ being set
for b₂, b₃, b₄ being Function st b₁ in dom b₂ & b₃ = b₄ \/ b₂ holds
b₃ . b₁ = b₂ . b₁

proof end;

theorem Th36: :: GRFUNC_1:36

for b₁ being set
for b₂, b₃, b₄ being Function st b₁ in dom b₂ & b₂ = b₃ \/ b₄ & not b₂ . b₁ = b₃ . b₁ holds
b₂ . b₁ = b₄ . b₁

proof end;

theorem Th37: :: GRFUNC_1:37

for b₁, b₂, b₃ being Function st b₁ is one-to-one & b₂ is one-to-one & b₃ = b₁ \/ b₂ & rng b₁ misses rng b₂ holds
b₃ is one-to-one

proof end;

theorem Th38: :: GRFUNC_1:38

for b₁ being set
for b₂ being Function holds b₂ \ b₁ is Function

proof end;

theorem Th39: :: GRFUNC_1:39

canceled;

theorem Th40: :: GRFUNC_1:40

canceled;

theorem Th41: :: GRFUNC_1:41

canceled;

theorem Th42: :: GRFUNC_1:42

canceled;

theorem Th43: :: GRFUNC_1:43

canceled;

theorem Th44: :: GRFUNC_1:44

canceled;

theorem Th45: :: GRFUNC_1:45

canceled;

theorem Th46: :: GRFUNC_1:46

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

proof end;

theorem Th47: :: GRFUNC_1:47

for b₁ being Function st b₁ is one-to-one holds
for b₂, b₃ being set holds
( [b₃,b₂] in b₁ " iff [b₂,b₃] in b₁ )

proof end;

theorem Th48: :: GRFUNC_1:48

canceled;

theorem Th49: :: GRFUNC_1:49

for b₁ being Function st b₁ = {} holds
b₁ " = {}

proof end;

theorem Th50: :: GRFUNC_1:50

canceled;

theorem Th51: :: GRFUNC_1:51

canceled;

theorem Th52: :: GRFUNC_1:52

for b₁, b₂ being set
for b₃ being Function holds
( ( b₁ in dom b₃ & b₁ in b₂ ) iff [b₁,(b₃ . b₁)] in b₃ | b₂ )

proof end;

theorem Th53: :: GRFUNC_1:53

canceled;

theorem Th54: :: GRFUNC_1:54

for b₁ being set
for b₂, b₃, b₄ being Function holds
( (b₂ | b₁) * b₃ c= b₂ * b₃ & b₄ * (b₂ | b₁) c= b₄ * b₂ ) by RELAT_1:92, RELAT_1:93;

theorem Th55: :: GRFUNC_1:55

canceled;

theorem Th56: :: GRFUNC_1:56

canceled;

theorem Th57: :: GRFUNC_1:57

canceled;

theorem Th58: :: GRFUNC_1:58

canceled;

theorem Th59: :: GRFUNC_1:59

canceled;

theorem Th60: :: GRFUNC_1:60

canceled;

theorem Th61: :: GRFUNC_1:61

canceled;

theorem Th62: :: GRFUNC_1:62

canceled;

theorem Th63: :: GRFUNC_1:63

canceled;

theorem Th64: :: GRFUNC_1:64

for b₁, b₂ being Function st b₁ c= b₂ holds
b₂ | (dom b₁) = b₁

proof end;

theorem Th65: :: GRFUNC_1:65

canceled;

theorem Th66: :: GRFUNC_1:66

canceled;

theorem Th67: :: GRFUNC_1:67

for b₁, b₂ being set
for b₃ being Function holds
( ( b₁ in dom b₃ & b₃ . b₁ in b₂ ) iff [b₁,(b₃ . b₁)] in b₂ | b₃ )

proof end;

theorem Th68: :: GRFUNC_1:68

canceled;

theorem Th69: :: GRFUNC_1:69

for b₁ being set
for b₂, b₃, b₄ being Function holds
( (b₁ | b₂) * b₃ c= b₂ * b₃ & b₄ * (b₁ | b₂) c= b₄ * b₂ ) by RELAT_1:121, RELAT_1:122;

theorem Th70: :: GRFUNC_1:70

canceled;

theorem Th71: :: GRFUNC_1:71

canceled;

theorem Th72: :: GRFUNC_1:72

canceled;

theorem Th73: :: GRFUNC_1:73

canceled;

theorem Th74: :: GRFUNC_1:74

canceled;

theorem Th75: :: GRFUNC_1:75

canceled;

theorem Th76: :: GRFUNC_1:76

canceled;

theorem Th77: :: GRFUNC_1:77

canceled;

theorem Th78: :: GRFUNC_1:78

canceled;

theorem Th79: :: GRFUNC_1:79

for b₁, b₂ being Function st b₁ c= b₂ & b₂ is one-to-one holds
(rng b₁) | b₂ = b₁

proof end;

theorem Th80: :: GRFUNC_1:80

canceled;

theorem Th81: :: GRFUNC_1:81

canceled;

theorem Th82: :: GRFUNC_1:82

canceled;

theorem Th83: :: GRFUNC_1:83

canceled;

theorem Th84: :: GRFUNC_1:84

canceled;

theorem Th85: :: GRFUNC_1:85

canceled;

theorem Th86: :: GRFUNC_1:86

canceled;

theorem Th87: :: GRFUNC_1:87

for b₁, b₂ being set
for b₃ being Function holds
( b₁ in b₃ " b₂ iff ( [b₁,(b₃ . b₁)] in b₃ & b₃ . b₁ in b₂ ) )

proof end;

theorem Th88: :: GRFUNC_1:88

for b₁ being set
for b₂, b₃ being Function st b₁ c= dom b₂ & b₂ c= b₃ holds
b₂ | b₁ = b₃ | b₁

proof end;

theorem Th89: :: GRFUNC_1:89

for b₁ being Function
for b₂ being set st b₂ in dom b₁ holds
b₁ | {b₂} = {[b₂,(b₁ . b₂)]}

proof end;