:: FUNCT_6 semantic presentation

theorem Th1: :: FUNCT_6:1

for b₁, b₂ being set holds
( b₁ in product <*b₂*> iff ex b₃ being set st
( b₃ in b₂ & b₁ = <*b₃*> ) )

proof end;

theorem Th2: :: FUNCT_6:2

for b₁, b₂, b₃ being set holds
( b₁ in product <*b₂,b₃*> iff ex b₄, b₅ being set st
( b₄ in b₂ & b₅ in b₃ & b₁ = <*b₄,b₅*> ) )

proof end;

theorem Th3: :: FUNCT_6:3

for b₁, b₂, b₃, b₄ being set holds
( b₁ in product <*b₂,b₃,b₄*> iff ex b₅, b₆, b₇ being set st
( b₅ in b₂ & b₆ in b₃ & b₇ in b₄ & b₁ = <*b₅,b₆,b₇*> ) )

proof end;

theorem Th4: :: FUNCT_6:4

for b₁ being non empty set holds product <*b₁*> = 1 -tuples_on b₁

proof end;

theorem Th5: :: FUNCT_6:5

for b₁, b₂ being non empty set holds product <*b₁,b₂*> = { <*b₃,b₄*> where B is Element of b₁, B is Element of b₂ : verum }

proof end;

theorem Th6: :: FUNCT_6:6

for b₁ being non empty set holds product <*b₁,b₁*> = 2 -tuples_on b₁

proof end;

theorem Th7: :: FUNCT_6:7

for b₁, b₂, b₃ being non empty set holds product <*b₁,b₂,b₃*> = { <*b₄,b₅,b₆*> where B is Element of b₁, B is Element of b₂, B is Element of b₃ : verum }

proof end;

theorem Th8: :: FUNCT_6:8

for b₁ being non empty set holds product <*b₁,b₁,b₁*> = 3 -tuples_on b₁

proof end;

theorem Th9: :: FUNCT_6:9

for b₁ being Nat
for b₂ being non empty set holds product (b₁ |-> b₂) = b₁ -tuples_on b₂

proof end;

theorem Th10: :: FUNCT_6:10

for b₁ being Function holds product b₁ c= Funcs (dom b₁),(Union b₁)

proof end;

theorem Th11: :: FUNCT_6:11

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

proof end;

theorem Th12: :: FUNCT_6:12

for b₁, b₂, b₃ being set holds ~ ([:b₁,b₂:] --> b₃) = [:b₂,b₁:] --> b₃

proof end;

theorem Th13: :: FUNCT_6:13

for b₁ being Function holds
( curry b₁ = curry' (~ b₁) & uncurry b₁ = ~ (uncurry' b₁) )

proof end;

theorem Th14: :: FUNCT_6:14

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

proof end;

theorem Th15: :: FUNCT_6:15

for b₁, b₂, b₃ being set holds
( uncurry (b₁ --> (b₂ --> b₃)) = [:b₁,b₂:] --> b₃ & uncurry' (b₁ --> (b₂ --> b₃)) = [:b₂,b₁:] --> b₃ )

proof end;

theorem Th16: :: FUNCT_6:16

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

proof end;

theorem Th17: :: FUNCT_6:17

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

proof end;

theorem Th18: :: FUNCT_6:18

for b₁ being set
for b₂ being Function st b₁ <> {} holds
( rng (uncurry (b₁ --> b₂)) = rng b₂ & rng (uncurry' (b₁ --> b₂)) = rng b₂ )

proof end;

theorem Th19: :: FUNCT_6:19

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

proof end;

theorem Th20: :: FUNCT_6:20

for b₁, b₂, b₃ being set
for b₄ being Function st b₄ in Funcs b₁,(Funcs b₂,b₃) holds
( uncurry b₄ in Funcs [:b₁,b₂:],b₃ & uncurry' b₄ in Funcs [:b₂,b₁:],b₃ )

proof end;

theorem Th21: :: FUNCT_6:21

for b₁, b₂, b₃, b₄, b₅ being set
for b₆ being Function st ( curry b₆ in Funcs b₁,(Funcs b₂,b₃) or curry' b₆ in Funcs b₂,(Funcs b₁,b₃) ) & dom b₆ c= [:b₄,b₅:] holds
b₆ in Funcs [:b₁,b₂:],b₃

proof end;

theorem Th22: :: FUNCT_6:22

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

proof end;

theorem Th23: :: FUNCT_6:23

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

proof end;

theorem Th24: :: FUNCT_6:24

for b₁, b₂, b₃ being set
for b₄ being Function st b₄ in PFuncs b₁,(PFuncs b₂,b₃) holds
( uncurry b₄ in PFuncs [:b₁,b₂:],b₃ & uncurry' b₄ in PFuncs [:b₂,b₁:],b₃ )

proof end;

theorem Th25: :: FUNCT_6:25

for b₁, b₂, b₃, b₄, b₅ being set
for b₆ being Function st ( curry b₆ in PFuncs b₁,(PFuncs b₂,b₃) or curry' b₆ in PFuncs b₂,(PFuncs b₁,b₃) ) & dom b₆ c= [:b₄,b₅:] holds
b₆ in PFuncs [:b₁,b₂:],b₃

proof end;

theorem Th26: :: FUNCT_6:26

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

proof end;

definition

let c₁ be set ;
func SubFuncs c₁ -> set means :Def1: :: FUNCT_6:def 1
for b₁ being set holds
( b₁ in a₂ iff ( b₁ in a₁ & b₁ is Function ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines SubFuncs FUNCT_6:def 1 :

theorem Th27: :: FUNCT_6:27

for b₁ being set holds SubFuncs b₁ c= b₁

proof end;

theorem Th28: :: FUNCT_6:28

for b₁ being set
for b₂ being Function holds
( b₁ in b₂ " (SubFuncs (rng b₂)) iff ( b₁ in dom b₂ & b₂ . b₁ is Function ) )

proof end;

Lemma18: for b₁ being set st ( for b₂ being set st b₂ in b₁ holds
b₂ is Function ) holds
SubFuncs b₁ = b₁

proof end;

theorem Th29: :: FUNCT_6:29

for b₁, b₂, b₃ being Function holds
( SubFuncs {} = {} & SubFuncs {b₁} = {b₁} & SubFuncs {b₁,b₂} = {b₁,b₂} & SubFuncs {b₁,b₂,b₃} = {b₁,b₂,b₃} )

proof end;

theorem Th30: :: FUNCT_6:30

for b₁, b₂ being set st b₁ c= SubFuncs b₂ holds
SubFuncs b₁ = b₁

proof end;

definition

let c₁ be Function;
func doms c₁ -> Function means :Def2: :: FUNCT_6:def 2
( dom a₂ = a₁ " (SubFuncs (rng a₁)) & ( for b₁ being set st b₁ in a₁ " (SubFuncs (rng a₁)) holds
a₂ . b₁ = proj1 (a₁ . b₁) ) );
existence

proof end;

uniqueness

proof end;

func rngs c₁ -> Function means :Def3: :: FUNCT_6:def 3
( dom a₂ = a₁ " (SubFuncs (rng a₁)) & ( for b₁ being set st b₁ in a₁ " (SubFuncs (rng a₁)) holds
a₂ . b₁ = proj2 (a₁ . b₁) ) );
existence

proof end;

uniqueness

proof end;

func meet c₁ -> set equals :: FUNCT_6:def 4
meet (rng a₁);
correctness ;

end;

:: deftheorem Def2 defines doms FUNCT_6:def 2 :

:: deftheorem Def3 defines rngs FUNCT_6:def 3 :

:: deftheorem Def4 defines meet FUNCT_6:def 4 :

theorem Th31: :: FUNCT_6:31

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

proof end;

theorem Th32: :: FUNCT_6:32

( doms {} = {} & rngs {} = {} )

proof end;

theorem Th33: :: FUNCT_6:33

for b₁ being Function holds
( doms <*b₁*> = <*(dom b₁)*> & rngs <*b₁*> = <*(rng b₁)*> )

proof end;

theorem Th34: :: FUNCT_6:34

for b₁, b₂ being Function holds
( doms <*b₁,b₂*> = <*(dom b₁),(dom b₂)*> & rngs <*b₁,b₂*> = <*(rng b₁),(rng b₂)*> )

proof end;

theorem Th35: :: FUNCT_6:35

for b₁, b₂, b₃ being Function holds
( doms <*b₁,b₂,b₃*> = <*(dom b₁),(dom b₂),(dom b₃)*> & rngs <*b₁,b₂,b₃*> = <*(rng b₁),(rng b₂),(rng b₃)*> )

proof end;

theorem Th36: :: FUNCT_6:36

for b₁ being set
for b₂ being Function holds
( doms (b₁ --> b₂) = b₁ --> (dom b₂) & rngs (b₁ --> b₂) = b₁ --> (rng b₂) )

proof end;

theorem Th37: :: FUNCT_6:37

for b₁ being set
for b₂ being Function st b₂ <> {} holds
( b₁ in meet b₂ iff for b₃ being set st b₃ in dom b₂ holds
b₁ in b₂ . b₃ )

proof end;

theorem Th38: :: FUNCT_6:38

meet {} = {} by SETFAM_1:2;

theorem Th39: :: FUNCT_6:39

for b₁ being set holds
( Union <*b₁*> = b₁ & meet <*b₁*> = b₁ )

proof end;

theorem Th40: :: FUNCT_6:40

for b₁, b₂ being set holds
( Union <*b₁,b₂*> = b₁ \/ b₂ & meet <*b₁,b₂*> = b₁ /\ b₂ )

proof end;

theorem Th41: :: FUNCT_6:41

for b₁, b₂, b₃ being set holds
( Union <*b₁,b₂,b₃*> = (b₁ \/ b₂) \/ b₃ & meet <*b₁,b₂,b₃*> = (b₁ /\ b₂) /\ b₃ )

proof end;

theorem Th42: :: FUNCT_6:42

for b₁ being set holds
( Union ({} --> b₁) = {} & meet ({} --> b₁) = {} )

proof end;

theorem Th43: :: FUNCT_6:43

for b₁, b₂ being set st b₁ <> {} holds
( Union (b₁ --> b₂) = b₂ & meet (b₁ --> b₂) = b₂ )

proof end;

definition

let c₁ be Function;
let c₂, c₃ be set ;
func c₁ .. c₂,c₃ -> set equals :: FUNCT_6:def 5
(uncurry a₁) . [a₂,a₃];
correctness ;

end;

:: deftheorem Def5 defines .. FUNCT_6:def 5 :

theorem Th44: :: FUNCT_6:44

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₁,b₂ = b₄ . b₂ by FUNCT_5:45;

theorem Th45: :: FUNCT_6:45

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

proof end;

theorem Th46: :: FUNCT_6:46

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

proof end;

theorem Th47: :: FUNCT_6:47

for b₁ being set
for b₂, b₃, b₄ being Function st b₁ in dom b₂ holds
<*b₃,b₄,b₂*> .. 3,b₁ = b₂ . b₁

proof end;

theorem Th48: :: FUNCT_6:48

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

proof end;

definition

let c₁ be Function;
func <:c₁:> -> Function equals :: FUNCT_6:def 6
curry ((uncurry' a₁) | [:(meet (doms a₁)),(dom a₁):]);
correctness ;

end;

:: deftheorem Def6 defines <: FUNCT_6:def 6 :

theorem Th49: :: FUNCT_6:49

for b₁ being Function holds
( dom <:b₁:> = meet (doms b₁) & rng <:b₁:> c= product (rngs b₁) )

proof end;

theorem Th50: :: FUNCT_6:50

for b₁ being set
for b₂ being Function st b₁ in dom <:b₂:> holds
<:b₂:> . b₁ is Function

proof end;

theorem Th51: :: FUNCT_6:51

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

proof end;

theorem Th52: :: FUNCT_6:52

for b₁ being set
for b₂ being Function st b₁ in dom <:b₂:> holds
for b₃ being Function st b₃ in rng b₂ holds
b₁ in dom b₃

proof end;

theorem Th53: :: FUNCT_6:53

for b₁ being set
for b₂, b₃ being Function st b₂ in rng b₃ & ( for b₄ being Function st b₄ in rng b₃ holds
b₁ in dom b₄ ) holds
b₁ in dom <:b₃:>

proof end;

theorem Th54: :: FUNCT_6:54

for b₁, b₂ being set
for b₃, b₄, b₅ being Function st b₁ in dom b₃ & b₄ = b₃ . b₁ & b₂ in dom <:b₃:> & b₅ = <:b₃:> . b₂ holds
b₄ . b₂ = b₅ . b₁

proof end;

theorem Th55: :: FUNCT_6:55

for b₁, b₂ being set
for b₃ being Function st b₁ in dom b₃ & b₃ . b₁ is Function & b₂ in dom <:b₃:> holds
b₃ .. b₁,b₂ = <:b₃:> .. b₂,b₁

proof end;

definition

let c₁ be Function;
func Frege c₁ -> Function means :Def7: :: FUNCT_6:def 7
( dom a₂ = product (doms a₁) & ( for b₁ being Function st b₁ in product (doms a₁) holds
ex b₂ being Function st
( a₂ . b₁ = b₂ & dom b₂ = a₁ " (SubFuncs (rng a₁)) & ( for b₃ being set st b₃ in dom b₂ holds
b₂ . b₃ = (uncurry a₁) . [b₃,(b₁ . b₃)] ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines Frege FUNCT_6:def 7 :

theorem Th56: :: FUNCT_6:56

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

proof end;

Lemma37: for b₁ being Function holds rng (Frege b₁) c= product (rngs b₁)

proof end;

theorem Th57: :: FUNCT_6:57

for b₁ being set
for b₂, b₃, b₄, b₅ being Function st b₁ in dom b₂ & b₃ = b₂ . b₁ & b₄ in product (doms b₂) & b₅ = (Frege b₂) . b₄ holds
( b₄ . b₁ in dom b₃ & b₅ . b₁ = b₃ . (b₄ . b₁) & b₅ in product (rngs b₂) )

proof end;

Lemma39: for b₁ being Function holds product (rngs b₁) c= rng (Frege b₁)

proof end;

theorem Th58: :: FUNCT_6:58

for b₁ being Function holds rng (Frege b₁) = product (rngs b₁)

proof end;

theorem Th59: :: FUNCT_6:59

for b₁ being Function st not {} in rng b₁ holds
( Frege b₁ is one-to-one iff for b₂ being Function st b₂ in rng b₁ holds
b₂ is one-to-one )

proof end;

theorem Th60: :: FUNCT_6:60

( <:{} :> = {} & Frege {} = {{} } --> {} )

proof end;

theorem Th61: :: FUNCT_6:61

for b₁ being Function holds
( dom <:<*b₁*>:> = dom b₁ & ( for b₂ being set st b₂ in dom b₁ holds
<:<*b₁*>:> . b₂ = <*(b₁ . b₂)*> ) )

proof end;

theorem Th62: :: FUNCT_6:62

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

proof end;

theorem Th63: :: FUNCT_6:63

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

proof end;

theorem Th64: :: FUNCT_6:64

for b₁ being Function holds
( dom (Frege <*b₁*>) = product <*(dom b₁)*> & rng (Frege <*b₁*>) = product <*(rng b₁)*> & ( for b₂ being set st b₂ in dom b₁ holds
(Frege <*b₁*>) . <*b₂*> = <*(b₁ . b₂)*> ) )

proof end;

theorem Th65: :: FUNCT_6:65

for b₁, b₂ being Function holds
( dom (Frege <*b₁,b₂*>) = product <*(dom b₁),(dom b₂)*> & rng (Frege <*b₁,b₂*>) = product <*(rng b₁),(rng b₂)*> & ( for b₃, b₄ being set st b₃ in dom b₁ & b₄ in dom b₂ holds
(Frege <*b₁,b₂*>) . <*b₃,b₄*> = <*(b₁ . b₃),(b₂ . b₄)*> ) )

proof end;

theorem Th66: :: FUNCT_6:66

for b₁ being set
for b₂ being Function holds
( dom (Frege (b₁ --> b₂)) = Funcs b₁,(dom b₂) & rng (Frege (b₁ --> b₂)) = Funcs b₁,(rng b₂) & ( for b₃ being Function st b₃ in Funcs b₁,(dom b₂) holds
(Frege (b₁ --> b₂)) . b₃ = b₂ * b₃ ) )

proof end;

theorem Th67: :: FUNCT_6:67

for b₁ being set
for b₂, b₃ being Function st b₁ in dom b₂ & b₁ in dom b₃ holds
for b₄, b₅ being set holds
( <:b₂,b₃:> . b₁ = [b₄,b₅] iff <:<*b₂,b₃*>:> . b₁ = <*b₄,b₅*> )

proof end;

theorem Th68: :: FUNCT_6:68

for b₁, b₂ being set
for b₃, b₄ being Function st b₁ in dom b₃ & b₂ in dom b₄ holds
for b₅, b₆ being set holds
( [:b₃,b₄:] . [b₁,b₂] = [b₅,b₆] iff (Frege <*b₃,b₄*>) . <*b₁,b₂*> = <*b₅,b₆*> )

proof end;

theorem Th69: :: FUNCT_6:69

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

proof end;

theorem Th70: :: FUNCT_6:70

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

proof end;

theorem Th71: :: FUNCT_6:71

for b₁ being set
for b₂ being Function
for b₃ being Permutation of b₁ st dom b₂ = b₁ holds
product b₂, product (b₂ * b₃) are_equipotent

proof end;

definition

let c₁ be Function;
let c₂ be set ;
func Funcs c₁,c₂ -> Function means :Def8: :: FUNCT_6:def 8
( dom a₃ = dom a₁ & ( for b₁ being set st b₁ in dom a₁ holds
a₃ . b₁ = Funcs (a₁ . b₁),a₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines Funcs FUNCT_6:def 8 :

theorem Th72: :: FUNCT_6:72

for b₁ being Function st not {} in rng b₁ holds
Funcs b₁,{} = (dom b₁) --> {}

proof end;

theorem Th73: :: FUNCT_6:73

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

proof end;

theorem Th74: :: FUNCT_6:74

for b₁, b₂ being set holds Funcs <*b₁*>,b₂ = <*(Funcs b₁,b₂)*>

proof end;

theorem Th75: :: FUNCT_6:75

for b₁, b₂, b₃ being set holds Funcs <*b₁,b₂*>,b₃ = <*(Funcs b₁,b₃),(Funcs b₂,b₃)*>

proof end;

theorem Th76: :: FUNCT_6:76

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

proof end;

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

proof end;

theorem Th77: :: FUNCT_6:77

for b₁ being set
for b₂ being Function holds Funcs (Union (disjoin b₂)),b₁, product (Funcs b₂,b₁) are_equipotent

proof end;

definition

let c₁ be set ;
let c₂ be Function;
func Funcs c₁,c₂ -> Function means :Def9: :: FUNCT_6:def 9
( dom a₃ = dom a₂ & ( for b₁ being set st b₁ in dom a₂ holds
a₃ . b₁ = Funcs a₁,(a₂ . b₁) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines Funcs FUNCT_6:def 9 :

Lemma49: for b₁ being set
for b₂ being Function st b₂ <> {} & b₁ <> {} holds
product (Funcs b₁,b₂), Funcs b₁,(product b₂) are_equipotent

proof end;

theorem Th78: :: FUNCT_6:78

for b₁ being Function holds Funcs {} ,b₁ = (dom b₁) --> {{} }

proof end;

theorem Th79: :: FUNCT_6:79

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

proof end;

theorem Th80: :: FUNCT_6:80

for b₁, b₂ being set holds Funcs b₁,<*b₂*> = <*(Funcs b₁,b₂)*>

proof end;

theorem Th81: :: FUNCT_6:81

for b₁, b₂, b₃ being set holds Funcs b₁,<*b₂,b₃*> = <*(Funcs b₁,b₂),(Funcs b₁,b₃)*>

proof end;

theorem Th82: :: FUNCT_6:82

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

proof end;

theorem Th83: :: FUNCT_6:83

for b₁ being set
for b₂ being Function holds product (Funcs b₁,b₂), Funcs b₁,(product b₂) are_equipotent

proof end;

definition

let c₁ be Function;
canceled;
canceled;
func commute c₁ -> Function-yielding Function equals :: FUNCT_6:def 12
curry' (uncurry a₁);
coherence

proof end;

end;

:: deftheorem Def10 FUNCT_6:def 10 :

:: deftheorem Def11 FUNCT_6:def 11 :

:: deftheorem Def12 defines commute FUNCT_6:def 12 :

theorem Th84: :: FUNCT_6:84

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

theorem Th85: :: FUNCT_6:85

for b₁, b₂, b₃ being set
for b₄ being Function st b₁ <> {} & b₂ <> {} & b₄ in Funcs b₁,(Funcs b₂,b₃) holds
commute b₄ in Funcs b₂,(Funcs b₁,b₃)

proof end;

theorem Th86: :: FUNCT_6:86

for b₁, b₂, b₃ being set
for b₄ being Function st b₁ <> {} & b₂ <> {} & b₄ in Funcs b₁,(Funcs b₂,b₃) holds
for b₅, b₆ being Function
for b₇, b₈ being set st b₇ in b₁ & b₈ in b₂ & b₄ . b₇ = b₅ & (commute b₄) . b₈ = b₆ holds
( b₆ . b₇ = b₅ . b₈ & dom b₆ = b₁ & dom b₅ = b₂ & rng b₆ c= b₃ & rng b₅ c= b₃ )

proof end;

theorem Th87: :: FUNCT_6:87

for b₁, b₂, b₃ being set
for b₄ being Function st b₁ <> {} & b₂ <> {} & b₄ in Funcs b₁,(Funcs b₂,b₃) holds
commute (commute b₄) = b₄

proof end;

Lemma53: for b₁ being Function st dom b₁ = {} holds
commute b₁ = {}
by RELAT_1:64, FUNCT_5:49, FUNCT_5:50;

theorem Th88: :: FUNCT_6:88

commute {} = {} by Lemma53, RELAT_1:60;

theorem Th89: :: FUNCT_6:89

for b₁ being Function-yielding Function holds dom (doms b₁) = dom b₁

proof end;

theorem Th90: :: FUNCT_6:90

for b₁ being Function-yielding Function holds dom (rngs b₁) = dom b₁

proof end;