:: FUNCT_5 semantic presentation

scheme :: FUNCT_5:sch 1
s1{ F₁() -> set , F₂( set ) -> set } :

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

proof end;

theorem Th1: :: FUNCT_5:1

proof end;

definition

let c₁ be set ;
func proj1 c₁ -> set means :Def1: :: FUNCT_5:def 1
for b₁ being set holds
( b₁ in a₂ iff ex b₂ being set st [b₁,b₂] in a₁ );
existence

proof end;

uniqueness

proof end;

func proj2 c₁ -> set means :Def2: :: FUNCT_5:def 2
for b₁ being set holds
( b₁ in a₂ iff ex b₂ being set st [b₂,b₁] in a₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines proj1 FUNCT_5:def 1 :

:: deftheorem Def2 defines proj2 FUNCT_5:def 2 :

theorem Th2: :: FUNCT_5:2

canceled;

theorem Th3: :: FUNCT_5:3

canceled;

theorem Th4: :: FUNCT_5:4

for b₁, b₂, b₃ being set st [b₁,b₂] in b₃ holds
( b₁ in proj1 b₃ & b₂ in proj2 b₃ ) by Def1, Def2;

theorem Th5: :: FUNCT_5:5

for b₁, b₂ being set st b₁ c= b₂ holds
( proj1 b₁ c= proj1 b₂ & proj2 b₁ c= proj2 b₂ )

proof end;

theorem Th6: :: FUNCT_5:6

for b₁, b₂ being set holds
( proj1 (b₁ \/ b₂) = (proj1 b₁) \/ (proj1 b₂) & proj2 (b₁ \/ b₂) = (proj2 b₁) \/ (proj2 b₂) )

proof end;

theorem Th7: :: FUNCT_5:7

for b₁, b₂ being set holds
( proj1 (b₁ /\ b₂) c= (proj1 b₁) /\ (proj1 b₂) & proj2 (b₁ /\ b₂) c= (proj2 b₁) /\ (proj2 b₂) )

proof end;

theorem Th8: :: FUNCT_5:8

for b₁, b₂ being set holds
( (proj1 b₁) \ (proj1 b₂) c= proj1 (b₁ \ b₂) & (proj2 b₁) \ (proj2 b₂) c= proj2 (b₁ \ b₂) )

proof end;

theorem Th9: :: FUNCT_5:9

for b₁, b₂ being set holds
( (proj1 b₁) \+\ (proj1 b₂) c= proj1 (b₁ \+\ b₂) & (proj2 b₁) \+\ (proj2 b₂) c= proj2 (b₁ \+\ b₂) )

proof end;

theorem Th10: :: FUNCT_5:10

( proj1 {} = {} & proj2 {} = {} )

proof end;

theorem Th11: :: FUNCT_5:11

for b₁, b₂ being set st ( b₁ <> {} or [:b₂,b₁:] <> {} or [:b₁,b₂:] <> {} ) holds
( proj1 [:b₂,b₁:] = b₂ & proj2 [:b₁,b₂:] = b₂ )

proof end;

theorem Th12: :: FUNCT_5:12

for b₁, b₂ being set holds
( proj1 [:b₁,b₂:] c= b₁ & proj2 [:b₁,b₂:] c= b₂ )

proof end;

theorem Th13: :: FUNCT_5:13

for b₁, b₂, b₃ being set st b₁ c= [:b₂,b₃:] holds
( proj1 b₁ c= b₂ & proj2 b₁ c= b₃ )

proof end;

theorem Th14: :: FUNCT_5:14

canceled;

theorem Th15: :: FUNCT_5:15

for b₁, b₂ being set holds
( proj1 {[b₁,b₂]} = {b₁} & proj2 {[b₁,b₂]} = {b₂} )

proof end;

theorem Th16: :: FUNCT_5:16

for b₁, b₂, b₃, b₄ being set holds
( proj1 {[b₁,b₂],[b₃,b₄]} = {b₁,b₃} & proj2 {[b₁,b₂],[b₃,b₄]} = {b₂,b₄} )

proof end;

theorem Th17: :: FUNCT_5:17

for b₁ being set st ( for b₂, b₃ being set holds not [b₂,b₃] in b₁ ) holds
( proj1 b₁ = {} & proj2 b₁ = {} )

proof end;

theorem Th18: :: FUNCT_5:18

for b₁ being set st ( proj1 b₁ = {} or proj2 b₁ = {} ) holds
for b₂, b₃ being set holds not [b₂,b₃] in b₁ by Def1, Def2;

theorem Th19: :: FUNCT_5:19

for b₁ being set holds
( proj1 b₁ = {} iff proj2 b₁ = {} )

proof end;

theorem Th20: :: FUNCT_5:20

for b₁ being Function holds
( proj1 (dom b₁) = proj2 (dom (~ b₁)) & proj2 (dom b₁) = proj1 (dom (~ b₁)) )

proof end;

theorem Th21: :: FUNCT_5:21

for b₁ being Relation holds
( proj1 b₁ = dom b₁ & proj2 b₁ = rng b₁ )

proof end;

definition

let c₁ be Function;
func curry c₁ -> Function means :Def3: :: FUNCT_5:def 3
( dom a₂ = proj1 (dom a₁) & ( for b₁ being set st b₁ in proj1 (dom a₁) holds
ex b₂ being Function st
( a₂ . b₁ = b₂ & dom b₂ = proj2 ((dom a₁) /\ [:{b₁},(proj2 (dom a₁)):]) & ( for b₃ being set st b₃ in dom b₂ holds
b₂ . b₃ = a₁ . [b₁,b₃] ) ) ) );
existence

proof end;

uniqueness

proof end;

func uncurry c₁ -> Function means :Def4: :: FUNCT_5:def 4
( ( for b₁ being set holds
( b₁ in dom a₂ iff ex b₂ being set ex b₃ being Functionex b₄ being set st
( b₁ = [b₂,b₄] & b₂ in dom a₁ & b₃ = a₁ . b₂ & b₄ in dom b₃ ) ) ) & ( for b₁ being set
for b₂ being Function st b₁ in dom a₂ & b₂ = a₁ . (b₁ `1 ) holds
a₂ . b₁ = b₂ . (b₁ `2 ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines curry FUNCT_5:def 3 :

:: deftheorem Def4 defines uncurry FUNCT_5:def 4 :

definition

let c₁ be Function;
func curry' c₁ -> Function equals :: FUNCT_5:def 5
curry (~ a₁);
correctness ;
func uncurry' c₁ -> Function equals :: FUNCT_5:def 6
~ (uncurry a₁);
correctness ;

end;

:: deftheorem Def5 defines curry' FUNCT_5:def 5 :

:: deftheorem Def6 defines uncurry' FUNCT_5:def 6 :

theorem Th22: :: FUNCT_5:22

canceled;

theorem Th23: :: FUNCT_5:23

canceled;

theorem Th24: :: FUNCT_5:24

canceled;

theorem Th25: :: FUNCT_5:25

canceled;

theorem Th26: :: FUNCT_5:26

for b₁, b₂ being set
for b₃ being Function st [b₁,b₂] in dom b₃ holds
( b₁ in dom (curry b₃) & (curry b₃) . b₁ is Function )

proof end;

theorem Th27: :: FUNCT_5:27

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

proof end;

theorem Th28: :: FUNCT_5:28

for b₁, b₂ being set
for b₃ being Function st [b₁,b₂] in dom b₃ holds
( b₂ in dom (curry' b₃) & (curry' b₃) . b₂ is Function )

proof end;

theorem Th29: :: FUNCT_5:29

for b₁, b₂ being set
for b₃, b₄ being Function st [b₁,b₂] in dom b₃ & b₄ = (curry' b₃) . b₂ holds
( b₁ in dom b₄ & b₄ . b₁ = b₃ . [b₁,b₂] )

proof end;

theorem Th30: :: FUNCT_5:30

for b₁ being Function holds dom (curry' b₁) = proj2 (dom b₁)

proof end;

theorem Th31: :: FUNCT_5:31

for b₁, b₂ being set
for b₃ being Function st [:b₁,b₂:] <> {} & dom b₃ = [:b₁,b₂:] holds
( dom (curry b₃) = b₁ & dom (curry' b₃) = b₂ )

proof end;

theorem Th32: :: FUNCT_5:32

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

proof end;

theorem Th33: :: FUNCT_5:33

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

proof end;

theorem Th34: :: FUNCT_5:34

for b₁ being Function st ( for b₂, b₃ being set holds not [b₂,b₃] in dom b₁ ) holds
( curry b₁ = {} & curry' b₁ = {} )

proof end;

theorem Th35: :: FUNCT_5:35

for b₁ being Function st ( for b₂ being set holds
( not b₂ in dom b₁ or not b₁ . b₂ is Function ) ) holds
( uncurry b₁ = {} & uncurry' b₁ = {} )

proof end;

theorem Th36: :: FUNCT_5:36

for b₁, b₂, b₃ being set
for b₄ being Function st [:b₁,b₂:] <> {} & dom b₄ = [:b₁,b₂:] & b₃ in b₁ holds
ex b₅ being Function st
( (curry b₄) . b₃ = b₅ & dom b₅ = b₂ & rng b₅ c= rng b₄ & ( for b₆ being set st b₆ in b₂ holds
b₅ . b₆ = b₄ . [b₃,b₆] ) )

proof end;

theorem Th37: :: FUNCT_5:37

for b₁ being set
for b₂ being Function st b₁ in dom (curry b₂) holds
(curry b₂) . b₁ is Function

proof end;

theorem Th38: :: FUNCT_5:38

for b₁ being set
for b₂, b₃ being Function st b₁ in dom (curry b₂) & b₃ = (curry b₂) . b₁ holds
( dom b₃ = proj2 ((dom b₂) /\ [:{b₁},(proj2 (dom b₂)):]) & dom b₃ c= proj2 (dom b₂) & rng b₃ c= rng b₂ & ( for b₄ being set st b₄ in dom b₃ holds
( b₃ . b₄ = b₂ . [b₁,b₄] & [b₁,b₄] in dom b₂ ) ) )

proof end;

theorem Th39: :: FUNCT_5:39

for b₁, b₂, b₃ being set
for b₄ being Function st [:b₁,b₂:] <> {} & dom b₄ = [:b₁,b₂:] & b₃ in b₂ holds
ex b₅ being Function st
( (curry' b₄) . b₃ = b₅ & dom b₅ = b₁ & rng b₅ c= rng b₄ & ( for b₆ being set st b₆ in b₁ holds
b₅ . b₆ = b₄ . [b₆,b₃] ) )

proof end;

theorem Th40: :: FUNCT_5:40

for b₁ being set
for b₂ being Function st b₁ in dom (curry' b₂) holds
(curry' b₂) . b₁ is Function by Th37;

theorem Th41: :: FUNCT_5:41

for b₁ being set
for b₂, b₃ being Function st b₁ in dom (curry' b₂) & b₃ = (curry' b₂) . b₁ holds
( dom b₃ = proj1 ((dom b₂) /\ [:(proj1 (dom b₂)),{b₁}:]) & dom b₃ c= proj1 (dom b₂) & rng b₃ c= rng b₂ & ( for b₄ being set st b₄ in dom b₃ holds
( b₃ . b₄ = b₂ . [b₄,b₁] & [b₄,b₁] in dom b₂ ) ) )

proof end;

theorem Th42: :: FUNCT_5:42

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

proof end;

theorem Th43: :: FUNCT_5:43

for b₁ being Function holds
( rng (curry b₁) c= PFuncs (proj2 (dom b₁)),(rng b₁) & rng (curry' b₁) c= PFuncs (proj1 (dom b₁)),(rng b₁) )

proof end;

theorem Th44: :: FUNCT_5:44

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

proof end;

theorem Th45: :: FUNCT_5:45

for b₁, b₂ being set
for b₃, b₄ being Function st b₁ in dom b₃ & b₄ = b₃ . b₁ & b₂ in dom b₄ holds
( [b₁,b₂] in dom (uncurry b₃) & (uncurry b₃) . [b₁,b₂] = b₄ . b₂ & b₄ . b₂ in rng (uncurry b₃) )

proof end;

theorem Th46: :: FUNCT_5:46

for b₁, b₂ being set
for b₃, b₄ being Function st b₁ in dom b₃ & b₄ = b₃ . b₁ & b₂ in dom b₄ holds
( [b₂,b₁] in dom (uncurry' b₃) & (uncurry' b₃) . [b₂,b₁] = b₄ . b₂ & b₄ . b₂ in rng (uncurry' b₃) )

proof end;

theorem Th47: :: FUNCT_5:47

for b₁, b₂ being set
for b₃ being Function st rng b₃ c= PFuncs b₁,b₂ holds
( rng (uncurry b₃) c= b₂ & rng (uncurry' b₃) c= b₂ )

proof end;

theorem Th48: :: FUNCT_5:48

for b₁, b₂ being set
for b₃ being Function st rng b₃ c= Funcs b₁,b₂ holds
( rng (uncurry b₃) c= b₂ & rng (uncurry' b₃) c= b₂ )

proof end;

theorem Th49: :: FUNCT_5:49

( curry {} = {} & curry' {} = {} )

proof end;

theorem Th50: :: FUNCT_5:50

( uncurry {} = {} & uncurry' {} = {} )

proof end;

theorem Th51: :: FUNCT_5:51

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

proof end;

theorem Th52: :: FUNCT_5:52

for b₁, b₂ being set
for b₃, b₄ being Function st dom b₃ = [:b₁,b₂:] & dom b₄ = [:b₁,b₂:] & curry' b₃ = curry' b₄ holds
b₃ = b₄

proof end;

theorem Th53: :: FUNCT_5:53

for b₁, b₂ being set
for b₃, b₄ being Function st rng b₃ c= Funcs b₁,b₂ & rng b₄ c= Funcs b₁,b₂ & b₁ <> {} & uncurry b₃ = uncurry b₄ holds
b₃ = b₄

proof end;

theorem Th54: :: FUNCT_5:54

for b₁, b₂ being set
for b₃, b₄ being Function st rng b₃ c= Funcs b₁,b₂ & rng b₄ c= Funcs b₁,b₂ & b₁ <> {} & uncurry' b₃ = uncurry' b₄ holds
b₃ = b₄

proof end;

theorem Th55: :: FUNCT_5:55

for b₁, b₂ being set
for b₃ being Function st rng b₃ c= Funcs b₁,b₂ & b₁ <> {} holds
( curry (uncurry b₃) = b₃ & curry' (uncurry' b₃) = b₃ )

proof end;

theorem Th56: :: FUNCT_5:56

for b₁, b₂ being set
for b₃ being Function st dom b₃ = [:b₁,b₂:] holds
( uncurry (curry b₃) = b₃ & uncurry' (curry' b₃) = b₃ )

proof end;

theorem Th57: :: FUNCT_5:57

for b₁, b₂ being set
for b₃ being Function st dom b₃ c= [:b₁,b₂:] holds
( uncurry (curry b₃) = b₃ & uncurry' (curry' b₃) = b₃ )

proof end;

theorem Th58: :: FUNCT_5:58

for b₁, b₂ being set
for b₃ being Function st rng b₃ c= PFuncs b₁,b₂ & not {} in rng b₃ holds
( curry (uncurry b₃) = b₃ & curry' (uncurry' b₃) = b₃ )

proof end;

theorem Th59: :: FUNCT_5:59

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

proof end;

theorem Th60: :: FUNCT_5:60

for b₁, b₂ being set
for b₃, b₄ being Function st dom b₃ c= [:b₁,b₂:] & dom b₄ c= [:b₁,b₂:] & curry' b₃ = curry' b₄ holds
b₃ = b₄

proof end;

theorem Th61: :: FUNCT_5:61

for b₁, b₂ being set
for b₃, b₄ being Function st rng b₃ c= PFuncs b₁,b₂ & rng b₄ c= PFuncs b₁,b₂ & not {} in rng b₃ & not {} in rng b₄ & uncurry b₃ = uncurry b₄ holds
b₃ = b₄

proof end;

theorem Th62: :: FUNCT_5:62

for b₁, b₂ being set
for b₃, b₄ being Function st rng b₃ c= PFuncs b₁,b₂ & rng b₄ c= PFuncs b₁,b₂ & not {} in rng b₃ & not {} in rng b₄ & uncurry' b₃ = uncurry' b₄ holds
b₃ = b₄

proof end;

theorem Th63: :: FUNCT_5:63

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

proof end;

theorem Th64: :: FUNCT_5:64

for b₁ being set holds Funcs {} ,b₁ = {{} }

proof end;

theorem Th65: :: FUNCT_5:65

for b₁, b₂ being set holds
( b₁, Funcs {b₂},b₁ are_equipotent & Card b₁ = Card (Funcs {b₂},b₁) )

proof end;

theorem Th66: :: FUNCT_5:66

for b₁, b₂ being set holds Funcs b₁,{b₂} = {(b₁ --> b₂)}

proof end;

theorem Th67: :: FUNCT_5:67

for b₁, b₂, b₃, b₄ being set st b₁,b₂ are_equipotent & b₃,b₄ are_equipotent holds
( Funcs b₁,b₃, Funcs b₂,b₄ are_equipotent & Card (Funcs b₁,b₃) = Card (Funcs b₂,b₄) )

proof end;

theorem Th68: :: FUNCT_5:68

for b₁, b₂, b₃, b₄ being set st Card b₁ = Card b₂ & Card b₃ = Card b₄ holds
Card (Funcs b₁,b₃) = Card (Funcs b₂,b₄)

proof end;

theorem Th69: :: FUNCT_5:69

for b₁, b₂, b₃ being set st b₁ misses b₂ holds
( Funcs (b₁ \/ b₂),b₃,[:(Funcs b₁,b₃),(Funcs b₂,b₃):] are_equipotent & Card (Funcs (b₁ \/ b₂),b₃) = Card [:(Funcs b₁,b₃),(Funcs b₂,b₃):] )

proof end;

theorem Th70: :: FUNCT_5:70

for b₁, b₂, b₃ being set holds
( Funcs [:b₁,b₂:],b₃, Funcs b₁,(Funcs b₂,b₃) are_equipotent & Card (Funcs [:b₁,b₂:],b₃) = Card (Funcs b₁,(Funcs b₂,b₃)) )

proof end;

theorem Th71: :: FUNCT_5:71

for b₁, b₂, b₃ being set holds
( Funcs b₁,[:b₂,b₃:],[:(Funcs b₁,b₂),(Funcs b₁,b₃):] are_equipotent & Card (Funcs b₁,[:b₂,b₃:]) = Card [:(Funcs b₁,b₂),(Funcs b₁,b₃):] )

proof end;

theorem Th72: :: FUNCT_5:72

for b₁, b₂, b₃ being set st b₁ <> b₂ holds
( Funcs b₃,{b₁,b₂}, bool b₃ are_equipotent & Card (Funcs b₃,{b₁,b₂}) = Card (bool b₃) )

proof end;

theorem Th73: :: FUNCT_5:73

for b₁, b₂, b₃ being set st b₁ <> b₂ holds
( Funcs {b₁,b₂},b₃,[:b₃,b₃:] are_equipotent & Card (Funcs {b₁,b₂},b₃) = Card [:b₃,b₃:] )

proof end;