:: The Modification of a Function by a Function and the Iteration of the Composition of a Function
:: by Czes{\l}aw Byli\'nski
::
:: Received March 1, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users

Lm1: for x, y, x1, y1, x9, y9, x19, y19 being object st [[x,x9],[y,y9]] = [[x1,x19],[y1,y19]] holds
( x = x1 & y = y1 & x9 = x19 & y9 = y19 )

proof end;

theorem Th1: :: FUNCT_4:1

for Z being set st ( for z being object st z in Z holds
ex x, y being object st z = [x,y] ) holds
ex X, Y being set st Z c= [:X,Y:]

proof end;

theorem :: FUNCT_4:2

for f, g being Function holds g * f = (g | (rng f)) * f

proof end;

theorem :: FUNCT_4:3

for X, Y being set holds
( id X c= id Y iff X c= Y )

proof end;

theorem :: FUNCT_4:4

for a being object
for X, Y being set st X c= Y holds
X --> a c= Y --> a

proof end;

theorem Th5: :: FUNCT_4:5

for X, Y being set
for a, b being object st X --> a c= Y --> b holds
X c= Y

proof end;

theorem :: FUNCT_4:6

for X, Y being set
for a, b being object st X <> {} & X --> a c= Y --> b holds
a = b

proof end;

theorem :: FUNCT_4:7

for x being object
for f being Function st x in dom f holds
x .--> (f . x) c= f

proof end;

:: Natural order on functions

theorem :: FUNCT_4:8

for X, Y being set
for f being Function holds (Y |` f) | X c= f

proof end;

theorem :: FUNCT_4:9

for X, Y being set
for f, g being Function st f c= g holds
(Y |` f) | X c= (Y |` g) | X

proof end;

definition

let f, g be Function;

func f +* g -> Function means :Def1: :: FUNCT_4:def 1
( dom it = (dom f) \/ (dom g) & ( for x being object st x in (dom f) \/ (dom g) holds
( ( x in dom g implies it . x = g . x ) & ( not x in dom g implies it . x = f . x ) ) ) );

existence
ex b₁ being Function st
( dom b₁ = (dom f) \/ (dom g) & ( for x being object st x in (dom f) \/ (dom g) holds
( ( x in dom g implies b₁ . x = g . x ) & ( not x in dom g implies b₁ . x = f . x ) ) ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = (dom f) \/ (dom g) & ( for x being object st x in (dom f) \/ (dom g) holds
( ( x in dom g implies b₁ . x = g . x ) & ( not x in dom g implies b₁ . x = f . x ) ) ) & dom b₂ = (dom f) \/ (dom g) & ( for x being object st x in (dom f) \/ (dom g) holds
( ( x in dom g implies b₂ . x = g . x ) & ( not x in dom g implies b₂ . x = f . x ) ) ) holds
b₁ = b₂

proof end;

idempotence
for f being Function holds
( dom f = (dom f) \/ (dom f) & ( for x being object st x in (dom f) \/ (dom f) holds
( ( x in dom f implies f . x = f . x ) & ( not x in dom f implies f . x = f . x ) ) ) ) ;

end;

:: deftheorem Def1 defines +* FUNCT_4:def 1 :
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 f) \/ (dom g) holds
( ( x in dom g implies b₃ . x = g . x ) & ( not x in dom g implies b₃ . x = f . x ) ) ) ) );

theorem Th10: :: FUNCT_4:10

for f, g being Function holds
( dom f c= dom (f +* g) & dom g c= dom (f +* g) )

proof end;

theorem Th11: :: FUNCT_4:11

for f, g being Function
for x being object st not x in dom g holds
(f +* g) . x = f . x

proof end;

theorem Th12: :: FUNCT_4:12

for f, g being Function
for x being object holds
( x in dom (f +* g) iff ( x in dom f or x in dom g ) )

proof end;

theorem Th13: :: FUNCT_4:13

for f, g being Function
for x being object st x in dom g holds
(f +* g) . x = g . x

proof end;

theorem Th14: :: FUNCT_4:14

for f, g, h being Function holds (f +* g) +* h = f +* (g +* h)

proof end;

theorem Th15: :: FUNCT_4:15

for x being object
for f, g being Function st f tolerates g & x in dom f holds
(f +* g) . x = f . x

proof end;

theorem :: FUNCT_4:16

for x being object
for f, g being Function st dom f misses dom g & x in dom f holds
(f +* g) . x = f . x

proof end;

theorem Th17: :: FUNCT_4:17

for f, g being Function holds rng (f +* g) c= (rng f) \/ (rng g)

proof end;

theorem :: FUNCT_4:18

for f, g being Function holds rng g c= rng (f +* g)

proof end;

theorem Th19: :: FUNCT_4:19

for f, g being Function st dom f c= dom g holds
f +* g = g

proof end;

registration

let f be Function;
let g be empty Function;

reduce g +* f to f;

reducibility
g +* f = f

proof end;

reduce f +* g to f;

reducibility
f +* g = f

proof end;

end;

theorem :: FUNCT_4:20

for f being Function holds {} +* f = f ;

theorem :: FUNCT_4:21

for f being Function holds f +* {} = f ;

theorem :: FUNCT_4:22

for X, Y being set holds (id X) +* (id Y) = id (X \/ Y)

proof end;

theorem Th23: :: FUNCT_4:23

for f, g being Function holds (f +* g) | (dom g) = g

proof end;

registration

let f, g be Function;

reduce (f +* g) | (dom g) to g;

reducibility
(f +* g) | (dom g) = g by Th23;

end;

theorem Th24: :: FUNCT_4:24

for f, g being Function holds (f +* g) | ((dom f) \ (dom g)) c= f

proof end;

theorem Th25: :: FUNCT_4:25

for f, g being Function holds g c= f +* g

proof end;

theorem :: FUNCT_4:26

for f, g, h being Function st f tolerates g +* h holds
f | ((dom f) \ (dom h)) tolerates g

proof end;

theorem Th27: :: FUNCT_4:27

for f, g, h being Function st f tolerates g +* h holds
f tolerates h

proof end;

theorem Th28: :: FUNCT_4:28

for f, g being Function holds
( f tolerates g iff f c= f +* g )

proof end;

theorem Th29: :: FUNCT_4:29

for f, g being Function holds f +* g c= f \/ g

proof end;

theorem Th30: :: FUNCT_4:30

for f, g being Function holds
( f tolerates g iff f \/ g = f +* g )

proof end;

theorem Th31: :: FUNCT_4:31

for f, g being Function st dom f misses dom g holds
f \/ g = f +* g by Th30, PARTFUN1:56;

theorem Th32: :: FUNCT_4:32

for f, g being Function st dom f misses dom g holds
f c= f +* g

proof end;

theorem :: FUNCT_4:33

for f, g being Function st dom f misses dom g holds
(f +* g) | (dom f) = f

proof end;

theorem Th34: :: FUNCT_4:34

for f, g being Function holds
( f tolerates g iff f +* g = g +* f )

proof end;

theorem Th35: :: FUNCT_4:35

for f, g being Function st dom f misses dom g holds
f +* g = g +* f by Th34, PARTFUN1:56;

theorem :: FUNCT_4:36

for X, Y being set
for f, g being PartFunc of X,Y st g is total holds
f +* g = g

proof end;

theorem Th37: :: FUNCT_4:37

for X, Y being set
for f, g being Function of X,Y holds f +* g = g

proof end;

theorem :: FUNCT_4:38

for X being set
for f, g being Function of X,X holds f +* g = g by Th37;

theorem :: FUNCT_4:39

for X being set
for D being non empty set
for f, g being Function of X,D holds f +* g = g by Th37;

theorem :: FUNCT_4:40

for X, Y being set
for f, g being PartFunc of X,Y holds f +* g is PartFunc of X,Y

proof end;

:: The converse function whenever domain

definition

let f be Function;

func ~ f -> Function means :Def2: :: FUNCT_4:def 2
( ( for x being object holds
( x in dom it iff ex y, z being object st
( x = [z,y] & [y,z] in dom f ) ) ) & ( for y, z being object st [y,z] in dom f holds
it . (z,y) = f . (y,z) ) );

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

proof end;

uniqueness
for b₁, b₂ being Function st ( for x being object holds
( x in dom b₁ iff ex y, z being object st
( x = [z,y] & [y,z] in dom f ) ) ) & ( for y, z being object st [y,z] in dom f holds
b₁ . (z,y) = f . (y,z) ) & ( for x being object holds
( x in dom b₂ iff ex y, z being object st
( x = [z,y] & [y,z] in dom f ) ) ) & ( for y, z being object st [y,z] in dom f holds
b₂ . (z,y) = f . (y,z) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines ~ FUNCT_4:def 2 :
for f, b₂ being Function holds
( b₂ = ~ f iff ( ( for x being object holds
( x in dom b₂ iff ex y, z being object st
( x = [z,y] & [y,z] in dom f ) ) ) & ( for y, z being object st [y,z] in dom f holds
b₂ . (z,y) = f . (y,z) ) ) );

theorem Th41: :: FUNCT_4:41

for f being Function holds rng (~ f) c= rng f

proof end;

theorem Th42: :: FUNCT_4:42

for f being Function
for x, y being object holds
( [x,y] in dom f iff [y,x] in dom (~ f) )

proof end;

registration

let f be empty Function;

cluster ~ f -> empty ;

coherence
~ f is empty

proof end;

end;

theorem Th43: :: FUNCT_4:43

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

proof end;

theorem :: FUNCT_4:44

for f being Function ex X, Y being set st dom (~ f) c= [:X,Y:]

proof end;

theorem Th45: :: FUNCT_4:45

for X, Y being set
for f being Function st dom f c= [:X,Y:] holds
dom (~ f) c= [:Y,X:]

proof end;

theorem Th46: :: FUNCT_4:46

for X, Y being set
for f being Function st dom f = [:X,Y:] holds
dom (~ f) = [:Y,X:]

proof end;

theorem Th47: :: FUNCT_4:47

for X, Y being set
for f being Function st dom f c= [:X,Y:] holds
rng (~ f) = rng f

proof end;

theorem Th48: :: FUNCT_4:48

for X, Y, Z being set
for f being PartFunc of [:X,Y:],Z holds ~ f is PartFunc of [:Y,X:],Z

proof end;

definition

let X, Y, Z be set ;
let f be PartFunc of [:X,Y:],Z;
:: original: ~
redefine func ~ f -> PartFunc of [:Y,X:],Z;
coherence
~ f is PartFunc of [:Y,X:],Z by Th48;

end;

theorem Th49: :: FUNCT_4:49

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

proof end;

definition

let X, Y, Z be set ;
let f be Function of [:X,Y:],Z;
:: original: ~
redefine func ~ f -> Function of [:Y,X:],Z;
coherence
~ f is Function of [:Y,X:],Z by Th49;

end;

theorem :: FUNCT_4:50

for X, Y, Z being set
for f being Function of [:X,Y:],Z holds ~ f is Function of [:Y,X:],Z ;

theorem Th51: :: FUNCT_4:51

for f being Function holds ~ (~ f) c= f

proof end;

theorem Th52: :: FUNCT_4:52

for X, Y being set
for f being Function st dom f c= [:X,Y:] holds
~ (~ f) = f

proof end;

theorem :: FUNCT_4:53

for X, Y, Z being set
for f being PartFunc of [:X,Y:],Z holds ~ (~ f) = f

proof end;

:: Product of 2'ary functions

definition

let f, g be Function;

func |:f,g:| -> Function means :Def3: :: FUNCT_4:def 3
( ( for z being object holds
( z in dom it iff ex x, y, x9, y9 being object st
( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) ) & ( for x, y, x9, y9 being object st [x,y] in dom f & [x9,y9] in dom g holds
it . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] ) );

existence
ex b₁ being Function st
( ( for z being object holds
( z in dom b₁ iff ex x, y, x9, y9 being object st
( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) ) & ( for x, y, x9, y9 being object st [x,y] in dom f & [x9,y9] in dom g holds
b₁ . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] ) )

proof end;

uniqueness
for b₁, b₂ being Function st ( for z being object holds
( z in dom b₁ iff ex x, y, x9, y9 being object st
( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) ) & ( for x, y, x9, y9 being object st [x,y] in dom f & [x9,y9] in dom g holds
b₁ . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] ) & ( for z being object holds
( z in dom b₂ iff ex x, y, x9, y9 being object st
( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) ) & ( for x, y, x9, y9 being object st [x,y] in dom f & [x9,y9] in dom g holds
b₂ . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines |: FUNCT_4:def 3 :
for f, g, b₃ being Function holds
( b₃ = |:f,g:| iff ( ( for z being object holds
( z in dom b₃ iff ex x, y, x9, y9 being object st
( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) ) & ( for x, y, x9, y9 being object st [x,y] in dom f & [x9,y9] in dom g holds
b₃ . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] ) ) );

theorem Th54: :: FUNCT_4:54

for x, x9, y, y9 being object
for f, g being Function holds
( [[x,x9],[y,y9]] in dom |:f,g:| iff ( [x,y] in dom f & [x9,y9] in dom g ) )

proof end;

theorem :: FUNCT_4:55

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

proof end;

theorem Th56: :: FUNCT_4:56

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

proof end;

theorem Th57: :: FUNCT_4:57

for X, X9, Y, Y9 being set
for f, g being Function st dom f c= [:X,Y:] & dom g c= [:X9,Y9:] holds
dom |:f,g:| c= [:[:X,X9:],[:Y,Y9:]:]

proof end;

theorem Th58: :: FUNCT_4:58

for X, X9, Y, Y9 being set
for f, g being Function st dom f = [:X,Y:] & dom g = [:X9,Y9:] holds
dom |:f,g:| = [:[:X,X9:],[:Y,Y9:]:]

proof end;

theorem Th59: :: FUNCT_4:59

for X, X9, Y, Y9, Z, Z9 being set
for f being PartFunc of [:X,Y:],Z
for g being PartFunc of [:X9,Y9:],Z9 holds |:f,g:| is PartFunc of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:]

proof end;

theorem Th60: :: FUNCT_4:60

for X, X9, Y, Y9, Z, Z9 being set
for f being Function of [:X,Y:],Z
for g being Function of [:X9,Y9:],Z9 st Z <> {} & Z9 <> {} holds
|:f,g:| is Function of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:]

proof end;

theorem :: FUNCT_4:61

for X, X9, Y, Y9 being set
for D, D9 being non empty set
for f being Function of [:X,Y:],D
for g being Function of [:X9,Y9:],D9 holds |:f,g:| is Function of [:[:X,X9:],[:Y,Y9:]:],[:D,D9:] by Th60;

definition

let x, y, a, b be object ;

func (x,y) --> (a,b) -> set equals :: FUNCT_4:def 4
(x .--> a) +* (y .--> b);

correctness
coherence
(x .--> a) +* (y .--> b) is set ;
;

end;

:: deftheorem defines --> FUNCT_4:def 4 :
for x, y, a, b being object holds (x,y) --> (a,b) = (x .--> a) +* (y .--> b);

registration

let x, y, a, b be object ;

cluster (x,y) --> (a,b) -> Relation-like Function-like ;

coherence
( (x,y) --> (a,b) is Function-like & (x,y) --> (a,b) is Relation-like ) ;

end;

theorem Th62: :: FUNCT_4:62

for x1, x2, y1, y2 being object holds
( dom ((x1,x2) --> (y1,y2)) = {x1,x2} & rng ((x1,x2) --> (y1,y2)) c= {y1,y2} )

proof end;

theorem Th63: :: FUNCT_4:63

for x1, x2, y1, y2 being object holds
( ( x1 <> x2 implies ((x1,x2) --> (y1,y2)) . x1 = y1 ) & ((x1,x2) --> (y1,y2)) . x2 = y2 )

proof end;

theorem :: FUNCT_4:64

for x1, x2, y1, y2 being object st x1 <> x2 holds
rng ((x1,x2) --> (y1,y2)) = {y1,y2}

proof end;

theorem :: FUNCT_4:65

for x1, x2, y being object holds (x1,x2) --> (y,y) = {x1,x2} --> y

proof end;

definition

let A be non empty set ;
let x1, x2 be object ;
let y1, y2 be Element of A;
:: original: -->
redefine func (x1,x2) --> (y1,y2) -> Function of {x1,x2},A;
coherence
(x1,x2) --> (y1,y2) is Function of {x1,x2},A

proof end;

end;

theorem :: FUNCT_4:66

for a, b, c, d being object
for g being Function st dom g = {a,b} & g . a = c & g . b = d holds
g = (a,b) --> (c,d)

proof end;

theorem Th67: :: FUNCT_4:67

for a, b, c, d being object st a <> c holds
(a,c) --> (b,d) = {[a,b],[c,d]}

proof end;

theorem :: FUNCT_4:68

for a, b, x, y, x9, y9 being object st a <> b & (a,b) --> (x,y) = (a,b) --> (x9,y9) holds
( x = x9 & y = y9 )

proof end;

:: from CIRCCOMB

theorem :: FUNCT_4:69

for f1, f2, g1, g2 being Function st rng g1 c= dom f1 & rng g2 c= dom f2 & f1 tolerates f2 holds
(f1 +* f2) * (g1 +* g2) = (f1 * g1) +* (f2 * g2)

proof end;

theorem Th70: :: FUNCT_4:70

for f being Function
for A, B being set st dom f c= A \/ B holds
(f | A) +* (f | B) = f

proof end;

:: from AMI_5

theorem Th71: :: FUNCT_4:71

for p, q being Function
for A being set holds (p +* q) | A = (p | A) +* (q | A)

proof end;

theorem Th72: :: FUNCT_4:72

for f, g being Function
for A being set st A misses dom g holds
(f +* g) | A = f | A

proof end;

theorem :: FUNCT_4:73

for f, g being Function
for A being set st dom f misses A holds
(f +* g) | A = g | A

proof end;

theorem :: FUNCT_4:74

for f, g, h being Function st dom g = dom h holds
(f +* g) +* h = f +* h

proof end;

Lm2: for f, g being Function st f c= g holds
g +* f = g

proof end;

theorem :: FUNCT_4:75

for f being Function
for A being set holds f +* (f | A) = f by Lm2, RELAT_1:59;

theorem :: FUNCT_4:76

for f, g being Function
for B, C being set st dom f c= B & dom g c= C & B misses C holds
( (f +* g) | B = f & (f +* g) | C = g )

proof end;

theorem :: FUNCT_4:77

for p, q being Function
for A being set st dom p c= A & dom q misses A holds
(p +* q) | A = p

proof end;

theorem :: FUNCT_4:78

for f being Function
for A, B being set holds f | (A \/ B) = (f | A) +* (f | B)

proof end;

theorem :: FUNCT_4:79

for i, j, k being object holds (i,j) :-> k = [i,j] .--> k ;

theorem :: FUNCT_4:80

for i, j, k being object holds ((i,j) :-> k) . (i,j) = k by FUNCOP_1:71;

:: from AMI_1, 2006.03.14, A.T.

theorem Th81: :: FUNCT_4:81

for a, b, c being object holds (a,a) --> (b,c) = a .--> c

proof end;

theorem :: FUNCT_4:82

for x, y being object holds x .--> y = {[x,y]} by ZFMISC_1:29;

:: from SCMPDS_9, 2006.03.26, A.T.

theorem :: FUNCT_4:83

for f being Function
for a, b, c being object st a <> c holds
(f +* (a .--> b)) . c = f . c

proof end;

theorem Th84: :: FUNCT_4:84

for f being Function
for a, b, c, d being object st a <> b holds
( (f +* ((a,b) --> (c,d))) . a = c & (f +* ((a,b) --> (c,d))) . b = d )

proof end;

:: from AMI_3, 2007.06.14, A.T.

theorem Th85: :: FUNCT_4:85

for a, b being set
for f being Function st a in dom f & f . a = b holds
a .--> b c= f

proof end;

theorem :: FUNCT_4:86

for a, b, c, d being set
for f being Function st a in dom f & c in dom f & f . a = b & f . c = d holds
(a,c) --> (b,d) c= f

proof end;

:: from SCMFSA6A, 2007.07.23, A.T.

theorem Th87: :: FUNCT_4:87

for f, g, h being Function st f c= h & g c= h holds
f +* g c= h

proof end;

:: from SCMFSA6B, 2007.07.25, A.T.

theorem :: FUNCT_4:88

for f, g being Function
for A being set st A /\ (dom f) c= A /\ (dom g) holds
(f +* (g | A)) | A = g | A

proof end;

:: from SCMBSORT, 2007.07.26, A.T.

theorem Th89: :: FUNCT_4:89

for f being Function
for a, b, n, m being object holds ((f +* (a .--> b)) +* (m .--> n)) . m = n

proof end;

theorem :: FUNCT_4:90

for f being Function
for n, m being object holds ((f +* (n .--> m)) +* (m .--> n)) . n = m

proof end;

theorem :: FUNCT_4:91

for f being Function
for a, b, n, m, x being object st x <> m & x <> a holds
((f +* (a .--> b)) +* (m .--> n)) . x = f . x

proof end;

:: from KNASTER, 2007.010.28, A.T.

theorem :: FUNCT_4:92

for f, g being Function st f is one-to-one & g is one-to-one & rng f misses rng g holds
f +* g is one-to-one

proof end;

registration

let f, g be Function;

reduce (f +* g) +* g to f +* g;

reducibility
(f +* g) +* g = f +* g

proof end;

end;

:: from SCMFSA_9, 2008.03.04, A.T.

theorem :: FUNCT_4:93

for f, g being Function holds (f +* g) +* g = f +* g ;

theorem :: FUNCT_4:94

for f, g, h being Function
for D being set st (f +* g) | D = h | D holds
(h +* g) | D = (f +* g) | D

proof end;

theorem :: FUNCT_4:95

for f, g, h being Function
for D being set st f | D = h | D holds
(h +* g) | D = (f +* g) | D

proof end;

:: missing, 2008.03.20, A.T.

theorem Th96: :: FUNCT_4:96

for x being object holds x .--> x = id {x}

proof end;

theorem Th97: :: FUNCT_4:97

for f, g being Function st f c= g holds
f +* g = g

proof end;

theorem Th98: :: FUNCT_4:98

for f, g being Function st f c= g holds
g +* f = g

proof end;

definition

let f be Function;
let x, y be object ;

func f +~ (x,y) -> set equals :: FUNCT_4:def 5
f +* ((x .--> y) * f);

coherence
f +* ((x .--> y) * f) is set ;

end;

:: deftheorem defines +~ FUNCT_4:def 5 :
for f being Function
for x, y being object holds f +~ (x,y) = f +* ((x .--> y) * f);

registration

let f be Function;
let x, y be object ;

cluster f +~ (x,y) -> Relation-like Function-like ;

coherence
( f +~ (x,y) is Relation-like & f +~ (x,y) is Function-like ) ;

end;

theorem Th99: :: FUNCT_4:99

for f being Function
for x, y being object holds dom (f +~ (x,y)) = dom f

proof end;

theorem Th100: :: FUNCT_4:100

for f being Function
for x, y being object st x <> y holds
not x in rng (f +~ (x,y))

proof end;

theorem :: FUNCT_4:101

for f being Function
for x, y being object st x in rng f holds
y in rng (f +~ (x,y))

proof end;

theorem Th102: :: FUNCT_4:102

for f being Function
for x being object holds f +~ (x,x) = f

proof end;

theorem Th103: :: FUNCT_4:103

for f being Function
for x, y being object st not x in rng f holds
f +~ (x,y) = f

proof end;

theorem :: FUNCT_4:104

for f being Function
for x, y being object holds rng (f +~ (x,y)) c= ((rng f) \ {x}) \/ {y}

proof end;

theorem :: FUNCT_4:105

for f being Function
for x, y, z being object st f . z <> x holds
(f +~ (x,y)) . z = f . z

proof end;

theorem :: FUNCT_4:106

for z being object
for f being Function
for x, y being object st z in dom f & f . z = x holds
(f +~ (x,y)) . z = y

proof end;

:: missing, 2008.04.06, A.T.

theorem :: FUNCT_4:107

for f being Function
for x, y being object st not x in dom f holds
f c= f +* (x .--> y)

proof end;

theorem :: FUNCT_4:108

for X, Y being set
for f being PartFunc of X,Y
for x, y being object st x in X & y in Y holds
f +* (x .--> y) is PartFunc of X,Y

proof end;

:: from FINSEQ_1, 2008.05.06, A.T.

registration

let f be Function;
let g be non empty Function;

cluster f +* g -> non empty ;

coherence
not f +* g is empty

proof end;

cluster g +* f -> non empty ;

coherence
not g +* f is empty

proof end;

end;

:: from CIRCCOMB, 2009.01.26, A.T.

registration

let f, g be non-empty Function;

cluster f +* g -> non-empty ;

coherence
f +* g is non-empty

proof end;

end;

definition

let X, Y be set ;
let f, g be PartFunc of X,Y;
:: original: +*
redefine func f +* g -> PartFunc of X,Y;
coherence
f +* g is PartFunc of X,Y

proof end;

end;

theorem :: FUNCT_4:109

for z, y being object
for x being set holds dom ((x --> y) +* (x .--> z)) = succ x

proof end;

theorem :: FUNCT_4:110

for z, y being object
for x being set holds dom (((x --> y) +* (x .--> z)) +* ((succ x) .--> z)) = succ (succ x)

proof end;

registration

let f, g be Function-yielding Function;

cluster f +* g -> Function-yielding ;

coherence
f +* g is Function-yielding

proof end;

end;

:: 2009.10.03, A.T.

registration

let I be set ;
let f, g be I -defined Function;

cluster f +* g -> I -defined ;

coherence
f +* g is I -defined

proof end;

end;

registration

let I be set ;
let f be I -defined total Function;
let g be I -defined Function;

cluster f +* g -> I -defined total for I -defined Function;

coherence
for b₁ being I -defined Function st b₁ = f +* g holds
b₁ is total

proof end;

cluster g +* f -> I -defined total for I -defined Function;

coherence
for b₁ being I -defined Function st b₁ = g +* f holds
b₁ is total

proof end;

end;

registration

let I be set ;
let g, h be I -valued Function;

cluster g +* h -> I -valued ;

coherence
g +* h is I -valued

proof end;

end;

registration

let f be Function;
let g, h be f -compatible Function;

cluster g +* h -> f -compatible ;

coherence
g +* h is f -compatible

proof end;

end;

:: missing, 2010.01.6, A.T

theorem :: FUNCT_4:111

for f being Function
for A being set holds (f | A) +* f = f by Th97, RELAT_1:59;

:: from AMISTD_3, 2010.01.10, A.T

theorem :: FUNCT_4:112

for y, x being object
for R being Relation st dom R = {x} & rng R = {y} holds
R = x .--> y

proof end;

theorem :: FUNCT_4:113

for f being Function
for y, x being object holds (f +* (x .--> y)) . x = y

proof end;

theorem :: FUNCT_4:114

for z1, z2 being object
for f being Function
for x being object holds (f +* (x .--> z1)) +* (x .--> z2) = f +* (x .--> z2)

proof end;

registration

let A be non empty set ;
let a, b be Element of A;
let x, y be set ;

cluster (a,b) --> (x,y) -> A -defined ;

coherence
(a,b) --> (x,y) is A -defined ;

end;

theorem :: FUNCT_4:115

for f, g, h being Function st dom g misses dom h holds
((f +* g) +* h) +* g = (f +* g) +* h

proof end;

theorem :: FUNCT_4:116

for f, g, h being Function st dom f misses dom h & f c= g +* h holds
f c= g

proof end;

theorem Th117: :: FUNCT_4:117

for f, g, h being Function st dom f misses dom h & f c= g holds
f c= g +* h

proof end;

theorem :: FUNCT_4:118

for f, g, h being Function st dom g misses dom h holds
(f +* g) +* h = (f +* h) +* g

proof end;

theorem :: FUNCT_4:119

for f, g being Function st dom f misses dom g holds
(f +* g) \ g = f

proof end;

theorem :: FUNCT_4:120

for f, g being Function st dom f misses dom g holds
f \ g = f by RELAT_1:179, XBOOLE_1:83;

theorem :: FUNCT_4:121

for f, g, h being Function st dom g misses dom h holds
(f \ g) +* h = (f +* h) \ g

proof end;

theorem :: FUNCT_4:122

for f1, f2, g1, g2 being Function st f1 c= g1 & f2 c= g2 & dom f1 misses dom g2 holds
f1 +* f2 c= g1 +* g2

proof end;

theorem Th123: :: FUNCT_4:123

for f, g, h being Function st f c= g holds
f +* h c= g +* h

proof end;

theorem :: FUNCT_4:124

for f, g, h being Function st f c= g & dom f misses dom h holds
f c= g +* h

proof end;

registration

let x, y be set ;

cluster x .--> y -> trivial ;

coherence
x .--> y is trivial ;

end;

:: from CIRCCOMB, 2011.04.19, A.T

theorem :: FUNCT_4:125

for f, g, h being Function st f tolerates g & g tolerates h & h tolerates f holds
f +* g tolerates h

proof end;

definition

let A, B be non empty set ;
let f be PartFunc of [:A,A:],A;
let g be PartFunc of [:B,B:],B;
:: original: |:
redefine func |:f,g:| -> PartFunc of [:[:A,B:],[:A,B:]:],[:A,B:];
coherence
|:f,g:| is PartFunc of [:[:A,B:],[:A,B:]:],[:A,B:] by Th59;

end;

theorem :: FUNCT_4:126

for A1, A2 being non empty set
for Y1 being non empty Subset of A1
for Y2 being non empty Subset of A2
for f being PartFunc of [:A1,A1:],A1
for g being PartFunc of [:A2,A2:],A2
for F being PartFunc of [:Y1,Y1:],Y1 st F = f || Y1 holds
for G being PartFunc of [:Y2,Y2:],Y2 st G = g || Y2 holds
|:F,G:| = |:f,g:| || [:Y1,Y2:]

proof end;

theorem :: FUNCT_4:127

for z being object
for f being Function
for x, y being object st x <> y holds
(f +~ (x,y)) +~ (x,z) = f +~ (x,y)

proof end;

definition

let a, b, c, x, y, z be object ;

func (a,b,c) --> (x,y,z) -> set equals :: FUNCT_4:def 6
((a,b) --> (x,y)) +* (c .--> z);

coherence
((a,b) --> (x,y)) +* (c .--> z) is set ;

end;

:: deftheorem defines --> FUNCT_4:def 6 :
for a, b, c, x, y, z being object holds (a,b,c) --> (x,y,z) = ((a,b) --> (x,y)) +* (c .--> z);

registration

let a, b, c, x, y, z be object ;

cluster (a,b,c) --> (x,y,z) -> Relation-like Function-like ;

coherence
( (a,b,c) --> (x,y,z) is Function-like & (a,b,c) --> (x,y,z) is Relation-like ) ;

end;

theorem Th128: :: FUNCT_4:128

for a, b, c, x, y, z being object holds dom ((a,b,c) --> (x,y,z)) = {a,b,c}

proof end;

theorem :: FUNCT_4:129

for a, b, c, x, y, z being object holds rng ((a,b,c) --> (x,y,z)) c= {x,y,z}

proof end;

theorem :: FUNCT_4:130

for a, x, y, z being object holds (a,a,a) --> (x,y,z) = a .--> z

proof end;

theorem :: FUNCT_4:131

for a, b, x, y, z being object holds (a,a,b) --> (x,y,z) = (a,b) --> (y,z) by Th81;

theorem Th132: :: FUNCT_4:132

for a, b, x, y, z being object st a <> b holds
(a,b,a) --> (x,y,z) = (a,b) --> (z,y)

proof end;

theorem :: FUNCT_4:133

for a, b, x, y, z being object holds (a,b,b) --> (x,y,z) = (a,b) --> (x,z)

proof end;

theorem Th134: :: FUNCT_4:134

for a, b, c, x, y, z being object st a <> b & a <> c holds
((a,b,c) --> (x,y,z)) . a = x

proof end;

theorem Th135: :: FUNCT_4:135

for a, b, c, x, y, z being object holds
( ( b <> c implies ((a,b,c) --> (x,y,z)) . b = y ) & ((a,b,c) --> (x,y,z)) . c = z )

proof end;

theorem :: FUNCT_4:136

for a, b, c, x, y, z being object
for f being Function st dom f = {a,b,c} & f . a = x & f . b = y & f . c = z holds
f = (a,b,c) --> (x,y,z)

proof end;

:: from QUATERNI

definition

let x, y, w, z, a, b, c, d be object ;

func (x,y,w,z) --> (a,b,c,d) -> set equals :: FUNCT_4:def 7
((x,y) --> (a,b)) +* ((w,z) --> (c,d));

coherence
((x,y) --> (a,b)) +* ((w,z) --> (c,d)) is set ;

end;

:: deftheorem defines --> FUNCT_4:def 7 :
for x, y, w, z, a, b, c, d being object holds (x,y,w,z) --> (a,b,c,d) = ((x,y) --> (a,b)) +* ((w,z) --> (c,d));

registration

let x, y, w, z, a, b, c, d be object ;

cluster (x,y,w,z) --> (a,b,c,d) -> Relation-like Function-like ;

coherence
( (x,y,w,z) --> (a,b,c,d) is Function-like & (x,y,w,z) --> (a,b,c,d) is Relation-like ) ;

end;

theorem Th137: :: FUNCT_4:137

for a, b, c, x, y, z, w, d being object holds dom ((x,y,w,z) --> (a,b,c,d)) = {x,y,w,z}

proof end;

theorem Th138: :: FUNCT_4:138

for a, b, c, x, y, z, w, d being object holds rng ((x,y,w,z) --> (a,b,c,d)) c= {a,b,c,d}

proof end;

theorem Th139: :: FUNCT_4:139

for a, b, c, x, y, z, w, d being object holds ((x,y,w,z) --> (a,b,c,d)) . z = d

proof end;

theorem Th140: :: FUNCT_4:140

for a, b, c, x, y, z, w, d being object st w <> z holds
((x,y,w,z) --> (a,b,c,d)) . w = c

proof end;

theorem Th141: :: FUNCT_4:141

for a, b, c, x, y, z, w, d being object st y <> w & y <> z holds
((x,y,w,z) --> (a,b,c,d)) . y = b

proof end;

theorem Th142: :: FUNCT_4:142

for a, b, c, x, y, z, w, d being object st x <> y & x <> w & x <> z holds
((x,y,w,z) --> (a,b,c,d)) . x = a

proof end;

theorem :: FUNCT_4:143

for a, b, c, x, y, z, w, d being object st x,y,w,z are_mutually_distinct holds
rng ((x,y,w,z) --> (a,b,c,d)) = {a,b,c,d}

proof end;

theorem :: FUNCT_4:144

for a, b, c, d, e, i, j, k being object
for g being Function st dom g = {a,b,c,d} & g . a = e & g . b = i & g . c = j & g . d = k holds
g = (a,b,c,d) --> (e,i,j,k)

proof end;

theorem :: FUNCT_4:145

for a, c, b, d, x, y, z, w being object st a,c,x,w are_mutually_distinct holds
(a,c,x,w) --> (b,d,y,z) = {[a,b],[c,d],[x,y],[w,z]}

proof end;

theorem :: FUNCT_4:146

for a, b, c, d, x, y, z, w, x9, y9, z9, w9 being object st a,b,c,d are_mutually_distinct & (a,b,c,d) --> (x,y,z,w) = (a,b,c,d) --> (x9,y9,z9,w9) holds
( x = x9 & y = y9 & z = z9 & w = w9 )

proof end;

:: from AOFA_A00

theorem :: FUNCT_4:147

for a1, a2, a3, b1, b2, b3 being object st a1,a2,a3 are_mutually_distinct holds
rng ((a1,a2,a3) --> (b1,b2,b3)) = {b1,b2,b3}

proof end;

definition

let C, D, E be non empty set ;
let f be Function of [:C,D:],E;

:: original: ~
redefine func ~ f -> Function of [:D,C:],E means :: FUNCT_4:def 8
for d being Element of D
for c being Element of C holds it . (d,c) = f . (c,d);

coherence
~ f is Function of [:D,C:],E

proof end;

compatibility
for b₁ being Function of [:D,C:],E holds
( b₁ = ~ f iff for d being Element of D
for c being Element of C holds b₁ . (d,c) = f . (c,d) )

proof end;

end;

:: deftheorem defines ~ FUNCT_4:def 8 :
for C, D, E being non empty set
for f being Function of [:C,D:],E
for b₅ being Function of [:D,C:],E holds
( b₅ = ~ f iff for d being Element of D
for c being Element of C holds b₅ . (d,c) = f . (c,d) );