:: FUNCT_3 semantic presentation

theorem Th1: :: FUNCT_3:1

for A, Y being set st A c= Y holds
id A = (id Y) | A

proof end;

theorem Th2: :: FUNCT_3:2

for X being set
for f, g being Function st X c= dom (g * f) holds
f .: X c= dom g

proof end;

theorem Th3: :: FUNCT_3:3

for X being set
for f, g being Function st X c= dom f & f .: X c= dom g holds
X c= dom (g * f)

proof end;

theorem Th4: :: FUNCT_3:4

for Y being set
for f, g being Function st Y c= rng (g * f) & g is one-to-one holds
g " Y c= rng f

proof end;

theorem Th5: :: FUNCT_3:5

for Y being set
for f, g being Function st Y c= rng g & g " Y c= rng f holds
Y c= rng (g * f)

proof end;

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

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

provided

A1: for x, y, z1, z2 being set st x in F₁() & y in F₂() & P₁[x,y,z1] & P₁[x,y,z2] holds
z1 = z2 and
A2: for x, y being set st x in F₁() & y in F₂() holds
ex z being set st P₁[x,y,z]

proof end;

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

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

proof end;

theorem Th6: :: FUNCT_3:6

for X, Y being set
for f, g being Function st dom f = [:X,Y:] & dom g = [:X,Y:] & ( for x, y being set st x in X & y in Y holds
f . [x,y] = g . [x,y] ) holds
f = g

proof end;

definition

let f be Function;
func .: f -> Function means :Def1: :: FUNCT_3:def 1
( dom it = bool (dom f) & ( for X being set st X c= dom f holds
it . X = f .: X ) );
existence

proof end;

uniqueness

proof end;

end;

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

theorem :: FUNCT_3:7

canceled;

theorem Th8: :: FUNCT_3:8

for X being set
for f being Function st X in dom (.: f) holds
(.: f) . X = f .: X

proof end;

theorem :: FUNCT_3:9

for f being Function holds (.: f) . {} = {}

proof end;

theorem Th10: :: FUNCT_3:10

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

proof end;

theorem :: FUNCT_3:11

canceled;

theorem :: FUNCT_3:12

for A being set
for f being Function holds (.: f) .: A c= bool (rng f)

proof end;

theorem Th13: :: FUNCT_3:13

for B being set
for f being Function holds (.: f) " B c= bool (dom f)

proof end;

theorem :: FUNCT_3:14

for X, B being set
for D being non empty set
for f being Function of X,D holds (.: f) " B c= bool X

proof end;

theorem Th15: :: FUNCT_3:15

for A being set
for f being Function holds union ((.: f) .: A) c= f .: (union A)

proof end;

theorem Th16: :: FUNCT_3:16

for A being set
for f being Function st A c= bool (dom f) holds
f .: (union A) = union ((.: f) .: A)

proof end;

theorem :: FUNCT_3:17

for X, A being set
for D being non empty set
for f being Function of X,D st A c= bool X holds
f .: (union A) = union ((.: f) .: A)

proof end;

theorem Th18: :: FUNCT_3:18

for B being set
for f being Function holds union ((.: f) " B) c= f " (union B)

proof end;

theorem :: FUNCT_3:19

for B being set
for f being Function st B c= bool (rng f) holds
f " (union B) = union ((.: f) " B)

proof end;

theorem :: FUNCT_3:20

for f, g being Function holds .: (g * f) = (.: g) * (.: f)

proof end;

theorem Th21: :: FUNCT_3:21

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

proof end;

theorem Th22: :: FUNCT_3:22

for X, Y being set
for f being Function of X,Y st ( Y = {} implies X = {} ) holds
.: f is Function of bool X, bool Y

proof end;

definition

let X be set ;
let D be non empty set ;
let f be Function of X,D;
:: original: .:
redefine func .: f -> Function of bool X, bool D;
coherence by Th22;

end;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines " FUNCT_3:def 2 :

theorem :: FUNCT_3:23

canceled;

theorem Th24: :: FUNCT_3:24

for Y being set
for f being Function st Y in dom (" f) holds
(" f) . Y = f " Y

proof end;

theorem Th25: :: FUNCT_3:25

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

proof end;

theorem :: FUNCT_3:26

canceled;

theorem :: FUNCT_3:27

for B being set
for f being Function holds (" f) .: B c= bool (dom f)

proof end;

theorem :: FUNCT_3:28

for A being set
for f being Function holds (" f) " A c= bool (rng f)

proof end;

theorem Th29: :: FUNCT_3:29

for B being set
for f being Function holds union ((" f) .: B) c= f " (union B)

proof end;

theorem :: FUNCT_3:30

for B being set
for f being Function st B c= bool (rng f) holds
union ((" f) .: B) = f " (union B)

proof end;

theorem Th31: :: FUNCT_3:31

for A being set
for f being Function holds union ((" f) " A) c= f .: (union A)

proof end;

theorem :: FUNCT_3:32

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

proof end;

theorem Th33: :: FUNCT_3:33

for B being set
for f being Function holds (" f) .: B c= (.: f) " B

proof end;

theorem :: FUNCT_3:34

for B being set
for f being Function st f is one-to-one holds
(" f) .: B = (.: f) " B

proof end;

theorem Th35: :: FUNCT_3:35

for f being Function
for A being set st A c= bool (dom f) holds
(" f) " A c= (.: f) .: A

proof end;

theorem Th36: :: FUNCT_3:36

for f being Function
for A being set st f is one-to-one holds
(.: f) .: A c= (" f) " A

proof end;

theorem :: FUNCT_3:37

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

proof end;

theorem :: FUNCT_3:38

for f, g being Function st g is one-to-one holds
" (g * f) = (" f) * (" g)

proof end;

theorem :: FUNCT_3:39

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

proof end;

definition

let A, X be set ;
func chi A,X -> Function means :Def3: :: FUNCT_3:def 3
( dom it = X & ( for x being set st x in X holds
( ( x in A implies it . x = 1 ) & ( not x in A implies it . x = 0 ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines chi FUNCT_3:def 3 :

theorem :: FUNCT_3:40

canceled;

theorem :: FUNCT_3:41

canceled;

theorem Th42: :: FUNCT_3:42

for x, A, X being set st (chi A,X) . x = 1 holds
x in A

proof end;

theorem :: FUNCT_3:43

for x, X, A being set st x in X \ A holds
(chi A,X) . x = 0

proof end;

theorem :: FUNCT_3:44

canceled;

theorem :: FUNCT_3:45

canceled;

theorem :: FUNCT_3:46

canceled;

theorem :: FUNCT_3:47

for A, X, B being set st A c= X & B c= X & chi A,X = chi B,X holds
A = B

proof end;

theorem Th48: :: FUNCT_3:48

for A, X being set holds rng (chi A,X) c= {0,1}

proof end;

theorem :: FUNCT_3:49

for X being set
for f being Function of X,{0,1} holds f = chi (f " {1}),X

proof end;

definition

let A, X be set ;
:: original: chi
redefine func chi A,X -> Function of X,{0,1};
coherence

proof end;

end;

notation

let Y be set ;
let A be Subset of Y;
synonym incl A for id Y;

end;

definition

let Y be set ;
let A be Subset of Y;
:: original: incl
redefine func incl A -> Function of A,Y;
coherence

proof end;

end;

theorem :: FUNCT_3:50

canceled;

theorem :: FUNCT_3:51

canceled;

theorem :: FUNCT_3:52

canceled;

theorem :: FUNCT_3:53

for Y being set
for A being Subset of Y holds incl A = (id Y) | A by Th1;

theorem :: FUNCT_3:54

canceled;

theorem :: FUNCT_3:55

canceled;

theorem :: FUNCT_3:56

for x, Y being set
for A being Subset of Y st x in A holds
(incl A) . x in Y

proof end;

definition

let X, Y be set ;
canceled;
func pr1 X,Y -> Function means :Def5: :: FUNCT_3:def 5
( dom it = [:X,Y:] & ( for x, y being set st x in X & y in Y holds
it . [x,y] = x ) );
existence

proof end;

uniqueness

proof end;

func pr2 X,Y -> Function means :Def6: :: FUNCT_3:def 6
( dom it = [:X,Y:] & ( for x, y being set st x in X & y in Y holds
it . [x,y] = y ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem FUNCT_3:def 4 :

:: deftheorem Def5 defines pr1 FUNCT_3:def 5 :

:: deftheorem Def6 defines pr2 FUNCT_3:def 6 :

theorem :: FUNCT_3:57

canceled;

theorem :: FUNCT_3:58

canceled;

theorem Th59: :: FUNCT_3:59

for X, Y being set holds rng (pr1 X,Y) c= X

proof end;

theorem :: FUNCT_3:60

for Y, X being set st Y <> {} holds
rng (pr1 X,Y) = X

proof end;

theorem Th61: :: FUNCT_3:61

for X, Y being set holds rng (pr2 X,Y) c= Y

proof end;

theorem :: FUNCT_3:62

for X, Y being set st X <> {} holds
rng (pr2 X,Y) = Y

proof end;

definition

let X, Y be set ;
:: original: pr1
redefine func pr1 X,Y -> Function of [:X,Y:],X;
coherence

proof end;

:: original: pr2
redefine func pr2 X,Y -> Function of [:X,Y:],Y;
coherence

proof end;

end;

definition

let X be set ;
func delta X -> Function means :Def7: :: FUNCT_3:def 7
( dom it = X & ( for x being set st x in X holds
it . x = [x,x] ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines delta FUNCT_3:def 7 :

theorem :: FUNCT_3:63

canceled;

theorem :: FUNCT_3:64

canceled;

theorem :: FUNCT_3:65

canceled;

theorem Th66: :: FUNCT_3:66

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

proof end;

definition

let X be set ;
:: original: delta
redefine func delta X -> Function of X,[:X,X:];
coherence

proof end;

end;

definition

let f, g be Function;
func <:f,g:> -> Function means :Def8: :: FUNCT_3:def 8
( dom it = (dom f) /\ (dom g) & ( for x being set st x in dom it holds
it . x = [(f . x),(g . x)] ) );
existence

proof end;

uniqueness

proof end;

end;

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

theorem :: FUNCT_3:67

canceled;

theorem Th68: :: FUNCT_3:68

for x being set
for f, g being Function st x in (dom f) /\ (dom g) holds
<:f,g:> . x = [(f . x),(g . x)]

proof end;

theorem Th69: :: FUNCT_3:69

for x, X being set
for f, g being Function st dom f = X & dom g = X & x in X holds
<:f,g:> . x = [(f . x),(g . x)]

proof end;

theorem Th70: :: FUNCT_3:70

for X being set
for f, g being Function st dom f = X & dom g = X holds
dom <:f,g:> = X

proof end;

theorem Th71: :: FUNCT_3:71

for f, g being Function holds rng <:f,g:> c= [:(rng f),(rng g):]

proof end;

theorem Th72: :: FUNCT_3:72

for Y, Z being set
for f, g being Function st dom f = dom g & rng f c= Y & rng g c= Z holds
( (pr1 Y,Z) * <:f,g:> = f & (pr2 Y,Z) * <:f,g:> = g )

proof end;

theorem Th73: :: FUNCT_3:73

for X, Y being set holds <:(pr1 X,Y),(pr2 X,Y):> = id [:X,Y:]

proof end;

theorem Th74: :: FUNCT_3:74

for f, g, h, k being Function st dom f = dom g & dom k = dom h & <:f,g:> = <:k,h:> holds
( f = k & g = h )

proof end;

theorem :: FUNCT_3:75

for f, g, h being Function holds <:(f * h),(g * h):> = <:f,g:> * h

proof end;

theorem :: FUNCT_3:76

for A being set
for f, g being Function holds <:f,g:> .: A c= [:(f .: A),(g .: A):]

proof end;

theorem :: FUNCT_3:77

for B being set
for C being non empty set
for f, g being Function holds <:f,g:> " [:B,C:] = (f " B) /\ (g " C)

proof end;

theorem Th78: :: FUNCT_3:78

for X, Y, Z being set
for f being Function of X,Y
for g being Function of X,Z st ( Y = {} implies X = {} ) & ( Z = {} implies X = {} ) holds
<:f,g:> is Function of X,[:Y,Z:]

proof end;

definition

let X be set ;
let D1, D2 be non empty set ;
let f1 be Function of X,D1;
let f2 be Function of X,D2;
:: original: <:
redefine func <:f1,f2:> -> Function of X,[:D1,D2:];
coherence by Th78;

end;

theorem :: FUNCT_3:79

for C, D1, D2 being non empty set
for f1 being Function of C,D1
for f2 being Function of C,D2
for c being Element of C holds <:f1,f2:> . c = [(f1 . c),(f2 . c)]

proof end;

theorem :: FUNCT_3:80

for X, Y, Z being set
for f being Function of X,Y
for g being Function of X,Z holds rng <:f,g:> c= [:Y,Z:]

proof end;

theorem Th81: :: FUNCT_3:81

for X, Y, Z being set
for f being Function of X,Y
for g being Function of X,Z st ( Y = {} implies X = {} ) & ( Z = {} implies X = {} ) holds
( (pr1 Y,Z) * <:f,g:> = f & (pr2 Y,Z) * <:f,g:> = g )

proof end;

theorem :: FUNCT_3:82

for X being set
for D1, D2 being non empty set
for f being Function of X,D1
for g being Function of X,D2 holds
( (pr1 D1,D2) * <:f,g:> = f & (pr2 D1,D2) * <:f,g:> = g ) by Th81;

theorem :: FUNCT_3:83

for X, Y, Z being set
for f1, f2 being Function of X,Y
for g1, g2 being Function of X,Z st ( Y = {} implies X = {} ) & ( Z = {} implies X = {} ) & <:f1,g1:> = <:f2,g2:> holds
( f1 = f2 & g1 = g2 )

proof end;

theorem :: FUNCT_3:84

for X being set
for D1, D2 being non empty set
for f1, f2 being Function of X,D1
for g1, g2 being Function of X,D2 st <:f1,g1:> = <:f2,g2:> holds
( f1 = f2 & g1 = g2 )

proof end;

definition

let f, g be Function;
func [:f,g:] -> Function means :Def9: :: FUNCT_3:def 9
( dom it = [:(dom f),(dom g):] & ( for x, y being set st x in dom f & y in dom g holds
it . [x,y] = [(f . x),(g . y)] ) );
existence

proof end;

uniqueness

proof end;

end;

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

theorem :: FUNCT_3:85

canceled;

theorem Th86: :: FUNCT_3:86

for f, g being Function
for x, y being set st [x,y] in [:(dom f),(dom g):] holds
[:f,g:] . [x,y] = [(f . x),(g . y)]

proof end;

theorem Th87: :: FUNCT_3:87

for f, g being Function holds [:f,g:] = <:(f * (pr1 (dom f),(dom g))),(g * (pr2 (dom f),(dom g))):>

proof end;

theorem Th88: :: FUNCT_3:88

for f, g being Function holds rng [:f,g:] = [:(rng f),(rng g):]

proof end;

theorem Th89: :: FUNCT_3:89

for X being set
for f, g being Function st dom f = X & dom g = X holds
<:f,g:> = [:f,g:] * (delta X)

proof end;

theorem :: FUNCT_3:90

for X, Y being set holds [:(id X),(id Y):] = id [:X,Y:]

proof end;

theorem :: FUNCT_3:91

for f, g, h, k being Function holds [:f,h:] * <:g,k:> = <:(f * g),(h * k):>

proof end;

theorem :: FUNCT_3:92

for f, g, h, k being Function holds [:f,h:] * [:g,k:] = [:(f * g),(h * k):]

proof end;

theorem :: FUNCT_3:93

for B, A being set
for f, g being Function holds [:f,g:] .: [:B,A:] = [:(f .: B),(g .: A):]

proof end;

theorem :: FUNCT_3:94

for B, A being set
for f, g being Function holds [:f,g:] " [:B,A:] = [:(f " B),(g " A):]

proof end;

theorem Th95: :: FUNCT_3:95

for X, Y, V, Z being set
for f being Function of X,Y
for g being Function of V,Z holds [:f,g:] is Function of [:X,V:],[:Y,Z:]

proof end;

definition

let X1, X2, Y1, Y2 be set ;
let f1 be Function of X1,Y1;
let f2 be Function of X2,Y2;
:: original: [:
redefine func [:f1,f2:] -> Function of [:X1,X2:],[:Y1,Y2:];
coherence by Th95;

end;

theorem :: FUNCT_3:96

for C1, D1, C2, D2 being non empty set
for f1 being Function of C1,D1
for f2 being Function of C2,D2
for c1 being Element of C1
for c2 being Element of C2 holds [:f1,f2:] . [c1,c2] = [(f1 . c1),(f2 . c2)]

proof end;

theorem :: FUNCT_3:97

for X1, Y1, X2, Y2 being set
for f1 being Function of X1,Y1
for f2 being Function of X2,Y2 st ( Y1 = {} implies X1 = {} ) & ( Y2 = {} implies X2 = {} ) holds
[:f1,f2:] = <:(f1 * (pr1 X1,X2)),(f2 * (pr2 X1,X2)):>

proof end;

theorem :: FUNCT_3:98

for X1, X2 being set
for D1, D2 being non empty set
for f1 being Function of X1,D1
for f2 being Function of X2,D2 holds [:f1,f2:] = <:(f1 * (pr1 X1,X2)),(f2 * (pr2 X1,X2)):>

proof end;

theorem :: FUNCT_3:99

for X, Y1, Y2 being set
for f1 being Function of X,Y1
for f2 being Function of X,Y2 holds <:f1,f2:> = [:f1,f2:] * (delta X)

proof end;

theorem :: FUNCT_3:100

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

proof end;