:: FUNCT_1 semantic presentation

definition

let c₁ be set ;
attr a₁ is Function-like means :Def1: :: FUNCT_1:def 1
for b₁, b₂, b₃ being set st [b₁,b₂] in a₁ & [b₁,b₃] in a₁ holds
b₂ = b₃;

end;

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

registration

cluster Relation-like Function-like set ;
existence

proof end;

end;

definition

mode Function is Relation-like Function-like set ;

end;

registration

cluster empty -> Function-like set ;
coherence

proof end;

end;

theorem Th1: :: FUNCT_1:1

canceled;

theorem Th2: :: FUNCT_1:2

for b₁ being set st ( for b₂ being set st b₂ in b₁ holds
ex b₃, b₄ being set st [b₃,b₄] = b₂ ) & ( for b₂, b₃, b₄ being set st [b₂,b₃] in b₁ & [b₂,b₄] in b₁ holds
b₃ = b₄ ) holds
b₁ is Function by Def1, RELAT_1:def 1;

scheme :: FUNCT_1:sch 1
s1{ F₁() -> set , P₁[ set , set ] } :

ex b₁ being Function st
for b₂, b₃ being set holds
( [b₂,b₃] in b₁ iff ( b₂ in F₁() & P₁[b₂,b₃] ) )

provided

E2: for b₁, b₂, b₃ being set st P₁[b₁,b₂] & P₁[b₁,b₃] holds
b₂ = b₃

proof end;

definition

let c₁ be Function;
let c₂ be set ;
canceled;
canceled;
func c₁ . c₂ -> set means :Def4: :: FUNCT_1:def 4
[a₂,a₃] in a₁ if a₂ in dom a₁
otherwise a₃ = {} ;
existence by RELAT_1:def 4;
uniqueness by Def1;
consistency ;

end;

:: deftheorem Def2 FUNCT_1:def 2 :

:: deftheorem Def3 FUNCT_1:def 3 :

:: deftheorem Def4 defines . FUNCT_1:def 4 :

theorem Th3: :: FUNCT_1:3

canceled;

theorem Th4: :: FUNCT_1:4

canceled;

theorem Th5: :: FUNCT_1:5

canceled;

theorem Th6: :: FUNCT_1:6

canceled;

theorem Th7: :: FUNCT_1:7

canceled;

theorem Th8: :: FUNCT_1:8

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

proof end;

theorem Th9: :: FUNCT_1:9

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

proof end;

definition

let c₁ be Function;
redefine func rng c₁ -> set means :Def5: :: FUNCT_1:def 5
for b₁ being set holds
( b₁ in a₂ iff ex b₂ being set st
( b₂ in dom a₁ & b₁ = a₁ . b₂ ) );
compatibility

proof end;

end;

:: deftheorem Def5 defines rng FUNCT_1:def 5 :

theorem Th10: :: FUNCT_1:10

canceled;

theorem Th11: :: FUNCT_1:11

canceled;

theorem Th12: :: FUNCT_1:12

for b₁ being set
for b₂ being Function st b₁ in dom b₂ holds
b₂ . b₁ in rng b₂ by Def5;

theorem Th13: :: FUNCT_1:13

canceled;

theorem Th14: :: FUNCT_1:14

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

proof end;

scheme :: FUNCT_1:sch 2
s2{ F₁() -> set , P₁[ set , set ] } :

ex b₁ being Function st
( dom b₁ = F₁() & ( for b₂ being set st b₂ in F₁() holds
P₁[b₂,b₁ . b₂] ) )

provided

E7: for b₁, b₂, b₃ being set st b₁ in F₁() & P₁[b₁,b₂] & P₁[b₁,b₃] holds
b₂ = b₃ and
E8: for b₁ being set st b₁ in F₁() holds
ex b₂ being set st P₁[b₁,b₂]

proof end;

scheme :: FUNCT_1:sch 3
s3{ F₁() -> set , F₂( set ) -> set } :

ex b₁ being Function st
( dom b₁ = F₁() & ( for b₂ being set st b₂ in F₁() holds
b₁ . b₂ = F₂(b₂) ) )

proof end;

theorem Th15: :: FUNCT_1:15

for b₁ being set st b₁ <> {} holds
for b₂ being set ex b₃ being Function st
( dom b₃ = b₁ & rng b₃ = {b₂} )

proof end;

theorem Th16: :: FUNCT_1:16

for b₁ being set st ( for b₂, b₃ being Function st dom b₂ = b₁ & dom b₃ = b₁ holds
b₂ = b₃ ) holds
b₁ = {}

proof end;

theorem Th17: :: FUNCT_1:17

for b₁ being set
for b₂, b₃ being Function st dom b₂ = dom b₃ & rng b₂ = {b₁} & rng b₃ = {b₁} holds
b₂ = b₃

proof end;

theorem Th18: :: FUNCT_1:18

for b₁, b₂ being set st ( b₁ <> {} or b₂ = {} ) holds
ex b₃ being Function st
( b₂ = dom b₃ & rng b₃ c= b₁ )

proof end;

theorem Th19: :: FUNCT_1:19

for b₁ being set
for b₂ being Function st ( for b₃ being set st b₃ in b₁ holds
ex b₄ being set st
( b₄ in dom b₂ & b₃ = b₂ . b₄ ) ) holds
b₁ c= rng b₂

proof end;

notation

let c₁, c₂ be Function;
synonym c₂ * c₁ for c₁ * c₂;

end;

registration

let c₁, c₂ be Function;
cluster a₂ * a₁ -> Function-like ;
coherence

proof end;

end;

theorem Th20: :: FUNCT_1:20

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

proof end;

theorem Th21: :: FUNCT_1:21

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

proof end;

theorem Th22: :: FUNCT_1:22

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

proof end;

theorem Th23: :: FUNCT_1:23

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

proof end;

theorem Th24: :: FUNCT_1:24

canceled;

theorem Th25: :: FUNCT_1:25

for b₁ being set
for b₂, b₃ being Function st b₁ in rng (b₂ * b₃) holds
b₁ in rng b₂

proof end;

theorem Th26: :: FUNCT_1:26

canceled;

theorem Th27: :: FUNCT_1:27

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

proof end;

theorem Th28: :: FUNCT_1:28

canceled;

theorem Th29: :: FUNCT_1:29

canceled;

theorem Th30: :: FUNCT_1:30

canceled;

theorem Th31: :: FUNCT_1:31

canceled;

theorem Th32: :: FUNCT_1:32

canceled;

theorem Th33: :: FUNCT_1:33

for b₁ being set
for b₂ being Function st rng b₂ c= b₁ & ( for b₃, b₄ being Function st dom b₃ = b₁ & dom b₄ = b₁ & b₃ * b₂ = b₄ * b₂ holds
b₃ = b₄ ) holds
b₁ = rng b₂

proof end;

registration

let c₁ be set ;
cluster id a₁ -> Function-like ;
coherence

proof end;

end;

theorem Th34: :: FUNCT_1:34

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

proof end;

theorem Th35: :: FUNCT_1:35

for b₁, b₂ being set st b₂ in b₁ holds
(id b₁) . b₂ = b₂ by Th34;

theorem Th36: :: FUNCT_1:36

canceled;

theorem Th37: :: FUNCT_1:37

for b₁ being set
for b₂ being Function holds dom (b₂ * (id b₁)) = (dom b₂) /\ b₁

proof end;

theorem Th38: :: FUNCT_1:38

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

proof end;

theorem Th39: :: FUNCT_1:39

canceled;

theorem Th40: :: FUNCT_1:40

for b₁, b₂ being set
for b₃ being Function holds
( b₂ in dom ((id b₁) * b₃) iff ( b₂ in dom b₃ & b₃ . b₂ in b₁ ) )

proof end;

theorem Th41: :: FUNCT_1:41

canceled;

theorem Th42: :: FUNCT_1:42

for b₁ being Function holds
( b₁ * (id (dom b₁)) = b₁ & (id (rng b₁)) * b₁ = b₁ ) by RELAT_1:77, RELAT_1:79;

theorem Th43: :: FUNCT_1:43

for b₁, b₂ being set holds (id b₁) * (id b₂) = id (b₁ /\ b₂)

proof end;

theorem Th44: :: FUNCT_1:44

for b₁, b₂ being Function st rng b₁ = dom b₂ & b₂ * b₁ = b₁ holds
b₂ = id (dom b₂)

proof end;

definition

let c₁ be Function;
canceled;
canceled;
attr a₁ is one-to-one means :Def8: :: FUNCT_1:def 8
for b₁, b₂ being set st b₁ in dom a₁ & b₂ in dom a₁ & a₁ . b₁ = a₁ . b₂ holds
b₁ = b₂;

end;

:: deftheorem Def6 FUNCT_1:def 6 :

:: deftheorem Def7 FUNCT_1:def 7 :

:: deftheorem Def8 defines one-to-one FUNCT_1:def 8 :

theorem Th45: :: FUNCT_1:45

canceled;

theorem Th46: :: FUNCT_1:46

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

proof end;

theorem Th47: :: FUNCT_1:47

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

proof end;

theorem Th48: :: FUNCT_1:48

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

proof end;

theorem Th49: :: FUNCT_1:49

for b₁ being Function holds
( b₁ is one-to-one iff for b₂, b₃ being Function st rng b₂ c= dom b₁ & rng b₃ c= dom b₁ & dom b₂ = dom b₃ & b₁ * b₂ = b₁ * b₃ holds
b₂ = b₃ )

proof end;

theorem Th50: :: FUNCT_1:50

for b₁ being set
for b₂, b₃ being Function st dom b₂ = b₁ & dom b₃ = b₁ & rng b₃ c= b₁ & b₂ is one-to-one & b₂ * b₃ = b₂ holds
b₃ = id b₁

proof end;

theorem Th51: :: FUNCT_1:51

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

proof end;

theorem Th52: :: FUNCT_1:52

for b₁ being set holds id b₁ is one-to-one

proof end;

theorem Th53: :: FUNCT_1:53

for b₁ being Function st ex b₂ being Function st b₂ * b₁ = id (dom b₁) holds
b₁ is one-to-one

proof end;

registration

cluster empty set ;
existence

proof end;

end;

registration

cluster empty -> one-to-one set ;
coherence

proof end;

end;

registration

cluster one-to-one set ;
existence

proof end;

end;

registration

let c₁ be one-to-one Function;
cluster a₁ ~ -> Function-like ;
coherence

proof end;

end;

definition

let c₁ be Function;
assume E18: c₁ is one-to-one ;
func c₁ " -> Function equals :Def9: :: FUNCT_1:def 9
a₁ ~ ;
coherence

proof end;

end;

:: deftheorem Def9 defines " FUNCT_1:def 9 :

theorem Th54: :: FUNCT_1:54

for b₁ being Function st b₁ is one-to-one holds
for b₂ being Function holds
( b₂ = b₁ " iff ( dom b₂ = rng b₁ & ( for b₃, b₄ being set holds
( b₃ in rng b₁ & b₄ = b₂ . b₃ iff ( b₄ in dom b₁ & b₃ = b₁ . b₄ ) ) ) ) )

proof end;

theorem Th55: :: FUNCT_1:55

for b₁ being Function st b₁ is one-to-one holds
( rng b₁ = dom (b₁ " ) & dom b₁ = rng (b₁ " ) )

proof end;

theorem Th56: :: FUNCT_1:56

for b₁ being set
for b₂ being Function st b₂ is one-to-one & b₁ in dom b₂ holds
( b₁ = (b₂ " ) . (b₂ . b₁) & b₁ = ((b₂ " ) * b₂) . b₁ )

proof end;

theorem Th57: :: FUNCT_1:57

for b₁ being set
for b₂ being Function st b₂ is one-to-one & b₁ in rng b₂ holds
( b₁ = b₂ . ((b₂ " ) . b₁) & b₁ = (b₂ * (b₂ " )) . b₁ )

proof end;

theorem Th58: :: FUNCT_1:58

for b₁ being Function st b₁ is one-to-one holds
( dom ((b₁ " ) * b₁) = dom b₁ & rng ((b₁ " ) * b₁) = dom b₁ )

proof end;

theorem Th59: :: FUNCT_1:59

for b₁ being Function st b₁ is one-to-one holds
( dom (b₁ * (b₁ " )) = rng b₁ & rng (b₁ * (b₁ " )) = rng b₁ )

proof end;

theorem Th60: :: FUNCT_1:60

for b₁, b₂ being Function st b₁ is one-to-one & dom b₁ = rng b₂ & rng b₁ = dom b₂ & ( for b₃, b₄ being set st b₃ in dom b₁ & b₄ in dom b₂ holds
( b₁ . b₃ = b₄ iff b₂ . b₄ = b₃ ) ) holds
b₂ = b₁ "

proof end;

theorem Th61: :: FUNCT_1:61

for b₁ being Function st b₁ is one-to-one holds
( (b₁ " ) * b₁ = id (dom b₁) & b₁ * (b₁ " ) = id (rng b₁) )

proof end;

theorem Th62: :: FUNCT_1:62

for b₁ being Function st b₁ is one-to-one holds
b₁ " is one-to-one

proof end;

Lemma27: for b₁ being set
for b₂, b₃, b₄ being Function st rng b₂ = b₁ & b₃ * b₂ = id (dom b₄) & b₄ * b₃ = id b₁ holds
b₄ = b₂

proof end;

theorem Th63: :: FUNCT_1:63

for b₁, b₂ being Function st b₁ is one-to-one & rng b₁ = dom b₂ & b₂ * b₁ = id (dom b₁) holds
b₂ = b₁ "

proof end;

theorem Th64: :: FUNCT_1:64

for b₁, b₂ being Function st b₁ is one-to-one & rng b₂ = dom b₁ & b₁ * b₂ = id (rng b₁) holds
b₂ = b₁ "

proof end;

theorem Th65: :: FUNCT_1:65

for b₁ being Function st b₁ is one-to-one holds
(b₁ " ) " = b₁

proof end;

theorem Th66: :: FUNCT_1:66

for b₁, b₂ being Function st b₁ is one-to-one & b₂ is one-to-one holds
(b₂ * b₁) " = (b₁ " ) * (b₂ " )

proof end;

theorem Th67: :: FUNCT_1:67

for b₁ being set holds (id b₁) " = id b₁

proof end;

registration

let c₁ be Function;
let c₂ be set ;
cluster a₁ | a₂ -> Function-like ;
coherence

proof end;

end;

theorem Th68: :: FUNCT_1:68

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

proof end;

theorem Th69: :: FUNCT_1:69

canceled;

theorem Th70: :: FUNCT_1:70

for b₁, b₂ being set
for b₃ being Function st b₂ in dom (b₃ | b₁) holds
(b₃ | b₁) . b₂ = b₃ . b₂ by Th68;

theorem Th71: :: FUNCT_1:71

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

proof end;

Lemma30: for b₁, b₂ being set
for b₃ being Function holds
( b₂ in dom (b₃ | b₁) iff ( b₂ in dom b₃ & b₂ in b₁ ) )

proof end;

theorem Th72: :: FUNCT_1:72

for b₁, b₂ being set
for b₃ being Function st b₂ in b₁ holds
(b₃ | b₁) . b₂ = b₃ . b₂

proof end;

theorem Th73: :: FUNCT_1:73

for b₁, b₂ being set
for b₃ being Function st b₂ in dom b₃ & b₂ in b₁ holds
b₃ . b₂ in rng (b₃ | b₁)

proof end;

theorem Th74: :: FUNCT_1:74

canceled;

theorem Th75: :: FUNCT_1:75

canceled;

theorem Th76: :: FUNCT_1:76

for b₁ being set
for b₂ being Function holds
( dom (b₂ | b₁) c= dom b₂ & rng (b₂ | b₁) c= rng b₂ ) by RELAT_1:89, RELAT_1:99;

theorem Th77: :: FUNCT_1:77

canceled;

theorem Th78: :: FUNCT_1:78

canceled;

theorem Th79: :: FUNCT_1:79

canceled;

theorem Th80: :: FUNCT_1:80

canceled;

theorem Th81: :: FUNCT_1:81

canceled;

theorem Th82: :: FUNCT_1:82

for b₁, b₂ being set
for b₃ being Function st b₁ c= b₂ holds
( (b₃ | b₁) | b₂ = b₃ | b₁ & (b₃ | b₂) | b₁ = b₃ | b₁ ) by RELAT_1:102, RELAT_1:103;

theorem Th83: :: FUNCT_1:83

canceled;

theorem Th84: :: FUNCT_1:84

for b₁ being set
for b₂ being Function st b₂ is one-to-one holds
b₂ | b₁ is one-to-one

proof end;

registration

let c₁ be set ;
let c₂ be Function;
cluster a₁ | a₂ -> Function-like ;
coherence

proof end;

end;

theorem Th85: :: FUNCT_1:85

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

proof end;

theorem Th86: :: FUNCT_1:86

for b₁, b₂ being set
for b₃ being Function holds
( b₂ in dom (b₁ | b₃) iff ( b₂ in dom b₃ & b₃ . b₂ in b₁ ) ) by Th85;

theorem Th87: :: FUNCT_1:87

for b₁, b₂ being set
for b₃ being Function st b₂ in dom (b₁ | b₃) holds
(b₁ | b₃) . b₂ = b₃ . b₂ by Th85;

theorem Th88: :: FUNCT_1:88

canceled;

theorem Th89: :: FUNCT_1:89

for b₁ being set
for b₂ being Function holds
( dom (b₁ | b₂) c= dom b₂ & rng (b₁ | b₂) c= rng b₂ )

proof end;

theorem Th90: :: FUNCT_1:90

canceled;

theorem Th91: :: FUNCT_1:91

canceled;

theorem Th92: :: FUNCT_1:92

canceled;

theorem Th93: :: FUNCT_1:93

canceled;

theorem Th94: :: FUNCT_1:94

canceled;

theorem Th95: :: FUNCT_1:95

canceled;

theorem Th96: :: FUNCT_1:96

canceled;

theorem Th97: :: FUNCT_1:97

for b₁, b₂ being set
for b₃ being Function st b₁ c= b₂ holds
( b₂ | (b₁ | b₃) = b₁ | b₃ & b₁ | (b₂ | b₃) = b₁ | b₃ ) by RELAT_1:129, RELAT_1:130;

theorem Th98: :: FUNCT_1:98

canceled;

theorem Th99: :: FUNCT_1:99

for b₁ being set
for b₂ being Function st b₂ is one-to-one holds
b₁ | b₂ is one-to-one

proof end;

definition

let c₁ be Function;
let c₂ be set ;
canceled;
canceled;
redefine func c₁ .: c₂ -> set means :Def12: :: FUNCT_1:def 12
for b₁ being set holds
( b₁ in a₃ iff ex b₂ being set st
( b₂ in dom a₁ & b₂ in a₂ & b₁ = a₁ . b₂ ) );
compatibility

proof end;

end;

:: deftheorem Def10 FUNCT_1:def 10 :

:: deftheorem Def11 FUNCT_1:def 11 :

:: deftheorem Def12 defines .: FUNCT_1:def 12 :

theorem Th100: :: FUNCT_1:100

canceled;

theorem Th101: :: FUNCT_1:101

canceled;

theorem Th102: :: FUNCT_1:102

canceled;

theorem Th103: :: FUNCT_1:103

canceled;

theorem Th104: :: FUNCT_1:104

canceled;

theorem Th105: :: FUNCT_1:105

canceled;

theorem Th106: :: FUNCT_1:106

canceled;

theorem Th107: :: FUNCT_1:107

canceled;

theorem Th108: :: FUNCT_1:108

canceled;

theorem Th109: :: FUNCT_1:109

canceled;

theorem Th110: :: FUNCT_1:110

canceled;

theorem Th111: :: FUNCT_1:111

canceled;

theorem Th112: :: FUNCT_1:112

canceled;

theorem Th113: :: FUNCT_1:113

canceled;

theorem Th114: :: FUNCT_1:114

canceled;

theorem Th115: :: FUNCT_1:115

canceled;

theorem Th116: :: FUNCT_1:116

canceled;

theorem Th117: :: FUNCT_1:117

for b₁ being set
for b₂ being Function st b₁ in dom b₂ holds
b₂ .: {b₁} = {(b₂ . b₁)}

proof end;

theorem Th118: :: FUNCT_1:118

for b₁, b₂ being set
for b₃ being Function st b₁ in dom b₃ & b₂ in dom b₃ holds
b₃ .: {b₁,b₂} = {(b₃ . b₁),(b₃ . b₂)}

proof end;

theorem Th119: :: FUNCT_1:119

canceled;

theorem Th120: :: FUNCT_1:120

for b₁, b₂ being set
for b₃ being Function holds (b₁ | b₃) .: b₂ c= b₃ .: b₂

proof end;

theorem Th121: :: FUNCT_1:121

for b₁, b₂ being set
for b₃ being Function st b₃ is one-to-one holds
b₃ .: (b₁ /\ b₂) = (b₃ .: b₁) /\ (b₃ .: b₂)

proof end;

theorem Th122: :: FUNCT_1:122

for b₁ being Function st ( for b₂, b₃ being set holds b₁ .: (b₂ /\ b₃) = (b₁ .: b₂) /\ (b₁ .: b₃) ) holds
b₁ is one-to-one

proof end;

theorem Th123: :: FUNCT_1:123

for b₁, b₂ being set
for b₃ being Function st b₃ is one-to-one holds
b₃ .: (b₁ \ b₂) = (b₃ .: b₁) \ (b₃ .: b₂)

proof end;

theorem Th124: :: FUNCT_1:124

for b₁ being Function st ( for b₂, b₃ being set holds b₁ .: (b₂ \ b₃) = (b₁ .: b₂) \ (b₁ .: b₃) ) holds
b₁ is one-to-one

proof end;

theorem Th125: :: FUNCT_1:125

for b₁, b₂ being set
for b₃ being Function st b₁ misses b₂ & b₃ is one-to-one holds
b₃ .: b₁ misses b₃ .: b₂

proof end;

theorem Th126: :: FUNCT_1:126

for b₁, b₂ being set
for b₃ being Function holds (b₁ | b₃) .: b₂ = b₁ /\ (b₃ .: b₂)

proof end;

definition

let c₁ be Function;
let c₂ be set ;
redefine func c₁ " c₂ -> set means :Def13: :: FUNCT_1:def 13
for b₁ being set holds
( b₁ in a₃ iff ( b₁ in dom a₁ & a₁ . b₁ in a₂ ) );
compatibility

proof end;

end;

:: deftheorem Def13 defines " FUNCT_1:def 13 :

theorem Th127: :: FUNCT_1:127

canceled;

theorem Th128: :: FUNCT_1:128

canceled;

theorem Th129: :: FUNCT_1:129

canceled;

theorem Th130: :: FUNCT_1:130

canceled;

theorem Th131: :: FUNCT_1:131

canceled;

theorem Th132: :: FUNCT_1:132

canceled;

theorem Th133: :: FUNCT_1:133

canceled;

theorem Th134: :: FUNCT_1:134

canceled;

theorem Th135: :: FUNCT_1:135

canceled;

theorem Th136: :: FUNCT_1:136

canceled;

theorem Th137: :: FUNCT_1:137

for b₁, b₂ being set
for b₃ being Function holds b₃ " (b₁ /\ b₂) = (b₃ " b₁) /\ (b₃ " b₂)

proof end;

theorem Th138: :: FUNCT_1:138

for b₁, b₂ being set
for b₃ being Function holds b₃ " (b₁ \ b₂) = (b₃ " b₁) \ (b₃ " b₂)

proof end;

theorem Th139: :: FUNCT_1:139

for b₁, b₂ being set
for b₃ being Relation holds (b₃ | b₁) " b₂ = b₁ /\ (b₃ " b₂)

proof end;

theorem Th140: :: FUNCT_1:140

canceled;

theorem Th141: :: FUNCT_1:141

canceled;

theorem Th142: :: FUNCT_1:142

for b₁ being set
for b₂ being Relation holds
( b₁ in rng b₂ iff b₂ " {b₁} <> {} )

proof end;

theorem Th143: :: FUNCT_1:143

for b₁ being set
for b₂ being Relation st ( for b₃ being set st b₃ in b₁ holds
b₂ " {b₃} <> {} ) holds
b₁ c= rng b₂

proof end;

theorem Th144: :: FUNCT_1:144

for b₁ being Function holds
( ( for b₂ being set st b₂ in rng b₁ holds
ex b₃ being set st b₁ " {b₂} = {b₃} ) iff b₁ is one-to-one )

proof end;

theorem Th145: :: FUNCT_1:145

for b₁ being set
for b₂ being Function holds b₂ .: (b₂ " b₁) c= b₁

proof end;

theorem Th146: :: FUNCT_1:146

for b₁ being set
for b₂ being Relation st b₁ c= dom b₂ holds
b₁ c= b₂ " (b₂ .: b₁)

proof end;

theorem Th147: :: FUNCT_1:147

for b₁ being set
for b₂ being Function st b₁ c= rng b₂ holds
b₂ .: (b₂ " b₁) = b₁

proof end;

theorem Th148: :: FUNCT_1:148

for b₁ being set
for b₂ being Function holds b₂ .: (b₂ " b₁) = b₁ /\ (b₂ .: (dom b₂))

proof end;

theorem Th149: :: FUNCT_1:149

for b₁, b₂ being set
for b₃ being Function holds b₃ .: (b₁ /\ (b₃ " b₂)) c= (b₃ .: b₁) /\ b₂

proof end;

theorem Th150: :: FUNCT_1:150

for b₁, b₂ being set
for b₃ being Function holds b₃ .: (b₁ /\ (b₃ " b₂)) = (b₃ .: b₁) /\ b₂

proof end;

theorem Th151: :: FUNCT_1:151

for b₁, b₂ being set
for b₃ being Relation holds b₁ /\ (b₃ " b₂) c= b₃ " ((b₃ .: b₁) /\ b₂)

proof end;

theorem Th152: :: FUNCT_1:152

for b₁ being set
for b₂ being Function st b₂ is one-to-one holds
b₂ " (b₂ .: b₁) c= b₁

proof end;

theorem Th153: :: FUNCT_1:153

for b₁ being Function st ( for b₂ being set holds b₁ " (b₁ .: b₂) c= b₂ ) holds
b₁ is one-to-one

proof end;

theorem Th154: :: FUNCT_1:154

for b₁ being set
for b₂ being Function st b₂ is one-to-one holds
b₂ .: b₁ = (b₂ " ) " b₁

proof end;

theorem Th155: :: FUNCT_1:155

for b₁ being set
for b₂ being Function st b₂ is one-to-one holds
b₂ " b₁ = (b₂ " ) .: b₁

proof end;

theorem Th156: :: FUNCT_1:156

for b₁ being set
for b₂, b₃, b₄ being Function st b₁ = rng b₂ & dom b₃ = b₁ & dom b₄ = b₁ & b₃ * b₂ = b₄ * b₂ holds
b₃ = b₄

proof end;

theorem Th157: :: FUNCT_1:157

for b₁, b₂ being set
for b₃ being Function st b₃ .: b₁ c= b₃ .: b₂ & b₁ c= dom b₃ & b₃ is one-to-one holds
b₁ c= b₂

proof end;

theorem Th158: :: FUNCT_1:158

for b₁, b₂ being set
for b₃ being Function st b₃ " b₁ c= b₃ " b₂ & b₁ c= rng b₃ holds
b₁ c= b₂

proof end;

theorem Th159: :: FUNCT_1:159

for b₁ being Function holds
( b₁ is one-to-one iff for b₂ being set ex b₃ being set st b₁ " {b₂} c= {b₃} )

proof end;

theorem Th160: :: FUNCT_1:160

for b₁ being set
for b₂, b₃ being Relation st rng b₂ c= dom b₃ holds
b₂ " b₁ c= (b₂ * b₃) " (b₃ .: b₁)

proof end;

theorem Th161: :: FUNCT_1:161

for b₁, b₂ being set
for b₃ being Function st b₃ " b₁ = b₃ " b₂ & b₁ c= rng b₃ & b₂ c= rng b₃ holds
b₁ = b₂

proof end;

theorem Th162: :: FUNCT_1:162

for b₁ being set
for b₂ being Subset of b₁ holds (id b₁) .: b₂ = b₂

proof end;

definition

let c₁ be Function;
redefine attr a₁ is empty-yielding means :: FUNCT_1:def 14
for b₁ being set st b₁ in dom a₁ holds
a₁ . b₁ is empty;
compatibility

proof end;

end;

:: deftheorem Def14 defines empty-yielding FUNCT_1:def 14 :

registration

cluster empty-yielding set ;
existence by RELAT_1:60;

end;

definition

let c₁ be Function;
redefine attr a₁ is non-empty means :Def15: :: FUNCT_1:def 15
for b₁ being set st b₁ in dom a₁ holds
not a₁ . b₁ is empty;
compatibility

proof end;

end;

:: deftheorem Def15 defines non-empty FUNCT_1:def 15 :

registration

cluster non-empty set ;
existence

proof end;

end;

scheme :: FUNCT_1:sch 4
s4{ F₁() -> non empty set , F₂( set ) -> set } :

ex b₁ being Function st
( dom b₁ = F₁() & ( for b₂ being Element of F₁() holds b₁ . b₂ = F₂(b₂) ) )

proof end;

registration

let c₁ be non-empty Function;
cluster rng a₁ -> with_non-empty_elements ;
coherence

proof end;

end;