:: 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{ F1() -> set , F2() -> set , P1[ object , object , object ] } :
ex f being Function st
( dom f = [:F1(),F2():] & ( for x, y being object st x in F1() & y in F2() holds
P1[x,y,f . (x,y)] ) )
provided
A1: for x, y, z1, z2 being object st x in F1() & y in F2() & P1[x,y,z1] & P1[x,y,z2] holds
z1 = z2 and
A2: for x, y being object st x in F1() & y in F2() holds
ex z being object st P1[x,y,z]
proof end;

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

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

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

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

:: deftheorem Def7 defines <: FUNCT_3:def 7 :
for f, g, b3 being Function holds
( b3 = <:f,g:> iff ( dom b3 = (dom f) /\ (dom g) & ( for x being object 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 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 b1 being Function st
( dom b1 = [:(dom f),(dom g):] & ( for x, y being object 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 object 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 object st x in dom f & y in dom g holds
b2 . (x,y) = [(f . x),(g . y)] ) 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, y being object st x in dom f & y in dom g holds
b3 . (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 b1 being BinOp of A st b1 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;