:: by Czes{\l}aw Byli\'nski

::

:: Received March 1, 1990

:: Copyright (c) 1990-2018 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:]

ex x, y being object st z = [x,y] ) holds

ex X, Y being set st Z c= [:X,Y:]

proof end;

:: Natural order on functions

definition

let f, g be Function;

ex b_{1} being Function st

( dom b_{1} = (dom f) \/ (dom g) & ( for x being object st x in (dom f) \/ (dom g) holds

( ( x in dom g implies b_{1} . x = g . x ) & ( not x in dom g implies b_{1} . x = f . x ) ) ) )

for b_{1}, b_{2} being Function st dom b_{1} = (dom f) \/ (dom g) & ( for x being object st x in (dom f) \/ (dom g) holds

( ( x in dom g implies b_{1} . x = g . x ) & ( not x in dom g implies b_{1} . x = f . x ) ) ) & dom b_{2} = (dom f) \/ (dom g) & ( for x being object st x in (dom f) \/ (dom g) holds

( ( x in dom g implies b_{2} . x = g . x ) & ( not x in dom g implies b_{2} . x = f . x ) ) ) holds

b_{1} = b_{2}

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;
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 ( 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 ) ) ) );

ex b

( dom b

( ( x in dom g implies b

proof end;

uniqueness for b

( ( x in dom g implies b

( ( x in dom g implies 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 ) ) ) ) ;

:: deftheorem Def1 defines +* FUNCT_4:def 1 :

for f, g, b_{3} being Function holds

( b_{3} = f +* g iff ( dom b_{3} = (dom f) \/ (dom g) & ( for x being object st x in (dom f) \/ (dom g) holds

( ( x in dom g implies b_{3} . x = g . x ) & ( not x in dom g implies b_{3} . x = f . x ) ) ) ) );

for f, g, b

( b

( ( x in dom g implies b

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 ) )

for x being object holds

( x in dom (f +* g) iff ( x in dom f or x in dom g ) )

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

for f, g being Function st dom f misses dom g & x in dom f holds

(f +* g) . x = f . x

proof end;

registration

let f be Function;

let g be empty Function;

reducibility

g +* f = f

f +* g = f

end;
let g be empty Function;

reducibility

g +* f = f

proof end;

reducibility f +* g = f

proof end;

theorem :: FUNCT_4:39

:: The converse function whenever domain

definition

let f be Function;

ex b_{1} being Function st

( ( for x being object holds

( x in dom b_{1} 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_{1} . (z,y) = f . (y,z) ) )

for b_{1}, b_{2} being Function st ( for x being object holds

( x in dom b_{1} 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_{1} . (z,y) = f . (y,z) ) & ( for x being object holds

( x in dom b_{2} 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_{2} . (z,y) = f . (y,z) ) holds

b_{1} = b_{2}

end;
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 ( ( 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) ) );

ex b

( ( for x being object holds

( x in dom b

( x = [z,y] & [y,z] in dom f ) ) ) & ( for y, z being object st [y,z] in dom f holds

b

proof end;

uniqueness for b

( x in dom b

( x = [z,y] & [y,z] in dom f ) ) ) & ( for y, z being object st [y,z] in dom f holds

b

( x in dom b

( x = [z,y] & [y,z] in dom f ) ) ) & ( for y, z being object st [y,z] in dom f holds

b

b

proof end;

:: deftheorem Def2 defines ~ FUNCT_4:def 2 :

for f, b_{2} being Function holds

( b_{2} = ~ f iff ( ( for x being object holds

( x in dom b_{2} 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_{2} . (z,y) = f . (y,z) ) ) );

for f, b

( b

( x in dom b

( x = [z,y] & [y,z] in dom f ) ) ) & ( for y, z being object st [y,z] in dom f holds

b

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

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

theorem :: FUNCT_4:50

:: Product of 2'ary functions

definition

let f, g be Function;

ex b_{1} being Function st

( ( for z being object holds

( z in dom b_{1} 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_{1} . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] ) )

for b_{1}, b_{2} being Function st ( for z being object holds

( z in dom b_{1} 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_{1} . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] ) & ( for z being object holds

( z in dom b_{2} 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_{2} . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] ) holds

b_{1} = b_{2}

end;
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 ( ( 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))] ) );

ex b

( ( for z being object holds

( z in dom b

( 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

proof end;

uniqueness for b

( z in dom b

( 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

( z in dom b

( 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

b

proof end;

:: deftheorem Def3 defines |: FUNCT_4:def 3 :

for f, g, b_{3} being Function holds

( b_{3} = |:f,g:| iff ( ( for z being object holds

( z in dom b_{3} 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_{3} . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] ) ) );

for f, g, b

( b

( z in dom b

( 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

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 ) )

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))]

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

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

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

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

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

:: deftheorem defines --> FUNCT_4:def 4 :

for x, y, a, b being object holds (x,y) --> (a,b) = (x .--> a) +* (y .--> b);

for x, y, a, b being object holds (x,y) --> (a,b) = (x .--> a) +* (y .--> b);

registration

let x, y, a, b be object ;

coherence

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

end;
coherence

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

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} )

( 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 )

( ( x1 <> x2 implies ((x1,x2) --> (y1,y2)) . x1 = y1 ) & ((x1,x2) --> (y1,y2)) . x2 = y2 )

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

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

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)

for g being Function st dom g = {a,b} & g . a = c & g . b = d holds

g = (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 )

( 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)

(f1 +* f2) * (g1 +* g2) = (f1 * g1) +* (f2 * g2)

proof end;

:: from AMI_5

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

g +* f = g

proof end;

theorem :: FUNCT_4:75

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 )

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;

:: from AMI_1, 2006.03.14, A.T.

:: from SCMPDS_9, 2006.03.26, A.T.

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 )

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

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.

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

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

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

f +* g is one-to-one

proof end;

:: from SCMFSA_9, 2008.03.04, A.T.

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

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

(h +* g) | D = (f +* g) | D

proof end;

:: missing, 2008.03.20, A.T.

:: deftheorem defines +~ FUNCT_4:def 5 :

for f being Function

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

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 ;

coherence

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

end;
let x, y be object ;

coherence

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

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

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

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;

coherence

not f +* g is empty

not g +* f is empty

end;
let g be non empty Function;

coherence

not f +* g is empty

proof end;

coherence not g +* f is empty

proof end;

:: from CIRCCOMB, 2009.01.26, A.T.

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

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

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)

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

proof end;

registration
end;

:: 2009.10.03, A.T.

registration
end;

registration

let I be set ;

let f be I -defined total Function;

let g be I -defined Function;

coherence

for b_{1} being I -defined Function st b_{1} = f +* g holds

b_{1} is total

for b_{1} being I -defined Function st b_{1} = g +* f holds

b_{1} is total

end;
let f be I -defined total Function;

let g be I -defined Function;

coherence

for b

b

proof end;

coherence for b

b

proof end;

registration
end;

registration
end;

:: missing, 2010.01.6, A.T

theorem :: FUNCT_4:111

:: from AMISTD_3, 2010.01.10, A.T

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)

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 ;

coherence

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

end;
let a, b be Element of A;

let x, y be set ;

coherence

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

theorem :: FUNCT_4:120

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

f1 +* f2 c= g1 +* g2

proof 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

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

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

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)

for f being Function

for x, y being object st x <> y holds

(f +~ (x,y)) +~ (x,z) = f +~ (x,y)

proof 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);

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 ;

coherence

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

end;
coherence

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

theorem :: FUNCT_4:131

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 )

( ( 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)

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

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 ;

coherence

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

end;
coherence

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

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

((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}

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)

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]}

(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 )

( 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}

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;

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

for b_{1} being Function of [:D,C:],E holds

( b_{1} = ~ f iff for d being Element of D

for c being Element of C holds b_{1} . (d,c) = f . (c,d) )

end;
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 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);

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

proof end;

compatibility for b

( b

for c being Element of C holds b

proof 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_{5} being Function of [:D,C:],E holds

( b_{5} = ~ f iff for d being Element of D

for c being Element of C holds b_{5} . (d,c) = f . (c,d) );

for C, D, E being non empty set

for f being Function of [:C,D:],E

for b

( b

for c being Element of C holds b