:: Basic Functions and Operations on Functions
:: by Czes{\l}aw Byli\'nski
::
:: Received May 9, 1989
:: Copyright (c) 1990-2011 Association of Mizar Users

begin

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
ex b₁ being Function st
( dom b₁ = bool (dom f) & ( for X being set st X c= dom f holds
b₁ . X = f .: X ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = bool (dom f) & ( for X being set st X c= dom f holds
b₁ . X = f .: X ) & dom b₂ = bool (dom f) & ( for X being set st X c= dom f holds
b₂ . X = f .: X ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines .: FUNCT_3:def 1 :
for f, b₂ being Function holds
( b₂ = .: f iff ( dom b₂ = bool (dom f) & ( for X being set st X c= dom f holds
b₂ . X = f .: X ) ) );

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
.: f is Function of (bool X),(bool D) 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
ex b₁ being Function st
( dom b₁ = bool (rng f) & ( for Y being set st Y c= rng f holds
b₁ . Y = f " Y ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = bool (rng f) & ( for Y being set st Y c= rng f holds
b₁ . Y = f " Y ) & dom b₂ = bool (rng f) & ( for Y being set st Y c= rng f holds
b₂ . Y = f " Y ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines " FUNCT_3:def 2 :
for f, b₂ being Function holds
( b₂ = " f iff ( dom b₂ = bool (rng f) & ( for Y being set st Y c= rng f holds
b₂ . Y = f " Y ) ) );

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 = {} ) ) ) );
existence
ex b₁ being Function st
( dom b₁ = X & ( for x being set st x in X holds
( ( x in A implies b₁ . x = 1 ) & ( not x in A implies b₁ . x = {} ) ) ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = X & ( for x being set st x in X holds
( ( x in A implies b₁ . x = 1 ) & ( not x in A implies b₁ . x = {} ) ) ) & dom b₂ = X & ( for x being set st x in X holds
( ( x in A implies b₂ . x = 1 ) & ( not x in A implies b₂ . x = {} ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines chi FUNCT_3:def 3 :
for A, X being set
for b₃ being Function holds
( b₃ = chi (A,X) iff ( dom b₃ = X & ( for x being set st x in X holds
( ( x in A implies b₃ . x = 1 ) & ( not x in A implies b₃ . x = {} ) ) ) ) );

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 = {}

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= {{},1}

proof end;

theorem :: FUNCT_3:49

for X being set
for f being Function of X,{{},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,{{},1};
coherence
chi (A,X) is Function of X,{{},1}

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
incl is Function of A,Y

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
ex b₁ being Function st
( dom b₁ = [:X,Y:] & ( for x, y being set st x in X & y in Y holds
b₁ . (x,y) = x ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = [:X,Y:] & ( for x, y being set st x in X & y in Y holds
b₁ . (x,y) = x ) & dom b₂ = [:X,Y:] & ( for x, y being set st x in X & y in Y holds
b₂ . (x,y) = x ) holds
b₁ = b₂

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
ex b₁ being Function st
( dom b₁ = [:X,Y:] & ( for x, y being set st x in X & y in Y holds
b₁ . (x,y) = y ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = [:X,Y:] & ( for x, y being set st x in X & y in Y holds
b₁ . (x,y) = y ) & dom b₂ = [:X,Y:] & ( for x, y being set st x in X & y in Y holds
b₂ . (x,y) = y ) holds
b₁ = b₂

proof end;

end;

:: deftheorem FUNCT_3:def 4 :
canceled;

:: deftheorem Def5 defines pr1 FUNCT_3:def 5 :
for X, Y being set
for b₃ being Function holds
( b₃ = pr1 (X,Y) iff ( dom b₃ = [:X,Y:] & ( for x, y being set st x in X & y in Y holds
b₃ . (x,y) = x ) ) );

:: deftheorem Def6 defines pr2 FUNCT_3:def 6 :
for X, Y being set
for b₃ being Function holds
( b₃ = pr2 (X,Y) iff ( dom b₃ = [:X,Y:] & ( for x, y being set st x in X & y in Y holds
b₃ . (x,y) = y ) ) );

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
pr1 (X,Y) is Function of [:X,Y:],X

proof end;

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

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
ex b₁ being Function st
( dom b₁ = X & ( for x being set st x in X holds
b₁ . x = [x,x] ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = X & ( for x being set st x in X holds
b₁ . x = [x,x] ) & dom b₂ = X & ( for x being set st x in X holds
b₂ . x = [x,x] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines delta FUNCT_3:def 7 :
for X being set
for b₂ being Function holds
( b₂ = delta X iff ( dom b₂ = X & ( for x being set st x in X holds
b₂ . x = [x,x] ) ) );

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
delta X is Function of X,[:X,X:]

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
ex b₁ being Function st
( dom b₁ = (dom f) /\ (dom g) & ( for x being set st x in dom b₁ holds
b₁ . x = [(f . x),(g . x)] ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = (dom f) /\ (dom g) & ( for x being set st x in dom b₁ holds
b₁ . x = [(f . x),(g . x)] ) & dom b₂ = (dom f) /\ (dom g) & ( for x being set st x in dom b₂ holds
b₂ . x = [(f . x),(g . x)] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines <: FUNCT_3:def 8 :
for f, g, b₃ being Function holds
( b₃ = <:f,g:> iff ( dom b₃ = (dom f) /\ (dom g) & ( for x being set st x in dom b₃ holds
b₃ . x = [(f . x),(g . x)] ) ) );

registration

let f be empty Function;
let g be Function;
cluster <:f,g:> -> empty ;
coherence
<:f,g:> is empty

proof end;

cluster <:g,f:> -> empty ;
coherence
<:g,f:> is empty

proof end;

end;

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
<:f1,f2:> is Function of X,[:D1,D2:] 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
ex b₁ being Function st
( dom b₁ = [:(dom f),(dom g):] & ( for x, y being set st x in dom f & y in dom g holds
b₁ . (x,y) = [(f . x),(g . y)] ) )

proof end;

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

proof end;

end;

:: deftheorem Def9 defines [: FUNCT_3:def 9 :
for f, g, b₃ being Function holds
( b₃ = [:f,g:] iff ( dom b₃ = [:(dom f),(dom g):] & ( for x, y being set st x in dom f & y in dom g holds
b₃ . (x,y) = [(f . x),(g . y)] ) ) );

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
[:f1,f2:] is Function of [:X1,X2:],[:Y1,Y2:] 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;

begin

theorem :: FUNCT_3:100

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

proof end;