:: by Edmund Woronowicz

::

:: Received March 15, 1989

:: Copyright (c) 1990 Association of Mizar Users

begin

definition

let IT be set ;

attr IT is Relation-like means :Def1: :: RELAT_1:def 1

for x being set st x in IT holds

ex y, z being set st x = [y,z];

end;
attr IT is Relation-like means :Def1: :: RELAT_1:def 1

for x being set st x in IT holds

ex y, z being set st x = [y,z];

:: deftheorem Def1 defines Relation-like RELAT_1:def 1 :

for IT being set holds

( IT is Relation-like iff for x being set st x in IT holds

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

registration

cluster empty -> Relation-like set ;

coherence

for b_{1} being set st b_{1} is empty holds

b_{1} is Relation-like

end;
coherence

for b

b

proof end;

theorem :: RELAT_1:1

canceled;

theorem :: RELAT_1:2

canceled;

registration

let R be Relation;

cluster -> Relation-like Element of bool R;

coherence

for b_{1} being Subset of R holds b_{1} is Relation-like

end;
cluster -> Relation-like Element of bool R;

coherence

for b

proof end;

scheme :: RELAT_1:sch 1

RelExistence{ F_{1}() -> set , F_{2}() -> set , P_{1}[ set , set ] } :

RelExistence{ F

ex R being Relation st

for x, y being set holds

( [x,y] in R iff ( x in F_{1}() & y in F_{2}() & P_{1}[x,y] ) )

for x, y being set holds

( [x,y] in R iff ( x in F

proof end;

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

( x in union (union X) & y in union (union X) )

proof end;

definition

let P, R be Relation;

redefine pred P = R means :: RELAT_1:def 2

for a, b being set holds

( [a,b] in P iff [a,b] in R );

compatibility

( P = R iff for a, b being set holds

( [a,b] in P iff [a,b] in R ) )

end;
redefine pred P = R means :: RELAT_1:def 2

for a, b being set holds

( [a,b] in P iff [a,b] in R );

compatibility

( P = R iff for a, b being set holds

( [a,b] in P iff [a,b] in R ) )

proof end;

:: deftheorem defines = RELAT_1:def 2 :

for P, R being Relation holds

( P = R iff for a, b being set holds

( [a,b] in P iff [a,b] in R ) );

registration

let P be Relation;

let X be set ;

cluster P /\ X -> Relation-like ;

coherence

P /\ X is Relation-like

coherence

P \ X is Relation-like ;

end;
let X be set ;

cluster P /\ X -> Relation-like ;

coherence

P /\ X is Relation-like

proof end;

cluster P \ X -> Relation-like ;coherence

P \ X is Relation-like ;

registration

let P, R be Relation;

cluster P \/ R -> Relation-like ;

coherence

P \/ R is Relation-like

end;
cluster P \/ R -> Relation-like ;

coherence

P \/ R is Relation-like

proof end;

registration
end;

registration

let a, b be set ;

cluster {[a,b]} -> Relation-like ;

coherence

{[a,b]} is Relation-like

coherence

[:a,b:] is Relation-like

end;
cluster {[a,b]} -> Relation-like ;

coherence

{[a,b]} is Relation-like

proof end;

cluster [:a,b:] -> Relation-like ;coherence

[:a,b:] is Relation-like

proof end;

registration

let a, b, c, d be set ;

cluster {[a,b],[c,d]} -> Relation-like ;

coherence

{[a,b],[c,d]} is Relation-like

end;
cluster {[a,b],[c,d]} -> Relation-like ;

coherence

{[a,b],[c,d]} is Relation-like

proof end;

theorem :: RELAT_1:3

canceled;

theorem :: RELAT_1:4

canceled;

theorem :: RELAT_1:5

canceled;

theorem :: RELAT_1:6

canceled;

definition

let P be Relation;

let A be set ;

redefine pred P c= A means :: RELAT_1:def 3

for a, b being set st [a,b] in P holds

[a,b] in A;

compatibility

( P c= A iff for a, b being set st [a,b] in P holds

[a,b] in A )

end;
let A be set ;

redefine pred P c= A means :: RELAT_1:def 3

for a, b being set st [a,b] in P holds

[a,b] in A;

compatibility

( P c= A iff for a, b being set st [a,b] in P holds

[a,b] in A )

proof end;

:: deftheorem defines c= RELAT_1:def 3 :

for P being Relation

for A being set holds

( P c= A iff for a, b being set st [a,b] in P holds

[a,b] in A );

definition

let R be set ;

func proj1 R -> set means :Def4: :: RELAT_1:def 4

for x being set holds

( x in it iff ex y being set st [x,y] in R );

existence

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ex y being set st [x,y] in R )

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

( x in b_{1} iff ex y being set st [x,y] in R ) ) & ( for x being set holds

( x in b_{2} iff ex y being set st [x,y] in R ) ) holds

b_{1} = b_{2}

end;
func proj1 R -> set means :Def4: :: RELAT_1:def 4

for x being set holds

( x in it iff ex y being set st [x,y] in R );

existence

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def4 defines proj1 RELAT_1:def 4 :

for R, b

( b

( x in b

theorem :: RELAT_1:7

canceled;

theorem :: RELAT_1:8

canceled;

theorem :: RELAT_1:9

canceled;

theorem :: RELAT_1:10

canceled;

theorem :: RELAT_1:11

canceled;

theorem :: RELAT_1:12

canceled;

theorem Th13: :: RELAT_1:13

proof end;

theorem Th14: :: RELAT_1:14

proof end;

theorem :: RELAT_1:15

proof end;

definition

let R be set ;

func proj2 R -> set means :Def5: :: RELAT_1:def 5

for y being set holds

( y in it iff ex x being set st [x,y] in R );

existence

ex b_{1} being set st

for y being set holds

( y in b_{1} iff ex x being set st [x,y] in R )

for b_{1}, b_{2} being set st ( for y being set holds

( y in b_{1} iff ex x being set st [x,y] in R ) ) & ( for y being set holds

( y in b_{2} iff ex x being set st [x,y] in R ) ) holds

b_{1} = b_{2}

end;
func proj2 R -> set means :Def5: :: RELAT_1:def 5

for y being set holds

( y in it iff ex x being set st [x,y] in R );

existence

ex b

for y being set holds

( y in b

proof end;

uniqueness for b

( y in b

( y in b

b

proof end;

:: deftheorem Def5 defines proj2 RELAT_1:def 5 :

for R, b

( b

( y in b

theorem :: RELAT_1:16

canceled;

theorem :: RELAT_1:17

canceled;

theorem :: RELAT_1:18

proof end;

theorem :: RELAT_1:19

proof end;

theorem :: RELAT_1:20

for x, y being set

for R being Relation st [x,y] in R holds

( x in dom R & y in rng R ) by Def4, Def5;

for R being Relation st [x,y] in R holds

( x in dom R & y in rng R ) by Def4, Def5;

theorem Th21: :: RELAT_1:21

proof end;

theorem :: RELAT_1:22

theorem Th23: :: RELAT_1:23

proof end;

theorem :: RELAT_1:24

for a, b, x, y being set

for R being Relation st R = {[a,b],[x,y]} holds

( dom R = {a,x} & rng R = {b,y} )

for R being Relation st R = {[a,b],[x,y]} holds

( dom R = {a,x} & rng R = {b,y} )

proof end;

theorem Th25: :: RELAT_1:25

proof end;

theorem Th26: :: RELAT_1:26

proof end;

theorem Th27: :: RELAT_1:27

proof end;

theorem :: RELAT_1:28

proof end;

definition

let R be Relation;

func field R -> set equals :: RELAT_1:def 6

(dom R) \/ (rng R);

coherence

(dom R) \/ (rng R) is set ;

end;
func field R -> set equals :: RELAT_1:def 6

(dom R) \/ (rng R);

coherence

(dom R) \/ (rng R) is set ;

:: deftheorem defines field RELAT_1:def 6 :

for R being Relation holds field R = (dom R) \/ (rng R);

theorem :: RELAT_1:29

canceled;

theorem :: RELAT_1:30

proof end;

theorem :: RELAT_1:31

proof end;

theorem Th32: :: RELAT_1:32

proof end;

theorem :: RELAT_1:33

proof end;

theorem :: RELAT_1:34

proof end;

definition

let R be Relation;

func R ~ -> Relation means :Def7: :: RELAT_1:def 7

for x, y being set holds

( [x,y] in it iff [y,x] in R );

existence

ex b_{1} being Relation st

for x, y being set holds

( [x,y] in b_{1} iff [y,x] in R )

for b_{1}, b_{2} being Relation st ( for x, y being set holds

( [x,y] in b_{1} iff [y,x] in R ) ) & ( for x, y being set holds

( [x,y] in b_{2} iff [y,x] in R ) ) holds

b_{1} = b_{2}

for b_{1}, b_{2} being Relation st ( for x, y being set holds

( [x,y] in b_{1} iff [y,x] in b_{2} ) ) holds

for x, y being set holds

( [x,y] in b_{2} iff [y,x] in b_{1} )
;

end;
func R ~ -> Relation means :Def7: :: RELAT_1:def 7

for x, y being set holds

( [x,y] in it iff [y,x] in R );

existence

ex b

for x, y being set holds

( [x,y] in b

proof end;

uniqueness for b

( [x,y] in b

( [x,y] in b

b

proof end;

involutiveness for b

( [x,y] in b

for x, y being set holds

( [x,y] in b

:: deftheorem Def7 defines ~ RELAT_1:def 7 :

for R, b

( b

( [x,y] in b

theorem :: RELAT_1:35

canceled;

theorem :: RELAT_1:36

canceled;

theorem Th37: :: RELAT_1:37

proof end;

theorem :: RELAT_1:38

proof end;

theorem :: RELAT_1:39

proof end;

theorem :: RELAT_1:40

proof end;

theorem :: RELAT_1:41

proof end;

definition

let P, R be Relation;

func P * R -> Relation means :Def8: :: RELAT_1:def 8

for x, y being set holds

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

( [x,z] in P & [z,y] in R ) );

existence

ex b_{1} being Relation st

for x, y being set holds

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

( [x,z] in P & [z,y] in R ) )

for b_{1}, b_{2} being Relation st ( for x, y being set holds

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

( [x,z] in P & [z,y] in R ) ) ) & ( for x, y being set holds

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

( [x,z] in P & [z,y] in R ) ) ) holds

b_{1} = b_{2}

end;
func P * R -> Relation means :Def8: :: RELAT_1:def 8

for x, y being set holds

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

( [x,z] in P & [z,y] in R ) );

existence

ex b

for x, y being set holds

( [x,y] in b

( [x,z] in P & [z,y] in R ) )

proof end;

uniqueness for b

( [x,y] in b

( [x,z] in P & [z,y] in R ) ) ) & ( for x, y being set holds

( [x,y] in b

( [x,z] in P & [z,y] in R ) ) ) holds

b

proof end;

:: deftheorem Def8 defines * RELAT_1:def 8 :

for P, R, b

( b

( [x,y] in b

( [x,z] in P & [z,y] in R ) ) );

theorem :: RELAT_1:42

canceled;

theorem :: RELAT_1:43

canceled;

theorem Th44: :: RELAT_1:44

proof end;

theorem Th45: :: RELAT_1:45

proof end;

theorem :: RELAT_1:46

proof end;

theorem :: RELAT_1:47

proof end;

theorem Th48: :: RELAT_1:48

proof end;

theorem Th49: :: RELAT_1:49

proof end;

theorem :: RELAT_1:50

proof end;

theorem :: RELAT_1:51

proof end;

theorem :: RELAT_1:52

proof end;

theorem :: RELAT_1:53

proof end;

theorem :: RELAT_1:54

proof end;

theorem Th55: :: RELAT_1:55

proof end;

registration

cluster non empty Relation-like set ;

existence

not for b_{1} being Relation holds b_{1} is empty

end;
existence

not for b

proof end;

registration

let f be non empty Relation;

cluster proj1 f -> non empty ;

coherence

not dom f is empty

coherence

not rng f is empty

end;
cluster proj1 f -> non empty ;

coherence

not dom f is empty

proof end;

cluster proj2 f -> non empty ;coherence

not rng f is empty

proof end;

theorem Th56: :: RELAT_1:56

proof end;

theorem :: RELAT_1:57

canceled;

theorem :: RELAT_1:58

canceled;

theorem :: RELAT_1:59

canceled;

theorem Th60: :: RELAT_1:60

proof end;

theorem :: RELAT_1:61

canceled;

theorem Th62: :: RELAT_1:62

proof end;

registration

let X be empty set ;

cluster proj1 X -> empty ;

coherence

dom X is empty by Th60;

cluster proj2 X -> empty ;

coherence

rng X is empty by Th60;

let R be Relation;

cluster X * R -> empty ;

coherence

X * R is empty by Th62;

cluster R * X -> empty ;

coherence

R * X is empty by Th62;

end;
cluster proj1 X -> empty ;

coherence

dom X is empty by Th60;

cluster proj2 X -> empty ;

coherence

rng X is empty by Th60;

let R be Relation;

cluster X * R -> empty ;

coherence

X * R is empty by Th62;

cluster R * X -> empty ;

coherence

R * X is empty by Th62;

theorem :: RELAT_1:63

theorem Th64: :: RELAT_1:64

theorem :: RELAT_1:65

theorem :: RELAT_1:66

theorem :: RELAT_1:67

proof end;

definition
end;

:: deftheorem Def9 defines non-empty RELAT_1:def 9 :

for R being Relation holds

( R is non-empty iff not {} in rng R );

registration

cluster Relation-like non-empty set ;

existence

ex b_{1} being Relation st b_{1} is non-empty

end;
existence

ex b

proof end;

registration

let R be Relation;

let S be non-empty Relation;

cluster R * S -> non-empty ;

coherence

R * S is non-empty

end;
let S be non-empty Relation;

cluster R * S -> non-empty ;

coherence

R * S is non-empty

proof end;

definition

let X be set ;

func id X -> Relation means :Def10: :: RELAT_1:def 10

for x, y being set holds

( [x,y] in it iff ( x in X & x = y ) );

existence

ex b_{1} being Relation st

for x, y being set holds

( [x,y] in b_{1} iff ( x in X & x = y ) )

for b_{1}, b_{2} being Relation st ( for x, y being set holds

( [x,y] in b_{1} iff ( x in X & x = y ) ) ) & ( for x, y being set holds

( [x,y] in b_{2} iff ( x in X & x = y ) ) ) holds

b_{1} = b_{2}

end;
func id X -> Relation means :Def10: :: RELAT_1:def 10

for x, y being set holds

( [x,y] in it iff ( x in X & x = y ) );

existence

ex b

for x, y being set holds

( [x,y] in b

proof end;

uniqueness for b

( [x,y] in b

( [x,y] in b

b

proof end;

:: deftheorem Def10 defines id RELAT_1:def 10 :

for X being set

for b

( b

( [x,y] in b

theorem :: RELAT_1:68

canceled;

theorem :: RELAT_1:69

canceled;

theorem :: RELAT_1:70

canceled;

theorem Th71: :: RELAT_1:71

proof end;

theorem :: RELAT_1:72

proof end;

theorem :: RELAT_1:73

for X being set

for R being Relation st ( for x being set st x in X holds

[x,x] in R ) holds

id X c= R

for R being Relation st ( for x being set st x in X holds

[x,x] in R ) holds

id X c= R

proof end;

theorem Th74: :: RELAT_1:74

for x, y, X being set

for R being Relation holds

( [x,y] in (id X) * R iff ( x in X & [x,y] in R ) )

for R being Relation holds

( [x,y] in (id X) * R iff ( x in X & [x,y] in R ) )

proof end;

theorem Th75: :: RELAT_1:75

for x, y, Y being set

for R being Relation holds

( [x,y] in R * (id Y) iff ( y in Y & [x,y] in R ) )

for R being Relation holds

( [x,y] in R * (id Y) iff ( y in Y & [x,y] in R ) )

proof end;

theorem Th76: :: RELAT_1:76

proof end;

theorem Th77: :: RELAT_1:77

proof end;

theorem :: RELAT_1:78

theorem Th79: :: RELAT_1:79

proof end;

theorem :: RELAT_1:80

theorem :: RELAT_1:81

proof end;

theorem :: RELAT_1:82

for X being set

for P2, R, P1 being Relation st rng P2 c= X & P2 * R = id (dom P1) & R * P1 = id X holds

P1 = P2

for P2, R, P1 being Relation st rng P2 c= X & P2 * R = id (dom P1) & R * P1 = id X holds

P1 = P2

proof end;

definition

let R be Relation;

let X be set ;

func R | X -> Relation means :Def11: :: RELAT_1:def 11

for x, y being set holds

( [x,y] in it iff ( x in X & [x,y] in R ) );

existence

ex b_{1} being Relation st

for x, y being set holds

( [x,y] in b_{1} iff ( x in X & [x,y] in R ) )

for b_{1}, b_{2} being Relation st ( for x, y being set holds

( [x,y] in b_{1} iff ( x in X & [x,y] in R ) ) ) & ( for x, y being set holds

( [x,y] in b_{2} iff ( x in X & [x,y] in R ) ) ) holds

b_{1} = b_{2}

end;
let X be set ;

func R | X -> Relation means :Def11: :: RELAT_1:def 11

for x, y being set holds

( [x,y] in it iff ( x in X & [x,y] in R ) );

existence

ex b

for x, y being set holds

( [x,y] in b

proof end;

uniqueness for b

( [x,y] in b

( [x,y] in b

b

proof end;

:: deftheorem Def11 defines | RELAT_1:def 11 :

for R being Relation

for X being set

for b

( b

( [x,y] in b

registration
end;

theorem :: RELAT_1:83

canceled;

theorem :: RELAT_1:84

canceled;

theorem :: RELAT_1:85

canceled;

theorem Th86: :: RELAT_1:86

proof end;

theorem Th87: :: RELAT_1:87

proof end;

theorem Th88: :: RELAT_1:88

proof end;

theorem Th89: :: RELAT_1:89

proof end;

theorem Th90: :: RELAT_1:90

proof end;

theorem :: RELAT_1:91

proof end;

theorem :: RELAT_1:92

theorem :: RELAT_1:93

theorem :: RELAT_1:94

proof end;

theorem :: RELAT_1:95

proof end;

theorem Th96: :: RELAT_1:96

proof end;

theorem Th97: :: RELAT_1:97

proof end;

theorem :: RELAT_1:98

theorem Th99: :: RELAT_1:99

proof end;

theorem Th100: :: RELAT_1:100

proof end;

theorem :: RELAT_1:101

proof end;

theorem :: RELAT_1:102

proof end;

theorem :: RELAT_1:103

proof end;

theorem Th104: :: RELAT_1:104

proof end;

theorem Th105: :: RELAT_1:105

proof end;

theorem Th106: :: RELAT_1:106

proof end;

theorem Th107: :: RELAT_1:107

proof end;

theorem :: RELAT_1:108

proof end;

theorem Th109: :: RELAT_1:109

proof end;

registration
end;

theorem :: RELAT_1:110

theorem :: RELAT_1:111

theorem :: RELAT_1:112

proof end;

definition

let Y be set ;

let R be Relation;

func Y | R -> Relation means :Def12: :: RELAT_1:def 12

for x, y being set holds

( [x,y] in it iff ( y in Y & [x,y] in R ) );

existence

ex b_{1} being Relation st

for x, y being set holds

( [x,y] in b_{1} iff ( y in Y & [x,y] in R ) )

for b_{1}, b_{2} being Relation st ( for x, y being set holds

( [x,y] in b_{1} iff ( y in Y & [x,y] in R ) ) ) & ( for x, y being set holds

( [x,y] in b_{2} iff ( y in Y & [x,y] in R ) ) ) holds

b_{1} = b_{2}

end;
let R be Relation;

func Y | R -> Relation means :Def12: :: RELAT_1:def 12

for x, y being set holds

( [x,y] in it iff ( y in Y & [x,y] in R ) );

existence

ex b

for x, y being set holds

( [x,y] in b

proof end;

uniqueness for b

( [x,y] in b

( [x,y] in b

b

proof end;

:: deftheorem Def12 defines | RELAT_1:def 12 :

for Y being set

for R, b

( b

( [x,y] in b

registration
end;

theorem :: RELAT_1:113

canceled;

theorem :: RELAT_1:114

canceled;

theorem Th115: :: RELAT_1:115

proof end;

theorem Th116: :: RELAT_1:116

proof end;

theorem Th117: :: RELAT_1:117

proof end;

theorem Th118: :: RELAT_1:118

proof end;

theorem Th119: :: RELAT_1:119

proof end;

theorem :: RELAT_1:120

proof end;

theorem :: RELAT_1:121

theorem :: RELAT_1:122

theorem :: RELAT_1:123

proof end;

theorem Th124: :: RELAT_1:124

proof end;

theorem Th125: :: RELAT_1:125

proof end;

theorem :: RELAT_1:126

theorem Th127: :: RELAT_1:127

proof end;

theorem :: RELAT_1:128

proof end;

theorem :: RELAT_1:129

proof end;

theorem :: RELAT_1:130

proof end;

theorem Th131: :: RELAT_1:131

proof end;

theorem Th132: :: RELAT_1:132

proof end;

theorem :: RELAT_1:133

proof end;

theorem :: RELAT_1:134

proof end;

theorem :: RELAT_1:135

proof end;

theorem :: RELAT_1:136

proof end;

theorem :: RELAT_1:137

theorem :: RELAT_1:138

proof end;

theorem :: RELAT_1:139

proof end;

theorem :: RELAT_1:140

proof end;

definition

let R be Relation;

let X be set ;

func R .: X -> set means :Def13: :: RELAT_1:def 13

for y being set holds

( y in it iff ex x being set st

( [x,y] in R & x in X ) );

existence

ex b_{1} being set st

for y being set holds

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

( [x,y] in R & x in X ) )

for b_{1}, b_{2} being set st ( for y being set holds

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

( [x,y] in R & x in X ) ) ) & ( for y being set holds

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

( [x,y] in R & x in X ) ) ) holds

b_{1} = b_{2}

end;
let X be set ;

func R .: X -> set means :Def13: :: RELAT_1:def 13

for y being set holds

( y in it iff ex x being set st

( [x,y] in R & x in X ) );

existence

ex b

for y being set holds

( y in b

( [x,y] in R & x in X ) )

proof end;

uniqueness for b

( y in b

( [x,y] in R & x in X ) ) ) & ( for y being set holds

( y in b

( [x,y] in R & x in X ) ) ) holds

b

proof end;

:: deftheorem Def13 defines .: RELAT_1:def 13 :

for R being Relation

for X, b

( b

( y in b

( [x,y] in R & x in X ) ) );

theorem :: RELAT_1:141

canceled;

theorem :: RELAT_1:142

canceled;

theorem Th143: :: RELAT_1:143

for y, X being set

for R being Relation holds

( y in R .: X iff ex x being set st

( x in dom R & [x,y] in R & x in X ) )

for R being Relation holds

( y in R .: X iff ex x being set st

( x in dom R & [x,y] in R & x in X ) )

proof end;

theorem Th144: :: RELAT_1:144

proof end;

theorem :: RELAT_1:145

proof end;

theorem Th146: :: RELAT_1:146

proof end;

theorem :: RELAT_1:147

proof end;

theorem :: RELAT_1:148

proof end;

theorem :: RELAT_1:149

proof end;

theorem :: RELAT_1:150

proof end;

theorem :: RELAT_1:151

proof end;

theorem :: RELAT_1:152

proof end;

theorem :: RELAT_1:153

proof end;

theorem :: RELAT_1:154

proof end;

theorem :: RELAT_1:155

proof end;

theorem Th156: :: RELAT_1:156

proof end;

theorem Th157: :: RELAT_1:157

proof end;

theorem :: RELAT_1:158

proof end;

theorem :: RELAT_1:159

proof end;

theorem Th160: :: RELAT_1:160

proof end;

theorem :: RELAT_1:161

theorem Th162: :: RELAT_1:162

proof end;

theorem :: RELAT_1:163

proof end;

definition

let R be Relation;

let Y be set ;

func R " Y -> set means :Def14: :: RELAT_1:def 14

for x being set holds

( x in it iff ex y being set st

( [x,y] in R & y in Y ) );

existence

ex b_{1} being set st

for x being set holds

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

( [x,y] in R & y in Y ) )

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

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

( [x,y] in R & y in Y ) ) ) & ( for x being set holds

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

( [x,y] in R & y in Y ) ) ) holds

b_{1} = b_{2}

end;
let Y be set ;

func R " Y -> set means :Def14: :: RELAT_1:def 14

for x being set holds

( x in it iff ex y being set st

( [x,y] in R & y in Y ) );

existence

ex b

for x being set holds

( x in b

( [x,y] in R & y in Y ) )

proof end;

uniqueness for b

( x in b

( [x,y] in R & y in Y ) ) ) & ( for x being set holds

( x in b

( [x,y] in R & y in Y ) ) ) holds

b

proof end;

:: deftheorem Def14 defines " RELAT_1:def 14 :

for R being Relation

for Y, b

( b

( x in b

( [x,y] in R & y in Y ) ) );

theorem :: RELAT_1:164

canceled;

theorem :: RELAT_1:165

canceled;

theorem Th166: :: RELAT_1:166

for x, Y being set

for R being Relation holds

( x in R " Y iff ex y being set st

( y in rng R & [x,y] in R & y in Y ) )

for R being Relation holds

( x in R " Y iff ex y being set st

( y in rng R & [x,y] in R & y in Y ) )

proof end;

theorem Th167: :: RELAT_1:167

proof end;

theorem :: RELAT_1:168

proof end;

theorem Th169: :: RELAT_1:169

proof end;

theorem :: RELAT_1:170

proof end;

theorem :: RELAT_1:171

proof end;

theorem :: RELAT_1:172

proof end;

theorem :: RELAT_1:173

proof end;

theorem :: RELAT_1:174

proof end;

theorem :: RELAT_1:175

proof end;

theorem :: RELAT_1:176

proof end;

theorem :: RELAT_1:177

proof end;

theorem Th178: :: RELAT_1:178

proof end;

theorem Th179: :: RELAT_1:179

proof end;

theorem :: RELAT_1:180

proof end;

theorem :: RELAT_1:181

proof end;

theorem Th182: :: RELAT_1:182

proof end;

theorem :: RELAT_1:183

proof end;

begin

definition
end;

:: deftheorem Def15 defines empty-yielding RELAT_1:def 15 :

for R being Relation holds

( R is empty-yielding iff rng R c= {{}} );

theorem :: RELAT_1:184

proof end;

theorem :: RELAT_1:185

for f, g being Relation

for A, B being set st f | A = g | A & f | B = g | B holds

f | (A \/ B) = g | (A \/ B)

for A, B being set st f | A = g | A & f | B = g | B holds

f | (A \/ B) = g | (A \/ B)

proof end;

theorem :: RELAT_1:186

proof end;

theorem :: RELAT_1:187

proof end;

theorem :: RELAT_1:188

proof end;

theorem :: RELAT_1:189

proof end;

registration

cluster empty Relation-like -> empty-yielding set ;

coherence

for b_{1} being Relation st b_{1} is empty holds

b_{1} is empty-yielding

end;
coherence

for b

b

proof end;

registration

let R be empty-yielding Relation;

let X be set ;

cluster R | X -> empty-yielding ;

coherence

R | X is empty-yielding

end;
let X be set ;

cluster R | X -> empty-yielding ;

coherence

R | X is empty-yielding

proof end;

theorem :: RELAT_1:190

definition

let R be Relation;

let x be set ;

func Im (R,x) -> set equals :: RELAT_1:def 16

R .: {x};

correctness

coherence

R .: {x} is set ;

;

end;
let x be set ;

func Im (R,x) -> set equals :: RELAT_1:def 16

R .: {x};

correctness

coherence

R .: {x} is set ;

;

:: deftheorem defines Im RELAT_1:def 16 :

for R being Relation

for x being set holds Im (R,x) = R .: {x};

scheme :: RELAT_1:sch 2

ExtensionalityR{ F_{1}() -> Relation, F_{2}() -> Relation, P_{1}[ set , set ] } :

provided

ExtensionalityR{ F

provided

A1:
for a, b being set holds

( [a,b] in F_{1}() iff P_{1}[a,b] )
and

A2: for a, b being set holds

( [a,b] in F_{2}() iff P_{1}[a,b] )

( [a,b] in F

A2: for a, b being set holds

( [a,b] in F

proof end;

theorem :: RELAT_1:191

proof end;

theorem :: RELAT_1:192

proof end;

theorem :: RELAT_1:193

proof end;

theorem :: RELAT_1:194

proof end;

theorem :: RELAT_1:195

proof end;

theorem :: RELAT_1:196

proof end;

theorem :: RELAT_1:197

proof end;

theorem :: RELAT_1:198

proof end;

theorem :: RELAT_1:199

proof end;

definition

let R be Relation;

let x be set ;

func Coim (R,x) -> set equals :: RELAT_1:def 17

R " {x};

coherence

R " {x} is set ;

end;
let x be set ;

func Coim (R,x) -> set equals :: RELAT_1:def 17

R " {x};

coherence

R " {x} is set ;

:: deftheorem defines Coim RELAT_1:def 17 :

for R being Relation

for x being set holds Coim (R,x) = R " {x};

registration
end;

registration
end;

theorem :: RELAT_1:200

proof end;

theorem :: RELAT_1:201

proof end;

definition

let X be set ;

let R be Relation;

attr R is X -defined means :Def18: :: RELAT_1:def 18

dom R c= X;

attr R is X -valued means :Def19: :: RELAT_1:def 19

rng R c= X;

end;
let R be Relation;

attr R is X -defined means :Def18: :: RELAT_1:def 18

dom R c= X;

attr R is X -valued means :Def19: :: RELAT_1:def 19

rng R c= X;

:: deftheorem Def18 defines -defined RELAT_1:def 18 :

for X being set

for R being Relation holds

( R is X -defined iff dom R c= X );

:: deftheorem Def19 defines -valued RELAT_1:def 19 :

for X being set

for R being Relation holds

( R is X -valued iff rng R c= X );

Lm2: for X, Y being set holds

( {} is X -defined & {} is Y -valued )

proof end;

registration

let X, Y be set ;

cluster Relation-like X -defined Y -valued set ;

existence

ex b_{1} being Relation st

( b_{1} is X -defined & b_{1} is Y -valued )

end;
cluster Relation-like X -defined Y -valued set ;

existence

ex b

( b

proof end;

theorem :: RELAT_1:202

proof end;

registration

let X, A be set ;

let R be A -valued Relation;

cluster R | X -> A -valued ;

coherence

R | X is A -valued

end;
let R be A -valued Relation;

cluster R | X -> A -valued ;

coherence

R | X is A -valued

proof end;

registration

let X, A be set ;

let R be A -defined Relation;

cluster R | X -> X -defined A -defined ;

coherence

( R | X is A -defined & R | X is X -defined )

end;
let R be A -defined Relation;

cluster R | X -> X -defined A -defined ;

coherence

( R | X is A -defined & R | X is X -defined )

proof end;

registration

let X be set ;

cluster id X -> X -defined X -valued ;

coherence

( id X is X -defined & id X is X -valued )

end;
cluster id X -> X -defined X -valued ;

coherence

( id X is X -defined & id X is X -valued )

proof end;

registration

let A be set ;

let R be A -valued Relation;

let S be Relation;

cluster S * R -> A -valued ;

coherence

S * R is A -valued

end;
let R be A -valued Relation;

let S be Relation;

cluster S * R -> A -valued ;

coherence

S * R is A -valued

proof end;

registration

let A be set ;

let R be A -defined Relation;

let S be Relation;

cluster R * S -> A -defined ;

coherence

R * S is A -defined

end;
let R be A -defined Relation;

let S be Relation;

cluster R * S -> A -defined ;

coherence

R * S is A -defined

proof end;

theorem :: RELAT_1:203

proof end;

theorem Th204: :: RELAT_1:204

proof end;

theorem :: RELAT_1:205

proof end;

theorem :: RELAT_1:206

registration

cluster empty Relation-like -> non-empty set ;

coherence

for b_{1} being Relation st b_{1} is empty holds

b_{1} is non-empty

end;
coherence

for b

b

proof end;

registration

let X be set ;

let R be X -defined Relation;

cluster -> X -defined Element of bool R;

coherence

for b_{1} being Subset of R holds b_{1} is X -defined

end;
let R be X -defined Relation;

cluster -> X -defined Element of bool R;

coherence

for b

proof end;

registration

let X be set ;

let R be X -valued Relation;

cluster -> X -valued Element of bool R;

coherence

for b_{1} being Subset of R holds b_{1} is X -valued

end;
let R be X -valued Relation;

cluster -> X -valued Element of bool R;

coherence

for b

proof end;

theorem :: RELAT_1:207

proof end;

theorem :: RELAT_1:208

proof end;

theorem Th209: :: RELAT_1:209

proof end;

theorem :: RELAT_1:210

proof end;

theorem Th211: :: RELAT_1:211

proof end;

theorem Th212: :: RELAT_1:212

proof end;

theorem :: RELAT_1:213

proof end;

theorem :: RELAT_1:214

proof end;

theorem :: RELAT_1:215

proof end;

theorem :: RELAT_1:216

proof end;

theorem :: RELAT_1:217

proof end;

theorem :: RELAT_1:218

proof end;

theorem :: RELAT_1:219

proof end;