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

::

:: Received March 1, 1990

:: Copyright (c) 1990 Association of Mizar Users

begin

Lm1: for x, y, Z being set st [x,y] in Z holds

( x in union (union Z) & y in union (union Z) )

proof end;

Lm2: for x, x9, y, y9, x1, x19, y1, y19 being set 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 set st z in Z holds

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

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

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

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

proof end;

theorem :: FUNCT_4:2

proof end;

theorem :: FUNCT_4:3

canceled;

theorem :: FUNCT_4:4

proof end;

theorem :: FUNCT_4:5

proof end;

theorem Th6: :: FUNCT_4:6

proof end;

theorem :: FUNCT_4:7

proof end;

theorem :: FUNCT_4:8

proof end;

theorem :: FUNCT_4:9

proof end;

theorem :: FUNCT_4:10

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 set 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_{1} being Function st

( dom b_{1} = (dom f) \/ (dom g) & ( for x being set 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 set 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 set 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 set 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 set 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

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

( b

( ( x in dom g implies b

theorem Th11: :: FUNCT_4:11

proof end;

theorem Th12: :: FUNCT_4:12

proof end;

theorem Th13: :: FUNCT_4:13

for x being set

for f, g being Function holds

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

for f, g being Function holds

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

proof end;

theorem Th14: :: FUNCT_4:14

proof end;

theorem Th15: :: FUNCT_4:15

proof end;

theorem Th16: :: FUNCT_4:16

proof end;

theorem :: FUNCT_4:17

for x being set

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;

theorem Th18: :: FUNCT_4:18

proof end;

theorem :: FUNCT_4:19

proof end;

theorem Th20: :: FUNCT_4:20

proof end;

theorem Th21: :: FUNCT_4:21

proof end;

theorem Th22: :: FUNCT_4:22

proof end;

theorem :: FUNCT_4:23

proof end;

theorem :: FUNCT_4:24

proof end;

theorem Th25: :: FUNCT_4:25

proof end;

theorem Th26: :: FUNCT_4:26

proof end;

theorem :: FUNCT_4:27

proof end;

theorem Th28: :: FUNCT_4:28

proof end;

theorem Th29: :: FUNCT_4:29

proof end;

theorem Th30: :: FUNCT_4:30

proof end;

theorem Th31: :: FUNCT_4:31

proof end;

theorem Th32: :: FUNCT_4:32

proof end;

theorem Th33: :: FUNCT_4:33

proof end;

theorem :: FUNCT_4:34

proof end;

theorem Th35: :: FUNCT_4:35

proof end;

theorem Th36: :: FUNCT_4:36

proof end;

theorem :: FUNCT_4:37

proof end;

theorem Th38: :: FUNCT_4:38

proof end;

theorem :: FUNCT_4:39

theorem :: FUNCT_4:40

theorem :: FUNCT_4:41

proof end;

definition

let f be Function;

func ~ f -> Function means :Def2: :: FUNCT_4:def 2

( ( for x being set holds

( x in dom it iff ex y, z being set st

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

it . (z,y) = f . (y,z) ) );

existence

ex b_{1} being Function st

( ( for x being set holds

( x in dom b_{1} iff ex y, z being set st

( x = [z,y] & [y,z] in dom f ) ) ) & ( for y, z being set 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 set holds

( x in dom b_{1} iff ex y, z being set st

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

b_{1} . (z,y) = f . (y,z) ) & ( for x being set holds

( x in dom b_{2} iff ex y, z being set st

( x = [z,y] & [y,z] in dom f ) ) ) & ( for y, z being set 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 set holds

( x in dom it iff ex y, z being set st

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

it . (z,y) = f . (y,z) ) );

existence

ex b

( ( for x being set holds

( x in dom b

( x = [z,y] & [y,z] in dom f ) ) ) & ( for y, z being set 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 set st [y,z] in dom f holds

b

( x in dom b

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

b

b

proof end;

:: deftheorem Def2 defines ~ FUNCT_4:def 2 :

for f, b

( b

( x in dom b

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

b

theorem Th42: :: FUNCT_4:42

proof end;

theorem Th43: :: FUNCT_4:43

proof end;

theorem :: FUNCT_4:44

proof end;

theorem :: FUNCT_4:45

proof end;

theorem Th46: :: FUNCT_4:46

proof end;

theorem Th47: :: FUNCT_4:47

proof end;

theorem Th48: :: FUNCT_4:48

proof end;

theorem :: FUNCT_4:49

proof end;

theorem Th50: :: FUNCT_4:50

for X, Y, Z being set

for f being Function of [:X,Y:],Z st Z <> {} holds

~ f is Function of [:Y,X:],Z

for f being Function of [:X,Y:],Z st Z <> {} holds

~ f is Function of [:Y,X:],Z

proof end;

theorem :: FUNCT_4:51

for X, Y being set

for D being non empty set

for f being Function of [:X,Y:],D holds ~ f is Function of [:Y,X:],D by Th50;

for D being non empty set

for f being Function of [:X,Y:],D holds ~ f is Function of [:Y,X:],D by Th50;

theorem Th52: :: FUNCT_4:52

proof end;

theorem Th53: :: FUNCT_4:53

proof end;

theorem :: FUNCT_4:54

proof end;

theorem :: FUNCT_4:55

canceled;

theorem :: FUNCT_4:56

canceled;

definition

let f, g be Function;

func |:f,g:| -> Function means :Def3: :: FUNCT_4:def 3

( ( for z being set holds

( z in dom it iff ex x, y, x9, y9 being set st

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

( ( for z being set holds

( z in dom b_{1} iff ex x, y, x9, y9 being set st

( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) ) & ( for x, y, x9, y9 being set 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 set holds

( z in dom b_{1} iff ex x, y, x9, y9 being set st

( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) ) & ( for x, y, x9, y9 being set 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 set holds

( z in dom b_{2} iff ex x, y, x9, y9 being set st

( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) ) & ( for x, y, x9, y9 being set 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 set holds

( z in dom it iff ex x, y, x9, y9 being set st

( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) ) & ( for x, y, x9, y9 being set 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

( ( for z being set 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 set 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 set 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 set 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

( 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 set st [x,y] in dom f & [x9,y9] in dom g holds

b

theorem Th57: :: FUNCT_4:57

for x, x9, y, y9 being set

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

for x, x9, y, y9 being set

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 Th59: :: FUNCT_4:59

proof end;

theorem Th60: :: FUNCT_4:60

for X, Y, X9, 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 Th61: :: FUNCT_4:61

for X, Y, X9, 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 :: FUNCT_4:62

for X, Y, Z, X9, Y9, 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 Th63: :: FUNCT_4:63

for X, Y, Z, X9, Y9, 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:64

for X, Y, X9, 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 Th63;

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

definition

let x, y, a, b be set ;

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

(x .--> a) +* (y .--> b);

correctness

coherence

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

;

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

(x .--> a) +* (y .--> b);

correctness

coherence

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

;

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

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

registration

let x, y, a, b be set ;

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;
cluster (x,y) --> (a,b) -> Relation-like Function-like ;

coherence

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

theorem Th65: :: FUNCT_4:65

for x1, x2, y1, y2 being set 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 Th66: :: FUNCT_4:66

for x1, x2, y1, y2 being set 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;

theorem :: FUNCT_4:67

proof end;

theorem :: FUNCT_4:68

proof end;

definition

let A be non empty set ;

let x1, x2 be set ;

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

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

for a, b, c, d being set

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

canceled;

theorem Th71: :: FUNCT_4:71

proof end;

theorem :: FUNCT_4:72

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

( x = x9 & y = y9 )

( x = x9 & y = y9 )

proof end;

begin

theorem :: FUNCT_4:73

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;

theorem Th74: :: FUNCT_4:74

proof end;

theorem Th75: :: FUNCT_4:75

proof end;

theorem Th76: :: FUNCT_4:76

proof end;

theorem :: FUNCT_4:77

proof end;

theorem :: FUNCT_4:78

proof end;

theorem Th79: :: FUNCT_4:79

proof end;

theorem :: FUNCT_4:80

proof end;

theorem :: FUNCT_4:81

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;

theorem :: FUNCT_4:82

proof end;

theorem :: FUNCT_4:83

proof end;

theorem :: FUNCT_4:84

theorem :: FUNCT_4:85

theorem :: FUNCT_4:86

proof end;

theorem :: FUNCT_4:87

theorem :: FUNCT_4:88

proof end;

theorem :: FUNCT_4:89

for f being Function

for a, b, c, d being set st a <> b holds

( (f +* ((a,b) --> (c,d))) . a = c & (f +* ((a,b) --> (c,d))) . b = d )

for a, b, c, d being set st a <> b holds

( (f +* ((a,b) --> (c,d))) . a = c & (f +* ((a,b) --> (c,d))) . b = d )

proof end;

theorem Th90: :: FUNCT_4:90

proof end;

theorem :: FUNCT_4:91

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;

theorem :: FUNCT_4:92

proof end;

theorem :: FUNCT_4:93

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;

theorem :: FUNCT_4:94

canceled;

theorem :: FUNCT_4:95

proof end;

theorem :: FUNCT_4:96

proof end;

theorem :: FUNCT_4:97

for f being Function

for a, b, n, m, x being set st x <> m & x <> a holds

((f +* (a .--> b)) +* (m .--> n)) . x = f . x

for a, b, n, m, x being set st x <> m & x <> a holds

((f +* (a .--> b)) +* (m .--> n)) . x = f . x

proof end;

theorem :: FUNCT_4:98

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;

theorem Th99: :: FUNCT_4:99

proof end;

theorem :: FUNCT_4:100

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;

theorem :: FUNCT_4:101

proof end;

theorem Th102: :: FUNCT_4:102

proof end;

theorem :: FUNCT_4:103

proof end;

theorem Th104: :: FUNCT_4:104

proof end;

begin

definition

let f be Function;

let x, y be set ;

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

f +* ((x .--> y) * f);

coherence

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

end;
let x, y be set ;

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

f +* ((x .--> y) * f);

coherence

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

:: deftheorem defines +~ FUNCT_4:def 5 :

for f being Function

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

registration

let f be Function;

let x, y be set ;

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

coherence

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

end;
let x, y be set ;

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

coherence

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

theorem Th105: :: FUNCT_4:105

proof end;

theorem Th106: :: FUNCT_4:106

proof end;

theorem :: FUNCT_4:107

proof end;

theorem Th108: :: FUNCT_4:108

proof end;

theorem Th109: :: FUNCT_4:109

proof end;

theorem :: FUNCT_4:110

proof end;

theorem :: FUNCT_4:111

for z being set

for f being Function

for x, y being set st f . z <> x holds

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

for f being Function

for x, y being set st f . z <> x holds

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

proof end;

theorem :: FUNCT_4:112

for z being set

for f being Function

for x, y being set st z in dom f & f . z = x holds

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

for f being Function

for x, y being set st z in dom f & f . z = x holds

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

proof end;

theorem :: FUNCT_4:113

canceled;

theorem :: FUNCT_4:114

canceled;

theorem :: FUNCT_4:115

proof end;

theorem :: FUNCT_4:116

for X, Y being set

for f being PartFunc of X,Y

for x, y being set 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 set st x in X & y in Y holds

f +* (x .--> y) is PartFunc of X,Y

proof end;

registration

let f be Function;

let g be non empty Function;

cluster f +* g -> non empty ;

coherence

not f +* g is empty

coherence

not g +* f is empty

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

registration

let f, g be non-empty Function;

cluster f +* g -> non-empty ;

coherence

f +* g is non-empty

end;
cluster f +* g -> non-empty ;

coherence

f +* g is non-empty

proof 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

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

proof end;

theorem :: FUNCT_4:118

proof end;

registration

let f, g be Function-yielding Function;

cluster f +* g -> Function-yielding ;

coherence

f +* g is Function-yielding

end;
cluster f +* g -> Function-yielding ;

coherence

f +* g is Function-yielding

proof end;

registration

let I be set ;

let f, g be I -defined Function;

cluster f +* g -> I -defined ;

coherence

f +* g is I -defined

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

cluster f +* g -> I -defined ;

coherence

f +* g is I -defined

proof 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 I -defined Function;

coherence

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

b_{1} is total

coherence

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;

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

coherence

for b

b

proof end;

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

for b

b

proof end;

registration

let I be set ;

let g, h be I -valued Function;

cluster g +* h -> I -valued ;

coherence

g +* h is I -valued

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

cluster g +* h -> I -valued ;

coherence

g +* h is I -valued

proof end;

registration

let f be Function;

let g, h be f -compatible Function;

cluster g +* h -> f -compatible ;

coherence

g +* h is f -compatible

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

cluster g +* h -> f -compatible ;

coherence

g +* h is f -compatible

proof end;

theorem :: FUNCT_4:119

proof end;

theorem :: FUNCT_4:120

proof end;

theorem :: FUNCT_4:121

proof end;

theorem :: FUNCT_4:122

for z1, z2 being set

for f being Function

for x being set holds (f +* (x .--> z1)) +* (x .--> z2) = f +* (x .--> z2)

for f being Function

for x being set 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;
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 ;

theorem :: FUNCT_4:123

proof end;

theorem :: FUNCT_4:124

proof end;

theorem :: FUNCT_4:125

proof end;

theorem :: FUNCT_4:126

proof end;

theorem :: FUNCT_4:127

proof end;

theorem :: FUNCT_4:128

proof end;

theorem :: FUNCT_4:129

proof end;