:: Basic Functions and Operations on Functions
:: by Czes{\l}aw Byli\'nski
::
:: Received May 9, 1989
:: Copyright (c) 1990 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{ F1() -> set , F2() -> set , P1[ set , set , set ] } :
ex f being Function st
( dom f = [:F1(),F2():] & ( for x, y being set st x in F1() & y in F2() holds
P1[x,y,f . (x,y)] ) )
provided
A1: for x, y, z1, z2 being set st x in F1() & y in F2() & P1[x,y,z1] & P1[x,y,z2] holds
z1 = z2 and
A2: for x, y being set st x in F1() & y in F2() holds
ex z being set st P1[x,y,z]
proof end;

scheme :: FUNCT_3:sch 2
Lambda3{ F1() -> set , F2() -> set , F3( set , set ) -> set } :
ex f being Function st
( dom f = [:F1(),F2():] & ( for x, y being set st x in F1() & y in F2() holds
f . (x,y) = F3(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 b1 being Function st
( dom b1 = bool (dom f) & ( for X being set st X c= dom f holds
b1 . X = f .: X ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = bool (dom f) & ( for X being set st X c= dom f holds
b1 . X = f .: X ) & dom b2 = bool (dom f) & ( for X being set st X c= dom f holds
b2 . X = f .: X ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines .: FUNCT_3:def 1 :
for f, b2 being Function holds
( b2 = .: f iff ( dom b2 = bool (dom f) & ( for X being set st X c= dom f holds
b2 . 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 b1 being Function st
( dom b1 = bool (rng f) & ( for Y being set st Y c= rng f holds
b1 . Y = f " Y ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = bool (rng f) & ( for Y being set st Y c= rng f holds
b1 . Y = f " Y ) & dom b2 = bool (rng f) & ( for Y being set st Y c= rng f holds
b2 . Y = f " Y ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines " FUNCT_3:def 2 :
for f, b2 being Function holds
( b2 = " f iff ( dom b2 = bool (rng f) & ( for Y being set st Y c= rng f holds
b2 . 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 b1 being Function st
( dom b1 = X & ( for x being set st x in X holds
( ( x in A implies b1 . x = 1 ) & ( not x in A implies b1 . x = {} ) ) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = X & ( for x being set st x in X holds
( ( x in A implies b1 . x = 1 ) & ( not x in A implies b1 . x = {} ) ) ) & dom b2 = X & ( for x being set st x in X holds
( ( x in A implies b2 . x = 1 ) & ( not x in A implies b2 . x = {} ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines chi FUNCT_3:def 3 :
for A, X being set
for b3 being Function holds
( b3 = chi (A,X) iff ( dom b3 = X & ( for x being set st x in X holds
( ( x in A implies b3 . x = 1 ) & ( not x in A implies b3 . 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 b1 being Function st
( dom b1 = [:X,Y:] & ( for x, y being set st x in X & y in Y holds
b1 . (x,y) = x ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = [:X,Y:] & ( for x, y being set st x in X & y in Y holds
b1 . (x,y) = x ) & dom b2 = [:X,Y:] & ( for x, y being set st x in X & y in Y holds
b2 . (x,y) = x ) holds
b1 = b2
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 b1 being Function st
( dom b1 = [:X,Y:] & ( for x, y being set st x in X & y in Y holds
b1 . (x,y) = y ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = [:X,Y:] & ( for x, y being set st x in X & y in Y holds
b1 . (x,y) = y ) & dom b2 = [:X,Y:] & ( for x, y being set st x in X & y in Y holds
b2 . (x,y) = y ) holds
b1 = b2
proof end;
end;

:: deftheorem FUNCT_3:def 4 :
canceled;

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

:: deftheorem Def6 defines pr2 FUNCT_3:def 6 :
for X, Y being set
for b3 being Function holds
( b3 = pr2 (X,Y) iff ( dom b3 = [:X,Y:] & ( for x, y being set st x in X & y in Y holds
b3 . (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 b1 being Function st
( dom b1 = X & ( for x being set st x in X holds
b1 . x = [x,x] ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = X & ( for x being set st x in X holds
b1 . x = [x,x] ) & dom b2 = X & ( for x being set st x in X holds
b2 . x = [x,x] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines delta FUNCT_3:def 7 :
for X being set
for b2 being Function holds
( b2 = delta X iff ( dom b2 = X & ( for x being set st x in X holds
b2 . 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 b1 being Function st
( dom b1 = (dom f) /\ (dom g) & ( for x being set st x in dom b1 holds
b1 . x = [(f . x),(g . x)] ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = (dom f) /\ (dom g) & ( for x being set st x in dom b1 holds
b1 . x = [(f . x),(g . x)] ) & dom b2 = (dom f) /\ (dom g) & ( for x being set st x in dom b2 holds
b2 . x = [(f . x),(g . x)] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines <: FUNCT_3:def 8 :
for f, g, b3 being Function holds
( b3 = <:f,g:> iff ( dom b3 = (dom f) /\ (dom g) & ( for x being set st x in dom b3 holds
b3 . 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 b1 being Function st
( dom b1 = [:(dom f),(dom g):] & ( for x, y being set st x in dom f & y in dom g holds
b1 . (x,y) = [(f . x),(g . y)] ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = [:(dom f),(dom g):] & ( for x, y being set st x in dom f & y in dom g holds
b1 . (x,y) = [(f . x),(g . y)] ) & dom b2 = [:(dom f),(dom g):] & ( for x, y being set st x in dom f & y in dom g holds
b2 . (x,y) = [(f . x),(g . y)] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines [: FUNCT_3:def 9 :
for f, g, b3 being Function holds
( b3 = [:f,g:] iff ( dom b3 = [:(dom f),(dom g):] & ( for x, y being set st x in dom f & y in dom g holds
b3 . (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;