:: FUNCT_3 semantic presentation

theorem Th1: :: FUNCT_3:1

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

proof end;

theorem Th2: :: FUNCT_3:2

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

proof end;

theorem Th3: :: FUNCT_3:3

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

proof end;

theorem Th4: :: FUNCT_3:4

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

proof end;

theorem Th5: :: FUNCT_3:5

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

proof end;

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

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

provided

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

proof end;

scheme :: FUNCT_3:sch 2
s2{ F₁() -> set , F₂() -> set , F₃( set , set ) -> set } :

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

proof end;

theorem Th6: :: FUNCT_3:6

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

proof end;

definition

let c₁ be Function;
func .: c₁ -> Function means :Def1: :: FUNCT_3:def 1
( dom a₂ = bool (dom a₁) & ( for b₁ being set st b₁ c= dom a₁ holds
a₂ . b₁ = a₁ .: b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines .: FUNCT_3:def 1 :

theorem Th7: :: FUNCT_3:7

canceled;

theorem Th8: :: FUNCT_3:8

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

proof end;

theorem Th9: :: FUNCT_3:9

for b₁ being Function holds (.: b₁) . {} = {}

proof end;

theorem Th10: :: FUNCT_3:10

for b₁ being Function holds rng (.: b₁) c= bool (rng b₁)

proof end;

theorem Th11: :: FUNCT_3:11

canceled;

theorem Th12: :: FUNCT_3:12

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

proof end;

theorem Th13: :: FUNCT_3:13

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

proof end;

theorem Th14: :: FUNCT_3:14

for b₁, b₂ being set
for b₃ being non empty set
for b₄ being Function of b₁,b₃ holds (.: b₄) " b₂ c= bool b₁

proof end;

theorem Th15: :: FUNCT_3:15

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

proof end;

theorem Th16: :: FUNCT_3:16

for b₁ being set
for b₂ being Function st b₁ c= bool (dom b₂) holds
b₂ .: (union b₁) = union ((.: b₂) .: b₁)

proof end;

theorem Th17: :: FUNCT_3:17

for b₁, b₂ being set
for b₃ being non empty set
for b₄ being Function of b₁,b₃ st b₂ c= bool b₁ holds
b₄ .: (union b₂) = union ((.: b₄) .: b₂)

proof end;

theorem Th18: :: FUNCT_3:18

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

proof end;

theorem Th19: :: FUNCT_3:19

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

proof end;

theorem Th20: :: FUNCT_3:20

for b₁, b₂ being Function holds .: (b₂ * b₁) = (.: b₂) * (.: b₁)

proof end;

theorem Th21: :: FUNCT_3:21

for b₁ being Function holds .: b₁ is Function of bool (dom b₁), bool (rng b₁)

proof end;

theorem Th22: :: FUNCT_3:22

for b₁, b₂ being set
for b₃ being Function of b₁,b₂ st ( b₂ = {} implies b₁ = {} ) holds
.: b₃ is Function of bool b₁, bool b₂

proof end;

definition

let c₁ be set ;
let c₂ be non empty set ;
let c₃ be Function of c₁,c₂;
redefine func .: as .: c₃ -> Function of bool a₁, bool a₂;
coherence by Th22;

end;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines " FUNCT_3:def 2 :

theorem Th23: :: FUNCT_3:23

canceled;

theorem Th24: :: FUNCT_3:24

for b₁ being set
for b₂ being Function st b₁ in dom (" b₂) holds
(" b₂) . b₁ = b₂ " b₁

proof end;

theorem Th25: :: FUNCT_3:25

for b₁ being Function holds rng (" b₁) c= bool (dom b₁)

proof end;

theorem Th26: :: FUNCT_3:26

canceled;

theorem Th27: :: FUNCT_3:27

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

proof end;

theorem Th28: :: FUNCT_3:28

for b₁ being set
for b₂ being Function holds (" b₂) " b₁ c= bool (rng b₂)

proof end;

theorem Th29: :: FUNCT_3:29

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

proof end;

theorem Th30: :: FUNCT_3:30

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

proof end;

theorem Th31: :: FUNCT_3:31

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

proof end;

theorem Th32: :: FUNCT_3:32

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

proof end;

theorem Th33: :: FUNCT_3:33

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

proof end;

theorem Th34: :: FUNCT_3:34

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

proof end;

theorem Th35: :: FUNCT_3:35

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

proof end;

theorem Th36: :: FUNCT_3:36

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

proof end;

theorem Th37: :: FUNCT_3:37

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

proof end;

theorem Th38: :: FUNCT_3:38

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

proof end;

theorem Th39: :: FUNCT_3:39

for b₁ being Function holds " b₁ is Function of bool (rng b₁), bool (dom b₁)

proof end;

definition

let c₁, c₂ be set ;
func chi c₁,c₂ -> Function means :Def3: :: FUNCT_3:def 3
( dom a₃ = a₂ & ( for b₁ being set st b₁ in a₂ holds
( ( b₁ in a₁ implies a₃ . b₁ = 1 ) & ( not b₁ in a₁ implies a₃ . b₁ = 0 ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines chi FUNCT_3:def 3 :

theorem Th40: :: FUNCT_3:40

canceled;

theorem Th41: :: FUNCT_3:41

canceled;

theorem Th42: :: FUNCT_3:42

for b₁, b₂, b₃ being set st (chi b₂,b₃) . b₁ = 1 holds
b₁ in b₂

proof end;

theorem Th43: :: FUNCT_3:43

for b₁, b₂, b₃ being set st b₁ in b₂ \ b₃ holds
(chi b₃,b₂) . b₁ = 0

proof end;

theorem Th44: :: FUNCT_3:44

canceled;

theorem Th45: :: FUNCT_3:45

canceled;

theorem Th46: :: FUNCT_3:46

canceled;

theorem Th47: :: FUNCT_3:47

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

proof end;

theorem Th48: :: FUNCT_3:48

for b₁, b₂ being set holds rng (chi b₁,b₂) c= {0,1}

proof end;

theorem Th49: :: FUNCT_3:49

for b₁ being set
for b₂ being Function of b₁,{0,1} holds b₂ = chi (b₂ " {1}),b₁

proof end;

definition

let c₁, c₂ be set ;
redefine func chi as chi c₁,c₂ -> Function of a₂,{0,1};
coherence

proof end;

end;

notation

let c₁ be set ;
let c₂ be Subset of c₁;
synonym incl c₂ for id c₁;

end;

definition

let c₁ be set ;
let c₂ be Subset of c₁;
redefine func incl as incl c₂ -> Function of a₂,a₁;
coherence

proof end;

end;

theorem Th50: :: FUNCT_3:50

canceled;

theorem Th51: :: FUNCT_3:51

canceled;

theorem Th52: :: FUNCT_3:52

canceled;

theorem Th53: :: FUNCT_3:53

for b₁ being set
for b₂ being Subset of b₁ holds incl b₂ = (id b₁) | b₂ by Th1;

theorem Th54: :: FUNCT_3:54

canceled;

theorem Th55: :: FUNCT_3:55

canceled;

theorem Th56: :: FUNCT_3:56

for b₁, b₂ being set
for b₃ being Subset of b₂ st b₁ in b₃ holds
(incl b₃) . b₁ in b₂

proof end;

definition

let c₁, c₂ be set ;
canceled;
func pr1 c₁,c₂ -> Function means :Def5: :: FUNCT_3:def 5
( dom a₃ = [:a₁,a₂:] & ( for b₁, b₂ being set st b₁ in a₁ & b₂ in a₂ holds
a₃ . [b₁,b₂] = b₁ ) );
existence

proof end;

uniqueness

proof end;

func pr2 c₁,c₂ -> Function means :Def6: :: FUNCT_3:def 6
( dom a₃ = [:a₁,a₂:] & ( for b₁, b₂ being set st b₁ in a₁ & b₂ in a₂ holds
a₃ . [b₁,b₂] = b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 FUNCT_3:def 4 :

:: deftheorem Def5 defines pr1 FUNCT_3:def 5 :

:: deftheorem Def6 defines pr2 FUNCT_3:def 6 :

theorem Th57: :: FUNCT_3:57

canceled;

theorem Th58: :: FUNCT_3:58

canceled;

theorem Th59: :: FUNCT_3:59

for b₁, b₂ being set holds rng (pr1 b₁,b₂) c= b₁

proof end;

theorem Th60: :: FUNCT_3:60

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

proof end;

theorem Th61: :: FUNCT_3:61

for b₁, b₂ being set holds rng (pr2 b₁,b₂) c= b₂

proof end;

theorem Th62: :: FUNCT_3:62

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

proof end;

definition

let c₁, c₂ be set ;
redefine func pr1 as pr1 c₁,c₂ -> Function of [:a₁,a₂:],a₁;
coherence

proof end;

redefine func pr2 as pr2 c₁,c₂ -> Function of [:a₁,a₂:],a₂;
coherence

proof end;

end;

definition

let c₁ be set ;
func delta c₁ -> Function means :Def7: :: FUNCT_3:def 7
( dom a₂ = a₁ & ( for b₁ being set st b₁ in a₁ holds
a₂ . b₁ = [b₁,b₁] ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines delta FUNCT_3:def 7 :

theorem Th63: :: FUNCT_3:63

canceled;

theorem Th64: :: FUNCT_3:64

canceled;

theorem Th65: :: FUNCT_3:65

canceled;

theorem Th66: :: FUNCT_3:66

for b₁ being set holds rng (delta b₁) c= [:b₁,b₁:]

proof end;

definition

let c₁ be set ;
redefine func delta as delta c₁ -> Function of a₁,[:a₁,a₁:];
coherence

proof end;

end;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines <: FUNCT_3:def 8 :

theorem Th67: :: FUNCT_3:67

canceled;

theorem Th68: :: FUNCT_3:68

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

proof end;

theorem Th69: :: FUNCT_3:69

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

proof end;

theorem Th70: :: FUNCT_3:70

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

proof end;

theorem Th71: :: FUNCT_3:71

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

proof end;

theorem Th72: :: FUNCT_3:72

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

proof end;

theorem Th73: :: FUNCT_3:73

for b₁, b₂ being set holds <:(pr1 b₁,b₂),(pr2 b₁,b₂):> = id [:b₁,b₂:]

proof end;

theorem Th74: :: FUNCT_3:74

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

proof end;

theorem Th75: :: FUNCT_3:75

for b₁, b₂, b₃ being Function holds <:(b₁ * b₃),(b₂ * b₃):> = <:b₁,b₂:> * b₃

proof end;

theorem Th76: :: FUNCT_3:76

for b₁ being set
for b₂, b₃ being Function holds <:b₂,b₃:> .: b₁ c= [:(b₂ .: b₁),(b₃ .: b₁):]

proof end;

theorem Th77: :: FUNCT_3:77

for b₁ being set
for b₂ being non empty set
for b₃, b₄ being Function holds <:b₃,b₄:> " [:b₁,b₂:] = (b₃ " b₁) /\ (b₄ " b₂)

proof end;

theorem Th78: :: FUNCT_3:78

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

proof end;

definition

let c₁ be set ;
let c₂, c₃ be non empty set ;
let c₄ be Function of c₁,c₂;
let c₅ be Function of c₁,c₃;
redefine func <: as <:c₄,c₅:> -> Function of a₁,[:a₂,a₃:];
coherence by Th78;

end;

theorem Th79: :: FUNCT_3:79

for b₁, b₂, b₃ being non empty set
for b₄ being Function of b₁,b₂
for b₅ being Function of b₁,b₃
for b₆ being Element of b₁ holds <:b₄,b₅:> . b₆ = [(b₄ . b₆),(b₅ . b₆)]

proof end;

theorem Th80: :: FUNCT_3:80

for b₁, b₂, b₃ being set
for b₄ being Function of b₁,b₂
for b₅ being Function of b₁,b₃ holds rng <:b₄,b₅:> c= [:b₂,b₃:]

proof end;

theorem Th81: :: FUNCT_3:81

for b₁, b₂, b₃ being set
for b₄ being Function of b₁,b₂
for b₅ being Function of b₁,b₃ st ( b₂ = {} implies b₁ = {} ) & ( b₃ = {} implies b₁ = {} ) holds
( (pr1 b₂,b₃) * <:b₄,b₅:> = b₄ & (pr2 b₂,b₃) * <:b₄,b₅:> = b₅ )

proof end;

theorem Th82: :: FUNCT_3:82

for b₁ being set
for b₂, b₃ being non empty set
for b₄ being Function of b₁,b₂
for b₅ being Function of b₁,b₃ holds
( (pr1 b₂,b₃) * <:b₄,b₅:> = b₄ & (pr2 b₂,b₃) * <:b₄,b₅:> = b₅ ) by Th81;

theorem Th83: :: FUNCT_3:83

for b₁, b₂, b₃ being set
for b₄, b₅ being Function of b₁,b₂
for b₆, b₇ being Function of b₁,b₃ st ( b₂ = {} implies b₁ = {} ) & ( b₃ = {} implies b₁ = {} ) & <:b₄,b₆:> = <:b₅,b₇:> holds
( b₄ = b₅ & b₆ = b₇ )

proof end;

theorem Th84: :: FUNCT_3:84

for b₁ being set
for b₂, b₃ being non empty set
for b₄, b₅ being Function of b₁,b₂
for b₆, b₇ being Function of b₁,b₃ st <:b₄,b₆:> = <:b₅,b₇:> holds
( b₄ = b₅ & b₆ = b₇ )

proof end;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines [: FUNCT_3:def 9 :

theorem Th85: :: FUNCT_3:85

canceled;

theorem Th86: :: FUNCT_3:86

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

proof end;

theorem Th87: :: FUNCT_3:87

for b₁, b₂ being Function holds [:b₁,b₂:] = <:(b₁ * (pr1 (dom b₁),(dom b₂))),(b₂ * (pr2 (dom b₁),(dom b₂))):>

proof end;

theorem Th88: :: FUNCT_3:88

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

proof end;

theorem Th89: :: FUNCT_3:89

for b₁ being set
for b₂, b₃ being Function st dom b₂ = b₁ & dom b₃ = b₁ holds
<:b₂,b₃:> = [:b₂,b₃:] * (delta b₁)

proof end;

theorem Th90: :: FUNCT_3:90

for b₁, b₂ being set holds [:(id b₁),(id b₂):] = id [:b₁,b₂:]

proof end;

theorem Th91: :: FUNCT_3:91

for b₁, b₂, b₃, b₄ being Function holds [:b₁,b₃:] * <:b₂,b₄:> = <:(b₁ * b₂),(b₃ * b₄):>

proof end;

theorem Th92: :: FUNCT_3:92

for b₁, b₂, b₃, b₄ being Function holds [:b₁,b₃:] * [:b₂,b₄:] = [:(b₁ * b₂),(b₃ * b₄):]

proof end;

theorem Th93: :: FUNCT_3:93

for b₁, b₂ being set
for b₃, b₄ being Function holds [:b₃,b₄:] .: [:b₁,b₂:] = [:(b₃ .: b₁),(b₄ .: b₂):]

proof end;

theorem Th94: :: FUNCT_3:94

for b₁, b₂ being set
for b₃, b₄ being Function holds [:b₃,b₄:] " [:b₁,b₂:] = [:(b₃ " b₁),(b₄ " b₂):]

proof end;

theorem Th95: :: FUNCT_3:95

for b₁, b₂, b₃, b₄ being set
for b₅ being Function of b₁,b₂
for b₆ being Function of b₃,b₄ holds [:b₅,b₆:] is Function of [:b₁,b₃:],[:b₂,b₄:]

proof end;

definition

let c₁, c₂, c₃, c₄ be set ;
let c₅ be Function of c₁,c₃;
let c₆ be Function of c₂,c₄;
redefine func [: as [:c₅,c₆:] -> Function of [:a₁,a₂:],[:a₃,a₄:];
coherence by Th95;

end;

theorem Th96: :: FUNCT_3:96

for b₁, b₂, b₃, b₄ being non empty set
for b₅ being Function of b₁,b₂
for b₆ being Function of b₃,b₄
for b₇ being Element of b₁
for b₈ being Element of b₃ holds [:b₅,b₆:] . [b₇,b₈] = [(b₅ . b₇),(b₆ . b₈)]

proof end;

theorem Th97: :: FUNCT_3:97

for b₁, b₂, b₃, b₄ being set
for b₅ being Function of b₁,b₂
for b₆ being Function of b₃,b₄ st ( b₂ = {} implies b₁ = {} ) & ( b₄ = {} implies b₃ = {} ) holds
[:b₅,b₆:] = <:(b₅ * (pr1 b₁,b₃)),(b₆ * (pr2 b₁,b₃)):>

proof end;

theorem Th98: :: FUNCT_3:98

for b₁, b₂ being set
for b₃, b₄ being non empty set
for b₅ being Function of b₁,b₃
for b₆ being Function of b₂,b₄ holds [:b₅,b₆:] = <:(b₅ * (pr1 b₁,b₂)),(b₆ * (pr2 b₁,b₂)):>

proof end;

theorem Th99: :: FUNCT_3:99

for b₁, b₂, b₃ being set
for b₄ being Function of b₁,b₂
for b₅ being Function of b₁,b₃ holds <:b₄,b₅:> = [:b₄,b₅:] * (delta b₁)

proof end;

theorem Th100: :: FUNCT_3:100

for b₁ being Function holds (pr1 (dom b₁),(rng b₁)) .: b₁ = dom b₁

proof end;