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

:: Additional propositions about functions

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₁[ object , object , object ] } :

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

provided

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

proof end;

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

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

proof end;

:: Function indicated by the image under a function

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 Th7: :: FUNCT_3:7

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

proof end;

theorem :: FUNCT_3:8

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

proof end;

theorem Th9: :: FUNCT_3:9

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

proof end;

theorem :: FUNCT_3:10

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

proof end;

theorem Th11: :: FUNCT_3:11

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

proof end;

theorem :: FUNCT_3:12

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

proof end;

theorem Th13: :: FUNCT_3:13

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

proof end;

theorem Th14: :: FUNCT_3:14

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:15

for A, X 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 Th16: :: FUNCT_3:16

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

proof end;

theorem :: FUNCT_3:17

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:18

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

proof end;

theorem Th19: :: FUNCT_3:19

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

proof end;

theorem Th20: :: FUNCT_3:20

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 Th20;

end;

:: Function indicated by the inverse image under a function

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 Th21: :: FUNCT_3:21

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

proof end;

theorem Th22: :: FUNCT_3:22

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

proof end;

theorem :: FUNCT_3:23

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

proof end;

theorem :: FUNCT_3:24

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

proof end;

theorem Th25: :: FUNCT_3:25

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

proof end;

theorem :: FUNCT_3:26

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

proof end;

theorem Th27: :: FUNCT_3:27

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

proof end;

theorem :: FUNCT_3:28

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 Th29: :: FUNCT_3:29

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

proof end;

theorem :: FUNCT_3:30

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

proof end;

theorem Th31: :: FUNCT_3:31

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

proof end;

theorem Th32: :: FUNCT_3:32

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:33

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:34

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

proof end;

theorem :: FUNCT_3:35

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

proof end;

:: Characteristic function

definition

let A, X be set ;

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

existence
ex b₁ being Function st
( dom b₁ = X & ( for x being object st x in X holds
( ( x in A implies b₁ . x = 1 ) & ( not x in A implies b₁ . x = 0 ) ) ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = X & ( for x being object st x in X holds
( ( x in A implies b₁ . x = 1 ) & ( not x in A implies b₁ . x = 0 ) ) ) & dom b₂ = X & ( for x being object st x in X holds
( ( x in A implies b₂ . x = 1 ) & ( not x in A implies b₂ . x = 0 ) ) ) 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 object st x in X holds
( ( x in A implies b₃ . x = 1 ) & ( not x in A implies b₃ . x = 0 ) ) ) ) );

theorem Th36: :: FUNCT_3:36

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

proof end;

theorem :: FUNCT_3:37

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

proof end;

theorem :: FUNCT_3:38

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

proof end;

theorem Th39: :: FUNCT_3:39

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

proof end;

theorem :: FUNCT_3:40

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
chi (A,X) is Function of X,{0,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:41

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

theorem :: FUNCT_3:42

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

proof end;

:: Projections

definition

let X, Y be set ;

func pr1 (X,Y) -> Function means :Def4: :: FUNCT_3:def 4
( dom it = [:X,Y:] & ( for x, y being object 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 object 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 object st x in X & y in Y holds
b₁ . (x,y) = x ) & dom b₂ = [:X,Y:] & ( for x, y being object st x in X & y in Y holds
b₂ . (x,y) = x ) holds
b₁ = b₂

proof end;

func pr2 (X,Y) -> Function means :Def5: :: FUNCT_3:def 5
( dom it = [:X,Y:] & ( for x, y being object 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 object 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 object st x in X & y in Y holds
b₁ . (x,y) = y ) & dom b₂ = [:X,Y:] & ( for x, y being object st x in X & y in Y holds
b₂ . (x,y) = y ) holds
b₁ = b₂

proof end;

end;

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

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

theorem Th43: :: FUNCT_3:43

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

proof end;

theorem :: FUNCT_3:44

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

proof end;

theorem Th45: :: FUNCT_3:45

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

proof end;

theorem :: FUNCT_3:46

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 :Def6: :: FUNCT_3:def 6
( dom it = X & ( for x being object st x in X holds
it . x = [x,x] ) );

existence
ex b₁ being Function st
( dom b₁ = X & ( for x being object st x in X holds
b₁ . x = [x,x] ) )

proof end;

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

proof end;

end;

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

theorem Th47: :: FUNCT_3:47

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;

:: Complex functions

definition

let f, g be Function;

func <:f,g:> -> Function means :Def7: :: FUNCT_3:def 7
( dom it = (dom f) /\ (dom g) & ( for x being object 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 object 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 object st x in dom b₁ holds
b₁ . x = [(f . x),(g . x)] ) & dom b₂ = (dom f) /\ (dom g) & ( for x being object st x in dom b₂ holds
b₂ . x = [(f . x),(g . x)] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines <: FUNCT_3:def 7 :
for f, g, b₃ being Function holds
( b₃ = <:f,g:> iff ( dom b₃ = (dom f) /\ (dom g) & ( for x being object 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 Th48: :: FUNCT_3:48

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 Th49: :: FUNCT_3:49

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 Th50: :: FUNCT_3:50

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

proof end;

theorem Th51: :: FUNCT_3:51

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

proof end;

theorem Th52: :: FUNCT_3:52

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 Th53: :: FUNCT_3:53

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

proof end;

theorem Th54: :: FUNCT_3:54

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:55

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

proof end;

theorem :: FUNCT_3:56

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

proof end;

theorem :: FUNCT_3:57

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 Th58: :: FUNCT_3:58

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 Th58;

end;

theorem :: FUNCT_3:59

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:60

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 Th61: :: FUNCT_3:61

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:62

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 Th61;

theorem :: FUNCT_3:63

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:64

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;

:: Product-functions

definition

let f, g be Function;

func [:f,g:] -> Function means :Def8: :: FUNCT_3:def 8
( dom it = [:(dom f),(dom g):] & ( for x, y being object 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 object 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 object 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 object st x in dom f & y in dom g holds
b₂ . (x,y) = [(f . x),(g . y)] ) 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, y being object st x in dom f & y in dom g holds
b₃ . (x,y) = [(f . x),(g . y)] ) ) );

theorem Th65: :: FUNCT_3:65

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

proof end;

theorem Th66: :: FUNCT_3:66

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

proof end;

theorem Th67: :: FUNCT_3:67

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

proof end;

theorem Th68: :: FUNCT_3:68

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:69

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

proof end;

theorem :: FUNCT_3:70

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

proof end;

theorem :: FUNCT_3:71

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

proof end;

theorem :: FUNCT_3:72

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

proof end;

theorem :: FUNCT_3:73

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

proof end;

theorem Th74: :: FUNCT_3:74

for V, X, Y, 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 Th74;

end;

theorem Th75: :: FUNCT_3:75

for C1, C2, D1, 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:76

for X1, X2, Y1, 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:77

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:78

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;

:: from AMI_1

theorem :: FUNCT_3:79

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

proof end;

theorem :: FUNCT_3:80

for A, B, C being non empty set
for f, g being Function of A,[:B,C:] st (pr1 (B,C)) * f = (pr1 (B,C)) * g & (pr2 (B,C)) * f = (pr2 (B,C)) * g holds
f = g

proof end;

registration

let F, G be one-to-one Function;

cluster [:F,G:] -> one-to-one ;

coherence
[:F,G:] is one-to-one

proof end;

end;

registration

let A be set ;

cluster Relation-like [:A,A:] -defined A -valued Function-like quasi_total idempotent for Element of bool [:[:A,A:],A:];

existence
ex b₁ being BinOp of A st b₁ is idempotent

proof end;

end;

registration

let A be set ;
let b be idempotent BinOp of A;
let a be Element of A;

reduce b . (a,a) to a;

reducibility
b . (a,a) = a by BINOP_1:def 4;

end;

definition

let A1 be set ;
let B1 be non empty set ;
let f be Function of A1,B1;
let Y1 be Subset of A1;
:: original: |
redefine func f | Y1 -> Function of Y1,B1;
coherence
f | Y1 is Function of Y1,B1 by FUNCT_2:32;

end;

theorem :: FUNCT_3:81

for A1, A2, B1, B2 being non empty set
for f being Function of A1,B1
for g being Function of A2,B2
for Y1 being non empty Subset of A1
for Y2 being non empty Subset of A2 holds [:f,g:] | [:Y1,Y2:] = [:(f | Y1),(g | Y2):]

proof end;