:: FUNCT_4 semantic presentation

Lemma1: for b₁, b₂, b₃ being set st [b₁,b₂] in b₃ holds
( b₁ in union (union b₃) & b₂ in union (union b₃) )

proof end;

Lemma2: for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈ being set st [[b₁,b₂],[b₃,b₄]] = [[b₅,b₆],[b₇,b₈]] holds
( b₁ = b₅ & b₃ = b₇ & b₂ = b₆ & b₄ = b₈ )

proof end;

theorem Th1: :: FUNCT_4:1

for b₁ being set st ( for b₂ being set st b₂ in b₁ holds
ex b₃, b₄ being set st b₂ = [b₃,b₄] ) holds
ex b₂, b₃ being set st b₁ c= [:b₂,b₃:]

proof end;

theorem Th2: :: FUNCT_4:2

for b₁, b₂ being Function holds b₁ * b₂ = (b₁ | (rng b₂)) * b₂

proof end;

theorem Th3: :: FUNCT_4:3

canceled;

theorem Th4: :: FUNCT_4:4

for b₁, b₂ being set holds
( id b₁ c= id b₂ iff b₁ c= b₂ )

proof end;

theorem Th5: :: FUNCT_4:5

for b₁, b₂, b₃ being set st b₁ c= b₂ holds
b₁ --> b₃ c= b₂ --> b₃

proof end;

theorem Th6: :: FUNCT_4:6

for b₁, b₂, b₃, b₄ being set st b₁ --> b₂ c= b₃ --> b₄ holds
b₁ c= b₃

proof end;

theorem Th7: :: FUNCT_4:7

for b₁, b₂, b₃, b₄ being set st b₁ <> {} & b₁ --> b₂ c= b₃ --> b₄ holds
b₂ = b₄

proof end;

theorem Th8: :: FUNCT_4:8

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

proof end;

notation

let c₁, c₂ be Function;
synonym c₁ <= c₂ for c₁ c= c₂;

end;

theorem Th9: :: FUNCT_4:9

for b₁, b₂ being set
for b₃ being Function holds (b₁ | b₃) | b₂ <= b₃

proof end;

theorem Th10: :: FUNCT_4:10

for b₁, b₂ being set
for b₃, b₄ being Function st b₃ <= b₄ holds
(b₁ | b₃) | b₂ <= (b₁ | b₄) | b₂

proof end;

definition

let c₁, c₂ be Function;
func c₁ +* c₂ -> Function means :Def1: :: FUNCT_4:def 1
( dom a₃ = (dom a₁) \/ (dom a₂) & ( for b₁ being set st b₁ in (dom a₁) \/ (dom a₂) holds
( ( b₁ in dom a₂ implies a₃ . b₁ = a₂ . b₁ ) & ( not b₁ in dom a₂ implies a₃ . b₁ = a₁ . b₁ ) ) ) );
existence

proof end;

uniqueness

proof end;

idempotence ;

end;

:: deftheorem Def1 defines +* FUNCT_4:def 1 :

theorem Th11: :: FUNCT_4:11

for b₁, b₂ being Function holds
( dom b₁ c= dom (b₁ +* b₂) & dom b₂ c= dom (b₁ +* b₂) )

proof end;

theorem Th12: :: FUNCT_4:12

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

proof end;

theorem Th13: :: FUNCT_4:13

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

proof end;

theorem Th14: :: FUNCT_4:14

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

proof end;

theorem Th15: :: FUNCT_4:15

for b₁, b₂, b₃ being Function holds (b₁ +* b₂) +* b₃ = b₁ +* (b₂ +* b₃)

proof end;

theorem Th16: :: FUNCT_4:16

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

proof end;

theorem Th17: :: FUNCT_4:17

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

proof end;

theorem Th18: :: FUNCT_4:18

for b₁, b₂ being Function holds rng (b₁ +* b₂) c= (rng b₁) \/ (rng b₂)

proof end;

theorem Th19: :: FUNCT_4:19

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

proof end;

theorem Th20: :: FUNCT_4:20

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

proof end;

theorem Th21: :: FUNCT_4:21

for b₁ being Function holds {} +* b₁ = b₁

proof end;

theorem Th22: :: FUNCT_4:22

for b₁ being Function holds b₁ +* {} = b₁

proof end;

theorem Th23: :: FUNCT_4:23

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

proof end;

theorem Th24: :: FUNCT_4:24

for b₁, b₂ being Function holds (b₁ +* b₂) | (dom b₂) = b₂

proof end;

theorem Th25: :: FUNCT_4:25

for b₁, b₂ being Function holds (b₁ +* b₂) | ((dom b₁) \ (dom b₂)) c= b₁

proof end;

theorem Th26: :: FUNCT_4:26

for b₁, b₂ being Function holds b₁ c= b₂ +* b₁

proof end;

theorem Th27: :: FUNCT_4:27

for b₁, b₂, b₃ being Function st b₁ tolerates b₂ +* b₃ holds
b₁ | ((dom b₁) \ (dom b₃)) tolerates b₂

proof end;

theorem Th28: :: FUNCT_4:28

for b₁, b₂, b₃ being Function st b₁ tolerates b₂ +* b₃ holds
b₁ tolerates b₃

proof end;

theorem Th29: :: FUNCT_4:29

for b₁, b₂ being Function holds
( b₁ tolerates b₂ iff b₁ c= b₁ +* b₂ )

proof end;

theorem Th30: :: FUNCT_4:30

for b₁, b₂ being Function holds b₁ +* b₂ c= b₁ \/ b₂

proof end;

theorem Th31: :: FUNCT_4:31

for b₁, b₂ being Function holds
( b₁ tolerates b₂ iff b₁ \/ b₂ = b₁ +* b₂ )

proof end;

theorem Th32: :: FUNCT_4:32

for b₁, b₂ being Function st dom b₁ misses dom b₂ holds
b₁ \/ b₂ = b₁ +* b₂

proof end;

theorem Th33: :: FUNCT_4:33

for b₁, b₂ being Function st dom b₁ misses dom b₂ holds
b₁ c= b₁ +* b₂

proof end;

theorem Th34: :: FUNCT_4:34

for b₁, b₂ being Function st dom b₁ misses dom b₂ holds
(b₁ +* b₂) | (dom b₁) = b₁

proof end;

theorem Th35: :: FUNCT_4:35

for b₁, b₂ being Function holds
( b₁ tolerates b₂ iff b₁ +* b₂ = b₂ +* b₁ )

proof end;

theorem Th36: :: FUNCT_4:36

for b₁, b₂ being Function st dom b₁ misses dom b₂ holds
b₁ +* b₂ = b₂ +* b₁

proof end;

theorem Th37: :: FUNCT_4:37

for b₁, b₂ being set
for b₃, b₄ being PartFunc of b₁,b₂ st b₄ is total holds
b₃ +* b₄ = b₄

proof end;

theorem Th38: :: FUNCT_4:38

for b₁, b₂ being set
for b₃, b₄ being Function of b₁,b₂ st ( b₂ = {} implies b₁ = {} ) holds
b₃ +* b₄ = b₄

proof end;

theorem Th39: :: FUNCT_4:39

for b₁ being set
for b₂, b₃ being Function of b₁,b₁ holds b₂ +* b₃ = b₃

proof end;

theorem Th40: :: FUNCT_4:40

for b₁ being set
for b₂ being non empty set
for b₃, b₄ being Function of b₁,b₂ holds b₃ +* b₄ = b₄ by Th38;

theorem Th41: :: FUNCT_4:41

for b₁, b₂ being set
for b₃, b₄ being PartFunc of b₁,b₂ holds b₃ +* b₄ is PartFunc of b₁,b₂

proof end;

definition

let c₁ be Function;
func ~ c₁ -> Function means :Def2: :: FUNCT_4:def 2
( ( for b₁ being set holds
( b₁ in dom a₂ iff ex b₂, b₃ being set st
( b₁ = [b₃,b₂] & [b₂,b₃] in dom a₁ ) ) ) & ( for b₁, b₂ being set st [b₁,b₂] in dom a₁ holds
a₂ . [b₂,b₁] = a₁ . [b₁,b₂] ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines ~ FUNCT_4:def 2 :

theorem Th42: :: FUNCT_4:42

for b₁ being Function holds rng (~ b₁) c= rng b₁

proof end;

theorem Th43: :: FUNCT_4:43

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

proof end;

theorem Th44: :: FUNCT_4:44

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

proof end;

theorem Th45: :: FUNCT_4:45

for b₁ being Function ex b₂, b₃ being set st dom (~ b₁) c= [:b₂,b₃:]

proof end;

theorem Th46: :: FUNCT_4:46

for b₁, b₂ being set
for b₃ being Function st dom b₃ c= [:b₁,b₂:] holds
dom (~ b₃) c= [:b₂,b₁:]

proof end;

theorem Th47: :: FUNCT_4:47

for b₁, b₂ being set
for b₃ being Function st dom b₃ = [:b₁,b₂:] holds
dom (~ b₃) = [:b₂,b₁:]

proof end;

theorem Th48: :: FUNCT_4:48

for b₁, b₂ being set
for b₃ being Function st dom b₃ c= [:b₁,b₂:] holds
rng (~ b₃) = rng b₃

proof end;

theorem Th49: :: FUNCT_4:49

for b₁, b₂, b₃ being set
for b₄ being PartFunc of [:b₁,b₂:],b₃ holds ~ b₄ is PartFunc of [:b₂,b₁:],b₃

proof end;

theorem Th50: :: FUNCT_4:50

for b₁, b₂, b₃ being set
for b₄ being Function of [:b₁,b₂:],b₃ st b₃ <> {} holds
~ b₄ is Function of [:b₂,b₁:],b₃

proof end;

theorem Th51: :: FUNCT_4:51

for b₁, b₂ being set
for b₃ being non empty set
for b₄ being Function of [:b₁,b₂:],b₃ holds ~ b₄ is Function of [:b₂,b₁:],b₃ by Th50;

theorem Th52: :: FUNCT_4:52

for b₁ being Function holds ~ (~ b₁) c= b₁

proof end;

theorem Th53: :: FUNCT_4:53

for b₁, b₂ being set
for b₃ being Function st dom b₃ c= [:b₁,b₂:] holds
~ (~ b₃) = b₃

proof end;

theorem Th54: :: FUNCT_4:54

for b₁, b₂, b₃ being set
for b₄ being PartFunc of [:b₁,b₂:],b₃ holds ~ (~ b₄) = b₄

proof end;

theorem Th55: :: FUNCT_4:55

for b₁, b₂, b₃ being set
for b₄ being Function of [:b₁,b₂:],b₃ st b₃ <> {} holds
~ (~ b₄) = b₄

proof end;

theorem Th56: :: FUNCT_4:56

for b₁, b₂ being set
for b₃ being non empty set
for b₄ being Function of [:b₁,b₂:],b₃ holds ~ (~ b₄) = b₄ by Th55;

definition

let c₁, c₂ be Function;
func |:c₁,c₂:| -> Function means :Def3: :: FUNCT_4:def 3
( ( for b₁ being set holds
( b₁ in dom a₃ iff ex b₂, b₃, b₄, b₅ being set st
( b₁ = [[b₂,b₄],[b₃,b₅]] & [b₂,b₃] in dom a₁ & [b₄,b₅] in dom a₂ ) ) ) & ( for b₁, b₂, b₃, b₄ being set st [b₁,b₂] in dom a₁ & [b₃,b₄] in dom a₂ holds
a₃ . [[b₁,b₃],[b₂,b₄]] = [(a₁ . [b₁,b₂]),(a₂ . [b₃,b₄])] ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines |: FUNCT_4:def 3 :

theorem Th57: :: FUNCT_4:57

for b₁, b₂, b₃, b₄ being set
for b₅, b₆ being Function holds
( [[b₁,b₂],[b₃,b₄]] in dom |:b₅,b₆:| iff ( [b₁,b₃] in dom b₅ & [b₂,b₄] in dom b₆ ) )

proof end;

theorem Th58: :: FUNCT_4:58

for b₁, b₂, b₃, b₄ being set
for b₅, b₆ being Function st [[b₁,b₂],[b₃,b₄]] in dom |:b₅,b₆:| holds
|:b₅,b₆:| . [[b₁,b₂],[b₃,b₄]] = [(b₅ . [b₁,b₃]),(b₆ . [b₂,b₄])]

proof end;

theorem Th59: :: FUNCT_4:59

for b₁, b₂ being Function holds rng |:b₁,b₂:| c= [:(rng b₁),(rng b₂):]

proof end;

theorem Th60: :: FUNCT_4:60

for b₁, b₂, b₃, b₄ being set
for b₅, b₆ being Function st dom b₅ c= [:b₁,b₂:] & dom b₆ c= [:b₃,b₄:] holds
dom |:b₅,b₆:| c= [:[:b₁,b₃:],[:b₂,b₄:]:]

proof end;

theorem Th61: :: FUNCT_4:61

for b₁, b₂, b₃, b₄ being set
for b₅, b₆ being Function st dom b₅ = [:b₁,b₂:] & dom b₆ = [:b₃,b₄:] holds
dom |:b₅,b₆:| = [:[:b₁,b₃:],[:b₂,b₄:]:]

proof end;

theorem Th62: :: FUNCT_4:62

for b₁, b₂, b₃, b₄, b₅, b₆ being set
for b₇ being PartFunc of [:b₁,b₂:],b₃
for b₈ being PartFunc of [:b₄,b₅:],b₆ holds |:b₇,b₈:| is PartFunc of [:[:b₁,b₄:],[:b₂,b₅:]:],[:b₃,b₆:]

proof end;

theorem Th63: :: FUNCT_4:63

for b₁, b₂, b₃, b₄, b₅, b₆ being set
for b₇ being Function of [:b₁,b₂:],b₃
for b₈ being Function of [:b₄,b₅:],b₆ st b₃ <> {} & b₆ <> {} holds
|:b₇,b₈:| is Function of [:[:b₁,b₄:],[:b₂,b₅:]:],[:b₃,b₆:]

proof end;

theorem Th64: :: FUNCT_4:64

for b₁, b₂, b₃, b₄ being set
for b₅, b₆ being non empty set
for b₇ being Function of [:b₁,b₂:],b₅
for b₈ being Function of [:b₃,b₄:],b₆ holds |:b₇,b₈:| is Function of [:[:b₁,b₃:],[:b₂,b₄:]:],[:b₅,b₆:] by Th63;

definition

let c₁, c₂, c₃, c₄ be set ;
func c₁,c₂ --> c₃,c₄ -> set equals :: FUNCT_4:def 4
({a₁} --> a₃) +* ({a₂} --> a₄);
correctness ;

end;

:: deftheorem Def4 defines --> FUNCT_4:def 4 :

registration

let c₁, c₂, c₃, c₄ be set ;
cluster a₁,a₂ --> a₃,a₄ -> Relation-like Function-like ;
coherence ;

end;

theorem Th65: :: FUNCT_4:65

for b₁, b₂, b₃, b₄ being set holds
( dom (b₁,b₂ --> b₃,b₄) = {b₁,b₂} & rng (b₁,b₂ --> b₃,b₄) c= {b₃,b₄} )

proof end;

theorem Th66: :: FUNCT_4:66

for b₁, b₂, b₃, b₄ being set st b₁ <> b₂ holds
( (b₁,b₂ --> b₃,b₄) . b₁ = b₃ & (b₁,b₂ --> b₃,b₄) . b₂ = b₄ )

proof end;

theorem Th67: :: FUNCT_4:67

for b₁, b₂, b₃, b₄ being set st b₁ <> b₂ holds
rng (b₁,b₂ --> b₃,b₄) = {b₃,b₄}

proof end;

theorem Th68: :: FUNCT_4:68

for b₁, b₂, b₃ being set holds b₁,b₂ --> b₃,b₃ = {b₁,b₂} --> b₃

proof end;

definition

let c₁ be non empty set ;
let c₂, c₃ be set ;
let c₄, c₅ be Element of c₁;
redefine func --> as c₂,c₃ --> c₄,c₅ -> Function of {a₂,a₃},a₁;
coherence

proof end;

end;

theorem Th69: :: FUNCT_4:69

for b₁, b₂, b₃, b₄ being set
for b₅ being Function st dom b₅ = {b₁,b₂} & b₅ . b₁ = b₃ & b₅ . b₂ = b₄ holds
b₅ = b₁,b₂ --> b₃,b₄

proof end;

theorem Th70: :: FUNCT_4:70

for b₁, b₂ being set holds {b₁} --> b₂ = {[b₁,b₂]}

proof end;

theorem Th71: :: FUNCT_4:71

for b₁, b₂, b₃, b₄ being set st b₁ <> b₃ holds
b₁,b₃ --> b₂,b₄ = {[b₁,b₂],[b₃,b₄]}

proof end;

theorem Th72: :: FUNCT_4:72

for b₁, b₂, b₃, b₄, b₅, b₆ being set st b₁ <> b₂ & b₁,b₂ --> b₃,b₄ = b₁,b₂ --> b₅,b₆ holds
( b₃ = b₅ & b₄ = b₆ )

proof end;

theorem Th73: :: FUNCT_4:73

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

proof end;

theorem Th74: :: FUNCT_4:74

for b₁ being Function
for b₂, b₃ being set st dom b₁ c= b₂ \/ b₃ holds
(b₁ | b₂) +* (b₁ | b₃) = b₁

proof end;

theorem Th75: :: FUNCT_4:75

for b₁, b₂ being Function
for b₃ being set holds (b₁ +* b₂) | b₃ = (b₁ | b₃) +* (b₂ | b₃)

proof end;

theorem Th76: :: FUNCT_4:76

for b₁, b₂ being Function
for b₃ being set st b₃ misses dom b₂ holds
(b₁ +* b₂) | b₃ = b₁ | b₃

proof end;

theorem Th77: :: FUNCT_4:77

for b₁, b₂ being Function
for b₃ being set st dom b₁ misses b₃ holds
(b₁ +* b₂) | b₃ = b₂ | b₃

proof end;

theorem Th78: :: FUNCT_4:78

for b₁, b₂, b₃ being Function st dom b₂ = dom b₃ holds
(b₁ +* b₂) +* b₃ = b₁ +* b₃

proof end;

theorem Th79: :: FUNCT_4:79

for b₁, b₂ being Function st b₁ c= b₂ holds
( b₁ +* b₂ = b₂ & b₂ +* b₁ = b₂ )

proof end;

theorem Th80: :: FUNCT_4:80

for b₁ being Function
for b₂ being set holds b₁ +* (b₁ | b₂) = b₁

proof end;

theorem Th81: :: FUNCT_4:81

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

proof end;

theorem Th82: :: FUNCT_4:82

for b₁, b₂ being Function
for b₃ being set st dom b₁ c= b₃ & dom b₂ misses b₃ holds
(b₁ +* b₂) | b₃ = b₁

proof end;

theorem Th83: :: FUNCT_4:83

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

proof end;