:: RELAT_1 semantic presentation

begin


definition
let IT be set ;
attrIT 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;

:: 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 for set ;
coherence
 for b1 being set st b1 is empty holds
b1 is Relation-like
proof
let X be set ; ::_thesis: ( X is empty implies X is Relation-like )
assume  X is empty ; ::_thesis: X is Relation-like
hence  for p being set st p in X holds
ex x, y being set st [x,y] = p ; :: according to RELAT_1:def_1 ::_thesis: verum
end;
end;

definition
mode Relation is Relation-like set ;
end;


registration
let R be Relation;
cluster  ->  Relation-like for Element of bool R;
coherence
 for b1 being Subset of R holds b1 is Relation-like
proof
let A be Subset of R; ::_thesis: A is Relation-like
let x be set ; :: according to RELAT_1:def_1 ::_thesis: ( x in A implies ex y, z being set st x = [y,z] )
thus  ( x in A implies ex y, z being set st x = [y,z] ) by Def1; ::_thesis: verum
end;
end;

scheme :: RELAT_1:sch 1
RelExistence{ F1() ->  set , F2() ->  set , P1[ set , set ] } :
 ex R being Relation st
for x, y being set holds
( [x,y] in R iff ( x in F1() & y in F2() & P1[x,y] ) )
proof
 ex R being Relation st
for p being set holds
( p in R iff ( p in [:F1(),F2():] & ex x, y being set st
( p = [x,y] & P1[x,y] ) ) )
proof
defpred S1[ set ] means  ex x, y being set st
( $1 = [x,y] & P1[x,y] );
consider B being set  such that
A1: for p being set holds
( p in B iff ( p in [:F1(),F2():] & S1[p] ) ) from XBOOLE_0:sch_1();
 for p being set st p in B holds
ex x, y being set st p = [x,y]
proof
let p be set ; ::_thesis: ( p in B implies ex x, y being set st p = [x,y] )
assume  p in B ; ::_thesis: ex x, y being set st p = [x,y]
then  ex x, y being set st
( p = [x,y] & P1[x,y] ) by A1;
hence  ex x, y being set st p = [x,y] ; ::_thesis: verum
end;
then  B is Relation by Def1;
hence  ex R being Relation st
for p being set holds
( p in R iff ( p in [:F1(),F2():] & ex x, y being set st
( p = [x,y] & P1[x,y] ) ) ) by A1; ::_thesis: verum
end;
then consider R being Relation such that
A2: for p being set holds
( p in R iff ( p in [:F1(),F2():] & ex x, y being set st
( p = [x,y] & P1[x,y] ) ) ) ;
take  R ; ::_thesis: for x, y being set holds
( [x,y] in R iff ( x in F1() & y in F2() & P1[x,y] ) )
let x, y be set ; ::_thesis: ( [x,y] in R iff ( x in F1() & y in F2() & P1[x,y] ) )
thus  ( [x,y] in R implies ( x in F1() & y in F2() & P1[x,y] ) ) ::_thesis: ( x in F1() & y in F2() & P1[x,y] implies [x,y] in R )
proof
assume A3: [x,y] in R ; ::_thesis: ( x in F1() & y in F2() & P1[x,y] )
then consider xx, yy being set  such that
A4: [x,y] = [xx,yy] and
A5: P1[xx,yy] by A2;
A6: [x,y] in [:F1(),F2():] by A2, A3;
 x = xx by A4, XTUPLE_0:1;
hence  ( x in F1() & y in F2() & P1[x,y] ) by A4, A5, A6, XTUPLE_0:1, ZFMISC_1:87; ::_thesis: verum
end;
thus  ( x in F1() & y in F2() & P1[x,y] implies [x,y] in R ) ::_thesis: verum
proof
assume that
A7: ( x in F1() & y in F2() ) and
A8: P1[x,y] ; ::_thesis: [x,y] in R
 [x,y] in [:F1(),F2():] by A7, ZFMISC_1:87;
hence  [x,y] in R by A2, A8; ::_thesis: verum
end;
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 ) )
proof
thus  ( P = R implies for a, b being set holds
( [a,b] in P iff [a,b] in R ) ) ; ::_thesis: ( ( for a, b being set holds
( [a,b] in P iff [a,b] in R ) ) implies P = R )
assume A1: for a, b being set holds
( [a,b] in P iff [a,b] in R ) ; ::_thesis: P = R
thus  P c= R :: according to XBOOLE_0:def_10 ::_thesis: R c= P
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P or x in R )
assume A2: x in P ; ::_thesis: x in R
then  ex y, z being set st x = [y,z] by Def1;
hence  x in R by A1, A2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in R or x in P )
assume A3: x in R ; ::_thesis: x in P
then  ex y, z being set st x = [y,z] by Def1;
hence  x in P by A1, A3; ::_thesis: verum
end;
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 ;
clusterP /\ X ->  Relation-like ;
coherence
 P /\ X is Relation-like
proof
 P /\ X c= P by XBOOLE_1:17;
hence  P /\ X is Relation-like ; ::_thesis: verum
end;
clusterP \ X ->  Relation-like ;
coherence
 P \ X is Relation-like ;
end;

registration
let P, R be Relation;
clusterP \/ R ->  Relation-like ;
coherence
 P \/ R is Relation-like
proof
let x be set ; :: according to RELAT_1:def_1 ::_thesis: ( x in P \/ R implies ex y, z being set st x = [y,z] )
A1: ( x in R implies ex y, z being set st x = [y,z] ) by Def1;
 ( x in P implies ex y, z being set st x = [y,z] ) by Def1;
hence  ( x in P \/ R implies ex y, z being set st x = [y,z] ) by A1, XBOOLE_0:def_3; ::_thesis: verum
end;
end;

registration
let R, S be Relation;
clusterR \+\ S ->  Relation-like ;
coherence
 R \+\ S is Relation-like ;
end;

registration
let a, b be set ;
cluster{[a,b]} ->  Relation-like ;
coherence
 {[a,b]} is Relation-like
proof
let x be set ; :: according to RELAT_1:def_1 ::_thesis: ( x in {[a,b]} implies ex y, z being set st x = [y,z] )
assume  x in {[a,b]} ; ::_thesis: ex y, z being set st x = [y,z]
then  x = [a,b] by TARSKI:def_1;
hence  ex y, z being set st x = [y,z] ; ::_thesis: verum
end;
cluster[:a,b:] ->  Relation-like ;
coherence
 [:a,b:] is Relation-like
proof
let z be set ; :: according to RELAT_1:def_1 ::_thesis: ( z in [:a,b:] implies ex y, z being set st z = [y,z] )
assume  z in [:a,b:] ; ::_thesis: ex y, z being set st z = [y,z]
then  ex x, y being set st
( x in a & y in b & [x,y] = z ) by ZFMISC_1:def_2;
hence  ex y, z being set st z = [y,z] ; ::_thesis: verum
end;
end;

registration
let a, b, c, d be set ;
cluster{[a,b],[c,d]} ->  Relation-like ;
coherence
 {[a,b],[c,d]} is Relation-like
proof
 {[a,b],[c,d]} = {[a,b]} \/ {[c,d]} by ENUMSET1:1;
hence  {[a,b],[c,d]} is Relation-like ; ::_thesis: verum
end;
end;

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 )
proof
thus  ( P c= A implies for a, b being set st [a,b] in P holds
[a,b] in A ) ; ::_thesis: ( ( for a, b being set st [a,b] in P holds
[a,b] in A ) implies P c= A )
assume A1: for a, b being set st [a,b] in P holds
[a,b] in A ; ::_thesis: P c= A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P or x in A )
assume A2: x in P ; ::_thesis: x in A
then  ex y, z being set st x = [y,z] by Def1;
hence  x in A by A1, A2; ::_thesis: verum
end;
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 );

notation
let R be Relation;
synonym  dom R for  proj1 R;
end;

theorem Th1: :: RELAT_1:1
for P, R being Relation holds dom (P \/ R) = (dom P) \/ (dom R) by XTUPLE_0:23;

theorem Th2: :: RELAT_1:2
for P, R being Relation holds dom (P /\ R) c= (dom P) /\ (dom R) by XTUPLE_0:24;

theorem :: RELAT_1:3
for P, R being Relation holds (dom P) \ (dom R) c= dom (P \ R) by XTUPLE_0:25;

notation
let R be Relation;
synonym  rng R for  proj2 R;
end;

theorem :: RELAT_1:4
canceled;

theorem :: RELAT_1:5
canceled;

theorem :: RELAT_1:6
canceled;

theorem Th7: :: RELAT_1:7
for R being Relation holds R c= [:(dom R),(rng R):]
proof
let R be Relation; ::_thesis: R c= [:(dom R),(rng R):]
let y be set ; :: according to RELAT_1:def_3 ::_thesis: for b being set st [y,b] in R holds
[y,b] in [:(dom R),(rng R):]
let z be set ; ::_thesis: ( [y,z] in R implies [y,z] in [:(dom R),(rng R):] )
assume  [y,z] in R ; ::_thesis: [y,z] in [:(dom R),(rng R):]
then  ( y in dom R & z in rng R ) by XTUPLE_0:def_12, XTUPLE_0:def_13;
hence  [y,z] in [:(dom R),(rng R):] by ZFMISC_1:87; ::_thesis: verum
end;

theorem :: RELAT_1:8
for R being Relation holds R /\ [:(dom R),(rng R):] = R by Th7, XBOOLE_1:28;

theorem Th9: :: RELAT_1:9
for x, y being set
for R being Relation st R = {[x,y]} holds
( dom R = {x} & rng R = {y} )
proof
let x, y be set ; ::_thesis: for R being Relation st R = {[x,y]} holds
( dom R = {x} & rng R = {y} )
let R be Relation; ::_thesis: ( R = {[x,y]} implies ( dom R = {x} & rng R = {y} ) )
assume A1: R = {[x,y]} ; ::_thesis: ( dom R = {x} & rng R = {y} )
 for z being set holds
( z in dom R iff z in {x} )
proof
let z be set ; ::_thesis: ( z in dom R iff z in {x} )
thus  ( z in dom R implies z in {x} ) ::_thesis: ( z in {x} implies z in dom R )
proof
assume  z in dom R ; ::_thesis: z in {x}
then consider b being set  such that
A2: [z,b] in R by XTUPLE_0:def_12;
 [z,b] = [x,y] by A1, A2, TARSKI:def_1;
then  z = x by XTUPLE_0:1;
hence  z in {x} by TARSKI:def_1; ::_thesis: verum
end;
assume  z in {x} ; ::_thesis: z in dom R
then  z = x by TARSKI:def_1;
then  [z,y] in R by A1, TARSKI:def_1;
hence  z in dom R by XTUPLE_0:def_12; ::_thesis: verum
end;
hence  dom R = {x} by TARSKI:1; ::_thesis: rng R = {y}
 for z being set holds
( z in rng R iff z in {y} )
proof
let z be set ; ::_thesis: ( z in rng R iff z in {y} )
thus  ( z in rng R implies z in {y} ) ::_thesis: ( z in {y} implies z in rng R )
proof
assume  z in rng R ; ::_thesis: z in {y}
then consider a being set  such that
A3: [a,z] in R by XTUPLE_0:def_13;
 [a,z] = [x,y] by A1, A3, TARSKI:def_1;
then  z = y by XTUPLE_0:1;
hence  z in {y} by TARSKI:def_1; ::_thesis: verum
end;
assume  z in {y} ; ::_thesis: z in rng R
then  z = y by TARSKI:def_1;
then  [x,z] in R by A1, TARSKI:def_1;
hence  z in rng R by XTUPLE_0:def_13; ::_thesis: verum
end;
hence  rng R = {y} by TARSKI:1; ::_thesis: verum
end;

theorem :: RELAT_1:10
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} )
proof
let a, b, x, y be set ; ::_thesis: for R being Relation st R = {[a,b],[x,y]} holds
( dom R = {a,x} & rng R = {b,y} )
let R be Relation; ::_thesis: ( R = {[a,b],[x,y]} implies ( dom R = {a,x} & rng R = {b,y} ) )
assume A1: R = {[a,b],[x,y]} ; ::_thesis: ( dom R = {a,x} & rng R = {b,y} )
thus  dom R = {a,x} ::_thesis: rng R = {b,y}
proof
thus  dom R c= {a,x} :: according to XBOOLE_0:def_10 ::_thesis: {a,x} c= dom R
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in dom R or z in {a,x} )
assume  z in dom R ; ::_thesis: z in {a,x}
then consider c being set  such that
A2: [z,c] in R by XTUPLE_0:def_12;
 ( [z,c] = [a,b] or [z,c] = [x,y] ) by A1, A2, TARSKI:def_2;
then  ( z = a or z = x ) by XTUPLE_0:1;
hence  z in {a,x} by TARSKI:def_2; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in {a,x} or z in dom R )
assume  z in {a,x} ; ::_thesis: z in dom R
then  ( z = a or z = x ) by TARSKI:def_2;
then  ( [z,b] in R or [z,y] in R ) by A1, TARSKI:def_2;
hence  z in dom R by XTUPLE_0:def_12; ::_thesis: verum
end;
thus  rng R c= {b,y} :: according to XBOOLE_0:def_10 ::_thesis: {b,y} c= rng R
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng R or z in {b,y} )
assume  z in rng R ; ::_thesis: z in {b,y}
then consider d being set  such that
A3: [d,z] in R by XTUPLE_0:def_13;
 ( [d,z] = [a,b] or [d,z] = [x,y] ) by A1, A3, TARSKI:def_2;
then  ( z = b or z = y ) by XTUPLE_0:1;
hence  z in {b,y} by TARSKI:def_2; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in {b,y} or z in rng R )
assume  z in {b,y} ; ::_thesis: z in rng R
then  ( z = b or z = y ) by TARSKI:def_2;
then  ( [a,z] in R or [x,z] in R ) by A1, TARSKI:def_2;
hence  z in rng R by XTUPLE_0:def_13; ::_thesis: verum
end;

theorem Th11: :: RELAT_1:11
for P, R being Relation st P c= R holds
( dom P c= dom R & rng P c= rng R ) by XTUPLE_0:8, XTUPLE_0:9;

theorem Th12: :: RELAT_1:12
for P, R being Relation holds rng (P \/ R) = (rng P) \/ (rng R) by XTUPLE_0:27;

theorem Th13: :: RELAT_1:13
for P, R being Relation holds rng (P /\ R) c= (rng P) /\ (rng R) by XTUPLE_0:28;

theorem :: RELAT_1:14
for P, R being Relation holds (rng P) \ (rng R) c= rng (P \ R) by XTUPLE_0:29;

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

:: deftheorem  RELAT_1:def_4_:_
canceled;

:: deftheorem  RELAT_1:def_5_:_
canceled;

:: deftheorem  defines field RELAT_1:def_6_:_
 for R being Relation holds field R = (dom R) \/ (rng R);

theorem :: RELAT_1:15
for a, b being set
for R being Relation st [a,b] in R holds
( a in field R & b in field R )
proof
let a, b be set ; ::_thesis: for R being Relation st [a,b] in R holds
( a in field R & b in field R )
let R be Relation; ::_thesis: ( [a,b] in R implies ( a in field R & b in field R ) )
assume A1: [a,b] in R ; ::_thesis: ( a in field R & b in field R )
then  a in dom R by XTUPLE_0:def_12;
hence  a in field R by XBOOLE_0:def_3; ::_thesis: b in field R
 b in rng R by A1, XTUPLE_0:def_13;
hence  b in field R by XBOOLE_0:def_3; ::_thesis: verum
end;

theorem :: RELAT_1:16
for P, R being Relation st P c= R holds
field P c= field R
proof
let P, R be Relation; ::_thesis: ( P c= R implies field P c= field R )
assume  P c= R ; ::_thesis: field P c= field R
then  ( dom P c= dom R & rng P c= rng R ) by Th11;
hence  field P c= field R by XBOOLE_1:13; ::_thesis: verum
end;

theorem Th17: :: RELAT_1:17
for x, y being set holds field {[x,y]} = {x,y}
proof
let x, y be set ; ::_thesis: field {[x,y]} = {x,y}
set R = {[x,y]};
 ( dom {[x,y]} = {x} & rng {[x,y]} = {y} ) by Th9;
hence  field {[x,y]} = {x,y} by ENUMSET1:1; ::_thesis: verum
end;

theorem :: RELAT_1:18
for P, R being Relation holds field (P \/ R) = (field P) \/ (field R)
proof
let P, R be Relation; ::_thesis: field (P \/ R) = (field P) \/ (field R)
thus  field (P \/ R) = ((dom P) \/ (dom R)) \/ (rng (P \/ R)) by Th1
.= ((dom P) \/ (dom R)) \/ ((rng P) \/ (rng R)) by Th12
.= (((dom P) \/ (dom R)) \/ (rng P)) \/ (rng R) by XBOOLE_1:4
.= ((field P) \/ (dom R)) \/ (rng R) by XBOOLE_1:4
.= (field P) \/ (field R) by XBOOLE_1:4 ; ::_thesis: verum
end;

theorem :: RELAT_1:19
for P, R being Relation holds field (P /\ R) c= (field P) /\ (field R)
proof
let P, R be Relation; ::_thesis: field (P /\ R) c= (field P) /\ (field R)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in field (P /\ R) or x in (field P) /\ (field R) )
assume  x in field (P /\ R) ; ::_thesis: x in (field P) /\ (field R)
then A1: ( x in dom (P /\ R) or x in rng (P /\ R) ) by XBOOLE_0:def_3;
 ( ( x in (dom P) /\ (dom R) or x in (rng P) /\ (rng R) ) implies ( ( x in dom P or x in rng P ) & ( x in dom R or x in rng R ) ) ) by XBOOLE_0:def_4;
then A2: ( ( x in (dom P) /\ (dom R) or x in (rng P) /\ (rng R) ) implies ( x in (dom P) \/ (rng P) & x in (dom R) \/ (rng R) ) ) by XBOOLE_0:def_3;
 ( dom (P /\ R) c= (dom P) /\ (dom R) & rng (P /\ R) c= (rng P) /\ (rng R) ) by Th2, Th13;
hence  x in (field P) /\ (field R) by A1, A2, XBOOLE_0:def_4; ::_thesis: verum
end;

definition
let R be Relation;
funcR ~  ->  Relation means :Def7: :: RELAT_1:def 7
 for x, y being set holds
( [x,y] in it iff [y,x] in R );
existence
 ex b1 being Relation st
for x, y being set holds
( [x,y] in b1 iff [y,x] in R )
proof
defpred S1[ set , set ] means [$2,$1] in R;
consider P being Relation such that
A1: for x, y being set holds
( [x,y] in P iff ( x in rng R & y in dom R & S1[x,y] ) ) from RELAT_1:sch_1();
take  P ; ::_thesis: for x, y being set holds
( [x,y] in P iff [y,x] in R )
let x, y be set ; ::_thesis: ( [x,y] in P iff [y,x] in R )
 ( [y,x] in R implies ( y in dom R & x in rng R ) ) by XTUPLE_0:def_12, XTUPLE_0:def_13;
hence  ( [x,y] in P iff [y,x] in R ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Relation st ( for x, y being set holds
( [x,y] in b1 iff [y,x] in R ) ) & ( for x, y being set holds
( [x,y] in b2 iff [y,x] in R ) ) holds
b1 = b2
proof
let P1, P2 be Relation; ::_thesis: ( ( for x, y being set holds
( [x,y] in P1 iff [y,x] in R ) ) & ( for x, y being set holds
( [x,y] in P2 iff [y,x] in R ) ) implies P1 = P2 )
assume that
A2: for x, y being set holds
( [x,y] in P1 iff [y,x] in R ) and
A3: for x, y being set holds
( [x,y] in P2 iff [y,x] in R ) ; ::_thesis: P1 = P2
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b being set holds
( [x,b] in P1 iff [x,b] in P2 )
let y be set ; ::_thesis: ( [x,y] in P1 iff [x,y] in P2 )
 ( [x,y] in P1 iff [y,x] in R ) by A2;
hence  ( [x,y] in P1 iff [x,y] in P2 ) by A3; ::_thesis: verum
end;
involutiveness
 for b1, b2 being Relation st ( for x, y being set holds
( [x,y] in b1 iff [y,x] in b2 ) ) holds
for x, y being set holds
( [x,y] in b2 iff [y,x] in b1 ) ;
end;

:: deftheorem Def7 defines ~ RELAT_1:def_7_:_
 for R, b2 being Relation holds
( b2 = R ~ iff for x, y being set holds
( [x,y] in b2 iff [y,x] in R ) );

theorem Th20: :: RELAT_1:20
for R being Relation holds
( rng R = dom (R ~) & dom R = rng (R ~) )
proof
let R be Relation; ::_thesis: ( rng R = dom (R ~) & dom R = rng (R ~) )
thus  rng R c= dom (R ~) :: according to XBOOLE_0:def_10 ::_thesis: ( dom (R ~) c= rng R & dom R = rng (R ~) )
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in rng R or u in dom (R ~) )
assume  u in rng R ; ::_thesis: u in dom (R ~)
then consider x being set  such that
A1: [x,u] in R by XTUPLE_0:def_13;
 [u,x] in R ~ by A1, Def7;
hence  u in dom (R ~) by XTUPLE_0:def_12; ::_thesis: verum
end;
thus  dom (R ~) c= rng R ::_thesis: dom R = rng (R ~)
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in dom (R ~) or u in rng R )
assume  u in dom (R ~) ; ::_thesis: u in rng R
then consider x being set  such that
A2: [u,x] in R ~ by XTUPLE_0:def_12;
 [x,u] in R by A2, Def7;
hence  u in rng R by XTUPLE_0:def_13; ::_thesis: verum
end;
thus  dom R c= rng (R ~) :: according to XBOOLE_0:def_10 ::_thesis: rng (R ~) c= dom R
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in dom R or u in rng (R ~) )
assume  u in dom R ; ::_thesis: u in rng (R ~)
then consider x being set  such that
A3: [u,x] in R by XTUPLE_0:def_12;
 [x,u] in R ~ by A3, Def7;
hence  u in rng (R ~) by XTUPLE_0:def_13; ::_thesis: verum
end;
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in rng (R ~) or u in dom R )
assume  u in rng (R ~) ; ::_thesis: u in dom R
then consider x being set  such that
A4: [x,u] in R ~ by XTUPLE_0:def_13;
 [u,x] in R by A4, Def7;
hence  u in dom R by XTUPLE_0:def_12; ::_thesis: verum
end;

theorem :: RELAT_1:21
for R being Relation holds field R = field (R ~)
proof
let R be Relation; ::_thesis: field R = field (R ~)
thus  field R = (rng (R ~)) \/ (rng R) by Th20
.= field (R ~) by Th20 ; ::_thesis: verum
end;

theorem :: RELAT_1:22
for P, R being Relation holds (P /\ R) ~ = (P ~) /\ (R ~)
proof
let P, R be Relation; ::_thesis: (P /\ R) ~ = (P ~) /\ (R ~)
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b being set holds
( [x,b] in (P /\ R) ~ iff [x,b] in (P ~) /\ (R ~) )
let y be set ; ::_thesis: ( [x,y] in (P /\ R) ~ iff [x,y] in (P ~) /\ (R ~) )
 ( [x,y] in (P /\ R) ~ iff [y,x] in P /\ R ) by Def7;
then  ( [x,y] in (P /\ R) ~ iff ( [y,x] in P & [y,x] in R ) ) by XBOOLE_0:def_4;
then  ( [x,y] in (P /\ R) ~ iff ( [x,y] in P ~ & [x,y] in R ~ ) ) by Def7;
hence  ( [x,y] in (P /\ R) ~ iff [x,y] in (P ~) /\ (R ~) ) by XBOOLE_0:def_4; ::_thesis: verum
end;

theorem :: RELAT_1:23
for P, R being Relation holds (P \/ R) ~ = (P ~) \/ (R ~)
proof
let P, R be Relation; ::_thesis: (P \/ R) ~ = (P ~) \/ (R ~)
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b being set holds
( [x,b] in (P \/ R) ~ iff [x,b] in (P ~) \/ (R ~) )
let y be set ; ::_thesis: ( [x,y] in (P \/ R) ~ iff [x,y] in (P ~) \/ (R ~) )
 ( [x,y] in (P \/ R) ~ iff [y,x] in P \/ R ) by Def7;
then  ( [x,y] in (P \/ R) ~ iff ( [y,x] in P or [y,x] in R ) ) by XBOOLE_0:def_3;
then  ( [x,y] in (P \/ R) ~ iff ( [x,y] in P ~ or [x,y] in R ~ ) ) by Def7;
hence  ( [x,y] in (P \/ R) ~ iff [x,y] in (P ~) \/ (R ~) ) by XBOOLE_0:def_3; ::_thesis: verum
end;

theorem :: RELAT_1:24
for P, R being Relation holds (P \ R) ~ = (P ~) \ (R ~)
proof
let P, R be Relation; ::_thesis: (P \ R) ~ = (P ~) \ (R ~)
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b being set holds
( [x,b] in (P \ R) ~ iff [x,b] in (P ~) \ (R ~) )
let y be set ; ::_thesis: ( [x,y] in (P \ R) ~ iff [x,y] in (P ~) \ (R ~) )
 ( [x,y] in (P \ R) ~ iff [y,x] in P \ R ) by Def7;
then  ( [x,y] in (P \ R) ~ iff ( [y,x] in P & not [y,x] in R ) ) by XBOOLE_0:def_5;
then  ( [x,y] in (P \ R) ~ iff ( [x,y] in P ~ & not [x,y] in R ~ ) ) by Def7;
hence  ( [x,y] in (P \ R) ~ iff [x,y] in (P ~) \ (R ~) ) by XBOOLE_0:def_5; ::_thesis: verum
end;

definition
let P, R be set ;
funcP (#) 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 b1 being Relation st
for x, y being set holds
( [x,y] in b1 iff ex z being set st
( [x,z] in P & [z,y] in R ) )
proof
defpred S1[ set , set ] means  ex z being set st
( [$1,z] in P & [z,$2] in R );
consider Q being Relation such that
A1: for x, y being set holds
( [x,y] in Q iff ( x in proj1 P & y in proj2 R & S1[x,y] ) ) from RELAT_1:sch_1();
take  Q ; ::_thesis: for x, y being set holds
( [x,y] in Q iff ex z being set st
( [x,z] in P & [z,y] in R ) )
let x, y be set ; ::_thesis: ( [x,y] in Q iff ex z being set st
( [x,z] in P & [z,y] in R ) )
thus  ( [x,y] in Q implies ex z being set st
( [x,z] in P & [z,y] in R ) ) by A1; ::_thesis: ( ex z being set st
( [x,z] in P & [z,y] in R ) implies [x,y] in Q )
given z being set  such that A2: ( [x,z] in P & [z,y] in R ) ; ::_thesis: [x,y] in Q
 ( x in proj1 P & y in proj2 R ) by A2, XTUPLE_0:def_12, XTUPLE_0:def_13;
hence  [x,y] in Q by A1, A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Relation st ( for x, y being set holds
( [x,y] in b1 iff ex z being set st
( [x,z] in P & [z,y] in R ) ) ) & ( for x, y being set holds
( [x,y] in b2 iff ex z being set st
( [x,z] in P & [z,y] in R ) ) ) holds
b1 = b2
proof
let P1, P2 be Relation; ::_thesis: ( ( for x, y being set holds
( [x,y] in P1 iff ex z being set st
( [x,z] in P & [z,y] in R ) ) ) & ( for x, y being set holds
( [x,y] in P2 iff ex z being set st
( [x,z] in P & [z,y] in R ) ) ) implies P1 = P2 )
assume that
A3: for x, y being set holds
( [x,y] in P1 iff ex z being set st
( [x,z] in P & [z,y] in R ) ) and
A4: for x, y being set holds
( [x,y] in P2 iff ex z being set st
( [x,z] in P & [z,y] in R ) ) ; ::_thesis: P1 = P2
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b being set holds
( [x,b] in P1 iff [x,b] in P2 )
let y be set ; ::_thesis: ( [x,y] in P1 iff [x,y] in P2 )
 ( [x,y] in P1 iff ex z being set st
( [x,z] in P & [z,y] in R ) ) by A3;
hence  ( [x,y] in P1 iff [x,y] in P2 ) by A4; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines (#) RELAT_1:def_8_:_
 for P, R being set
for b3 being Relation holds
( b3 = P (#) R iff for x, y being set holds
( [x,y] in b3 iff ex z being set st
( [x,z] in P & [z,y] in R ) ) );

notation
let P, R be Relation;
synonym P * R for P (#) R;
end;

theorem Th25: :: RELAT_1:25
for P, R being Relation holds dom (P * R) c= dom P
proof
let P, R be Relation; ::_thesis: dom (P * R) c= dom P
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (P * R) or x in dom P )
assume  x in dom (P * R) ; ::_thesis: x in dom P
then consider y being set  such that
A1: [x,y] in P * R by XTUPLE_0:def_12;
 ex z being set st
( [x,z] in P & [z,y] in R ) by A1, Def8;
hence  x in dom P by XTUPLE_0:def_12; ::_thesis: verum
end;

theorem Th26: :: RELAT_1:26
for P, R being Relation holds rng (P * R) c= rng R
proof
let P, R be Relation; ::_thesis: rng (P * R) c= rng R
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (P * R) or y in rng R )
assume  y in rng (P * R) ; ::_thesis: y in rng R
then consider x being set  such that
A1: [x,y] in P * R by XTUPLE_0:def_13;
 ex z being set st
( [x,z] in P & [z,y] in R ) by A1, Def8;
hence  y in rng R by XTUPLE_0:def_13; ::_thesis: verum
end;

theorem :: RELAT_1:27
for R, P being Relation st rng R c= dom P holds
dom (R * P) = dom R
proof
let R, P be Relation; ::_thesis: ( rng R c= dom P implies dom (R * P) = dom R )
assume A1: for y being set st y in rng R holds
y in dom P ; :: according to TARSKI:def_3 ::_thesis: dom (R * P) = dom R
thus  dom (R * P) c= dom R by Th25; :: according to XBOOLE_0:def_10 ::_thesis: dom R c= dom (R * P)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom R or x in dom (R * P) )
assume  x in dom R ; ::_thesis: x in dom (R * P)
then consider y being set  such that
A2: [x,y] in R by XTUPLE_0:def_12;
 y in rng R by A2, XTUPLE_0:def_13;
then  y in dom P by A1;
then consider z being set  such that
A3: [y,z] in P by XTUPLE_0:def_12;
 [x,z] in R * P by A2, A3, Def8;
hence  x in dom (R * P) by XTUPLE_0:def_12; ::_thesis: verum
end;

theorem :: RELAT_1:28
for P, R being Relation st dom P c= rng R holds
rng (R * P) = rng P
proof
let P, R be Relation; ::_thesis: ( dom P c= rng R implies rng (R * P) = rng P )
assume A1: for y being set st y in dom P holds
y in rng R ; :: according to TARSKI:def_3 ::_thesis: rng (R * P) = rng P
thus  rng (R * P) c= rng P by Th26; :: according to XBOOLE_0:def_10 ::_thesis: rng P c= rng (R * P)
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng P or z in rng (R * P) )
assume  z in rng P ; ::_thesis: z in rng (R * P)
then consider y being set  such that
A2: [y,z] in P by XTUPLE_0:def_13;
 y in dom P by A2, XTUPLE_0:def_12;
then  y in rng R by A1;
then consider x being set  such that
A3: [x,y] in R by XTUPLE_0:def_13;
 [x,z] in R * P by A2, A3, Def8;
hence  z in rng (R * P) by XTUPLE_0:def_13; ::_thesis: verum
end;

theorem Th29: :: RELAT_1:29
for P, R, Q being Relation st P c= R holds
Q * P c= Q * R
proof
let P, R, Q be Relation; ::_thesis: ( P c= R implies Q * P c= Q * R )
assume A1: P c= R ; ::_thesis: Q * P c= Q * R
let x be set ; :: according to RELAT_1:def_3 ::_thesis: for b being set st [x,b] in Q * P holds
[x,b] in Q * R
let y be set ; ::_thesis: ( [x,y] in Q * P implies [x,y] in Q * R )
assume  [x,y] in Q * P ; ::_thesis: [x,y] in Q * R
then  ex z being set st
( [x,z] in Q & [z,y] in P ) by Def8;
hence  [x,y] in Q * R by A1, Def8; ::_thesis: verum
end;

theorem Th30: :: RELAT_1:30
for P, Q, R being Relation st P c= Q holds
P * R c= Q * R
proof
let P, Q, R be Relation; ::_thesis: ( P c= Q implies P * R c= Q * R )
assume A1: P c= Q ; ::_thesis: P * R c= Q * R
let x be set ; :: according to RELAT_1:def_3 ::_thesis: for b being set st [x,b] in P * R holds
[x,b] in Q * R
let y be set ; ::_thesis: ( [x,y] in P * R implies [x,y] in Q * R )
assume  [x,y] in P * R ; ::_thesis: [x,y] in Q * R
then  ex z being set st
( [x,z] in P & [z,y] in R ) by Def8;
hence  [x,y] in Q * R by A1, Def8; ::_thesis: verum
end;

theorem :: RELAT_1:31
for P, R, Q, S being Relation st P c= R & Q c= S holds
P * Q c= R * S
proof
let P, R, Q, S be Relation; ::_thesis: ( P c= R & Q c= S implies P * Q c= R * S )
assume A1: ( P c= R & Q c= S ) ; ::_thesis: P * Q c= R * S
let x be set ; :: according to RELAT_1:def_3 ::_thesis: for b being set st [x,b] in P * Q holds
[x,b] in R * S
let y be set ; ::_thesis: ( [x,y] in P * Q implies [x,y] in R * S )
assume  [x,y] in P * Q ; ::_thesis: [x,y] in R * S
then  ex z being set st
( [x,z] in P & [z,y] in Q ) by Def8;
hence  [x,y] in R * S by A1, Def8; ::_thesis: verum
end;

theorem :: RELAT_1:32
for P, R, Q being Relation holds P * (R \/ Q) = (P * R) \/ (P * Q)
proof
let P, R, Q be Relation; ::_thesis: P * (R \/ Q) = (P * R) \/ (P * Q)
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b being set holds
( [x,b] in P * (R \/ Q) iff [x,b] in (P * R) \/ (P * Q) )
let y be set ; ::_thesis: ( [x,y] in P * (R \/ Q) iff [x,y] in (P * R) \/ (P * Q) )
hereby  ::_thesis: ( [x,y] in (P * R) \/ (P * Q) implies [x,y] in P * (R \/ Q) )
assume  [x,y] in P * (R \/ Q) ; ::_thesis: [x,y] in (P * R) \/ (P * Q)
then consider z being set  such that
A1: [x,z] in P and
A2: [z,y] in R \/ Q by Def8;
 ( [z,y] in R or [z,y] in Q ) by A2, XBOOLE_0:def_3;
then  ( [x,y] in P * R or [x,y] in P * Q ) by A1, Def8;
hence  [x,y] in (P * R) \/ (P * Q) by XBOOLE_0:def_3; ::_thesis: verum
end;
assume A3: [x,y] in (P * R) \/ (P * Q) ; ::_thesis: [x,y] in P * (R \/ Q)
percases ( [x,y] in P * Q or [x,y] in P * R ) by A3, XBOOLE_0:def_3;
suppose [x,y] in P * Q ; ::_thesis: [x,y] in P * (R \/ Q)
then consider z being set  such that
A4: [x,z] in P and
A5: [z,y] in Q by Def8;
 [z,y] in R \/ Q by A5, XBOOLE_0:def_3;
hence  [x,y] in P * (R \/ Q) by A4, Def8; ::_thesis: verum
end;
suppose [x,y] in P * R ; ::_thesis: [x,y] in P * (R \/ Q)
then consider z being set  such that
A6: [x,z] in P and
A7: [z,y] in R by Def8;
 [z,y] in R \/ Q by A7, XBOOLE_0:def_3;
hence  [x,y] in P * (R \/ Q) by A6, Def8; ::_thesis: verum
end;
end;
end;

theorem :: RELAT_1:33
for P, R, Q being Relation holds P * (R /\ Q) c= (P * R) /\ (P * Q)
proof
let P, R, Q be Relation; ::_thesis: P * (R /\ Q) c= (P * R) /\ (P * Q)
let x be set ; :: according to RELAT_1:def_3 ::_thesis: for b being set st [x,b] in P * (R /\ Q) holds
[x,b] in (P * R) /\ (P * Q)
let y be set ; ::_thesis: ( [x,y] in P * (R /\ Q) implies [x,y] in (P * R) /\ (P * Q) )
assume  [x,y] in P * (R /\ Q) ; ::_thesis: [x,y] in (P * R) /\ (P * Q)
then consider z being set  such that
A1: [x,z] in P and
A2: [z,y] in R /\ Q by Def8;
 [z,y] in Q by A2, XBOOLE_0:def_4;
then A3: [x,y] in P * Q by A1, Def8;
 [z,y] in R by A2, XBOOLE_0:def_4;
then  [x,y] in P * R by A1, Def8;
hence  [x,y] in (P * R) /\ (P * Q) by A3, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem :: RELAT_1:34
for P, R, Q being Relation holds (P * R) \ (P * Q) c= P * (R \ Q)
proof
let P, R, Q be Relation; ::_thesis: (P * R) \ (P * Q) c= P * (R \ Q)
let a be set ; :: according to RELAT_1:def_3 ::_thesis: for b being set st [a,b] in (P * R) \ (P * Q) holds
[a,b] in P * (R \ Q)
let b be set ; ::_thesis: ( [a,b] in (P * R) \ (P * Q) implies [a,b] in P * (R \ Q) )
assume A1: [a,b] in (P * R) \ (P * Q) ; ::_thesis: [a,b] in P * (R \ Q)
then consider y being set  such that
A2: [a,y] in P and
A3: [y,b] in R by Def8;
 not [a,b] in P * Q by A1, XBOOLE_0:def_5;
then  ( not [a,y] in P or not [y,b] in Q ) by Def8;
then  [y,b] in R \ Q by A2, A3, XBOOLE_0:def_5;
hence  [a,b] in P * (R \ Q) by A2, Def8; ::_thesis: verum
end;

theorem :: RELAT_1:35
for P, R being Relation holds (P * R) ~ = (R ~) * (P ~)
proof
let P, R be Relation; ::_thesis: (P * R) ~ = (R ~) * (P ~)
let a be set ; :: according to RELAT_1:def_2 ::_thesis: for b being set holds
( [a,b] in (P * R) ~ iff [a,b] in (R ~) * (P ~) )
let b be set ; ::_thesis: ( [a,b] in (P * R) ~ iff [a,b] in (R ~) * (P ~) )
hereby  ::_thesis: ( [a,b] in (R ~) * (P ~) implies [a,b] in (P * R) ~ )
assume  [a,b] in (P * R) ~ ; ::_thesis: [a,b] in (R ~) * (P ~)
then  [b,a] in P * R by Def7;
then consider y being set  such that
A1: ( [b,y] in P & [y,a] in R ) by Def8;
 ( [y,b] in P ~ & [a,y] in R ~ ) by A1, Def7;
hence  [a,b] in (R ~) * (P ~) by Def8; ::_thesis: verum
end;
assume  [a,b] in (R ~) * (P ~) ; ::_thesis: [a,b] in (P * R) ~
then consider y being set  such that
A2: ( [a,y] in R ~ & [y,b] in P ~ ) by Def8;
 ( [y,a] in R & [b,y] in P ) by A2, Def7;
then  [b,a] in P * R by Def8;
hence  [a,b] in (P * R) ~ by Def7; ::_thesis: verum
end;

theorem Th36: :: RELAT_1:36
for P, R, Q being Relation holds (P * R) * Q = P * (R * Q)
proof
let P, R, Q be Relation; ::_thesis: (P * R) * Q = P * (R * Q)
let a be set ; :: according to RELAT_1:def_2 ::_thesis: for b being set holds
( [a,b] in (P * R) * Q iff [a,b] in P * (R * Q) )
let b be set ; ::_thesis: ( [a,b] in (P * R) * Q iff [a,b] in P * (R * Q) )
hereby  ::_thesis: ( [a,b] in P * (R * Q) implies [a,b] in (P * R) * Q )
assume  [a,b] in (P * R) * Q ; ::_thesis: [a,b] in P * (R * Q)
then consider y being set  such that
A1: [a,y] in P * R and
A2: [y,b] in Q by Def8;
consider x being set  such that
A3: [a,x] in P and
A4: [x,y] in R by A1, Def8;
 [x,b] in R * Q by A2, A4, Def8;
hence  [a,b] in P * (R * Q) by A3, Def8; ::_thesis: verum
end;
assume  [a,b] in P * (R * Q) ; ::_thesis: [a,b] in (P * R) * Q
then consider y being set  such that
A5: [a,y] in P and
A6: [y,b] in R * Q by Def8;
consider x being set  such that
A7: [y,x] in R and
A8: [x,b] in Q by A6, Def8;
 [a,x] in P * R by A5, A7, Def8;
hence  [a,b] in (P * R) * Q by A8, Def8; ::_thesis: verum
end;

registration
cluster non empty Relation-like for set ;
existence
 not for b1 being Relation holds b1 is empty
proof
 not {[{},{}]} is empty ;
hence  not for b1 being Relation holds b1 is empty ; ::_thesis: verum
end;
end;

registration
let f be non empty Relation;
cluster dom f ->  non empty ;
coherence
 not dom f is empty
proof
 ex x1, x2 being set st the Element of f = [x1,x2] by Def1;
hence  not dom f is empty by XTUPLE_0:def_12; ::_thesis: verum
end;
cluster rng f ->  non empty ;
coherence
 not rng f is empty
proof
 ex x1, x2 being set st the Element of f = [x1,x2] by Def1;
hence  not rng f is empty by XTUPLE_0:def_13; ::_thesis: verum
end;
end;

theorem Th37: :: RELAT_1:37
for R being Relation st ( for x, y being set holds not [x,y] in R ) holds
R = {}
proof
let R be Relation; ::_thesis: ( ( for x, y being set holds not [x,y] in R ) implies R = {} )
assume A1: for x, y being set holds not [x,y] in R ; ::_thesis: R = {}
assume A2: not R = {} ; ::_thesis: contradiction
then  ex x, y being set st the Element of R = [x,y] by Def1;
hence  contradiction by A1, A2; ::_thesis: verum
end;

theorem Th38: :: RELAT_1:38
( dom {} = {} & rng {} = {} )
proof
thus  dom {} = {} ::_thesis: rng {} = {}
proof
let x, y be set ; :: according to RELAT_1:def_2 ::_thesis: ( [x,y] in dom {} iff [x,y] in {} )
thus  ( [x,y] in dom {} implies [x,y] in {} ) ::_thesis: ( [x,y] in {} implies [x,y] in dom {} )
proof
assume  [x,y] in dom {} ; ::_thesis: [x,y] in {}
then  ex z being set st [[x,y],z] in {} ;
hence  [x,y] in {} ; ::_thesis: verum
end;
thus  ( [x,y] in {} implies [x,y] in dom {} ) ; ::_thesis: verum
end;
let x, y be set ; :: according to RELAT_1:def_2 ::_thesis: ( [x,y] in rng {} iff [x,y] in {} )
thus  ( [x,y] in rng {} implies [x,y] in {} ) ::_thesis: ( [x,y] in {} implies [x,y] in rng {} )
proof
assume  [x,y] in rng {} ; ::_thesis: [x,y] in {}
then  ex z being set st [z,[x,y]] in {} ;
hence  [x,y] in {} ; ::_thesis: verum
end;
thus  ( [x,y] in {} implies [x,y] in rng {} ) ; ::_thesis: verum
end;

theorem Th39: :: RELAT_1:39
for R being Relation holds
( {} * R = {} & R * {} = {} )
proof
let R be Relation; ::_thesis: ( {} * R = {} & R * {} = {} )
thus  {} * R = {} ::_thesis: R * {} = {}
proof
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b being set holds
( [x,b] in {} * R iff [x,b] in {} )
let y be set ; ::_thesis: ( [x,y] in {} * R iff [x,y] in {} )
hereby  ::_thesis: ( [x,y] in {} implies [x,y] in {} * R )
assume  [x,y] in {} * R ; ::_thesis: [x,y] in {}
then  ex z being set st
( [x,z] in {} & [z,y] in R ) by Def8;
hence  [x,y] in {} ; ::_thesis: verum
end;
thus  ( [x,y] in {} implies [x,y] in {} * R ) ; ::_thesis: verum
end;
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b being set holds
( [x,b] in R * {} iff [x,b] in {} )
let y be set ; ::_thesis: ( [x,y] in R * {} iff [x,y] in {} )
hereby  ::_thesis: ( [x,y] in {} implies [x,y] in R * {} )
assume  [x,y] in R * {} ; ::_thesis: [x,y] in {}
then  ex z being set st
( [x,z] in R & [z,y] in {} ) by Def8;
hence  [x,y] in {} ; ::_thesis: verum
end;
thus  ( [x,y] in {} implies [x,y] in R * {} ) ; ::_thesis: verum
end;

registration
let X be empty set ;
cluster dom X ->  empty ;
coherence
 dom X is empty ;
cluster rng X ->  empty ;
coherence
 rng X is empty ;
let R be Relation;
clusterX (#) R ->  empty ;
coherence
 X * R is empty by Th39;
clusterR (#) X ->  empty ;
coherence
 R * X is empty by Th39;
end;

theorem :: RELAT_1:40
field {} = {} ;

theorem Th41: :: RELAT_1:41
for R being Relation st ( dom R = {} or rng R = {} ) holds
R = {} ;

theorem :: RELAT_1:42
for R being Relation holds
( dom R = {} iff rng R = {} ) by Th38, Th41;

registration
let X be empty set ;
clusterX ~  ->  empty ;
coherence
 X ~ is empty
proof
 for x, y being set holds not [x,y] in {} ~ by Def7;
hence  X ~ is empty by Th37; ::_thesis: verum
end;
end;

theorem :: RELAT_1:43
{} ~ = {} ;

theorem :: RELAT_1:44
for R, P being Relation st rng R misses dom P holds
R * P = {}
proof
let R, P be Relation; ::_thesis: ( rng R misses dom P implies R * P = {} )
assume A1: (rng R) /\ (dom P) = {} ; :: according to XBOOLE_0:def_7 ::_thesis: R * P = {}
assume  R * P <> {} ; ::_thesis: contradiction
then consider x, z being set  such that
A2: [x,z] in R * P by Th37;
consider y being set  such that
A3: ( [x,y] in R & [y,z] in P ) by A2, Def8;
 ( y in rng R & y in dom P ) by A3, XTUPLE_0:def_12, XTUPLE_0:def_13;
hence  contradiction by A1, XBOOLE_0:def_4; ::_thesis: verum
end;

definition
let R be Relation;
attrR is non-empty  means :Def9: :: RELAT_1:def 9
 not {} in rng R;
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 for set ;
existence
 ex b1 being Relation st b1 is non-empty
proof
take  {} ; ::_thesis: {} is non-empty
thus  not {} in rng {} ; :: according to RELAT_1:def_9 ::_thesis: verum
end;
end;

registration
let R be Relation;
let S be non-empty Relation;
clusterR (#) S ->  non-empty ;
coherence
 R * S is non-empty
proof
 rng (R * S) c= rng S by Th26;
hence  not {} in rng (R * S) by Def9; :: according to RELAT_1:def_9 ::_thesis: verum
end;
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 b1 being Relation st
for x, y being set holds
( [x,y] in b1 iff ( x in X & x = y ) )
proof
defpred S1[ set , set ] means $1 = $2;
consider R being Relation such that
A1: for x, y being set holds
( [x,y] in R iff ( x in X & y in X & S1[x,y] ) ) from RELAT_1:sch_1();
take  R ; ::_thesis: for x, y being set holds
( [x,y] in R iff ( x in X & x = y ) )
let x, y be set ; ::_thesis: ( [x,y] in R iff ( x in X & x = y ) )
thus  ( [x,y] in R iff ( x in X & x = y ) ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Relation st ( for x, y being set holds
( [x,y] in b1 iff ( x in X & x = y ) ) ) & ( for x, y being set holds
( [x,y] in b2 iff ( x in X & x = y ) ) ) holds
b1 = b2
proof
let P1, P2 be Relation; ::_thesis: ( ( for x, y being set holds
( [x,y] in P1 iff ( x in X & x = y ) ) ) & ( for x, y being set holds
( [x,y] in P2 iff ( x in X & x = y ) ) ) implies P1 = P2 )
assume that
A2: for x, y being set holds
( [x,y] in P1 iff ( x in X & x = y ) ) and
A3: for x, y being set holds
( [x,y] in P2 iff ( x in X & x = y ) ) ; ::_thesis: P1 = P2
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b being set holds
( [x,b] in P1 iff [x,b] in P2 )
let y be set ; ::_thesis: ( [x,y] in P1 iff [x,y] in P2 )
 ( [x,y] in P1 iff ( x in X & x = y ) ) by A2;
hence  ( [x,y] in P1 iff [x,y] in P2 ) by A3; ::_thesis: verum
end;
end;

:: deftheorem Def10 defines id RELAT_1:def_10_:_
 for X being set
for b2 being Relation holds
( b2 = id X iff for x, y being set holds
( [x,y] in b2 iff ( x in X & x = y ) ) );

registration
let X be set ;
reduce dom (id X) to X;
reducibility
 dom (id X) = X
proof
thus  dom (id X) c= X :: according to XBOOLE_0:def_10 ::_thesis: X c= dom (id X)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (id X) or x in X )
assume  x in dom (id X) ; ::_thesis: x in X
then  ex y being set st [x,y] in id X by XTUPLE_0:def_12;
hence  x in X by Def10; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in dom (id X) )
assume  x in X ; ::_thesis: x in dom (id X)
then  [x,x] in id X by Def10;
hence  x in dom (id X) by XTUPLE_0:def_12; ::_thesis: verum
end;
reduce rng (id X) to X;
reducibility
 rng (id X) = X
proof
thus  rng (id X) c= X :: according to XBOOLE_0:def_10 ::_thesis: X c= rng (id X)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (id X) or x in X )
assume  x in rng (id X) ; ::_thesis: x in X
then consider y being set  such that
A1: [y,x] in id X by XTUPLE_0:def_13;
 x = y by A1, Def10;
hence  x in X by A1, Def10; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in rng (id X) )
 ( [x,x] in id X iff x in X ) by Def10;
hence  ( not x in X or x in rng (id X) ) by XTUPLE_0:def_13; ::_thesis: verum
end;
end;

theorem :: RELAT_1:45
for X being set holds
( dom (id X) = X & rng (id X) = X ) ;

registration
let X be set ;
reduce(id X) ~  to  id X;
reducibility
 (id X) ~ = id X
proof
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b being set holds
( [x,b] in (id X) ~ iff [x,b] in id X )
let y be set ; ::_thesis: ( [x,y] in (id X) ~ iff [x,y] in id X )
thus  ( [x,y] in (id X) ~ implies [x,y] in id X ) ::_thesis: ( [x,y] in id X implies [x,y] in (id X) ~ )
proof
assume  [x,y] in (id X) ~ ; ::_thesis: [x,y] in id X
then  [y,x] in id X by Def7;
hence  [x,y] in id X by Def10; ::_thesis: verum
end;
assume A1: [x,y] in id X ; ::_thesis: [x,y] in (id X) ~
then  x = y by Def10;
hence  [x,y] in (id X) ~ by A1, Def7; ::_thesis: verum
end;
end;

theorem :: RELAT_1:46
for X being set holds (id X) ~ = id X ;

theorem :: RELAT_1:47
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
proof
let X be set ; ::_thesis: for R being Relation st ( for x being set st x in X holds
[x,x] in R ) holds
id X c= R
let R be Relation; ::_thesis: ( ( for x being set st x in X holds
[x,x] in R ) implies id X c= R )
assume A1: for x being set st x in X holds
[x,x] in R ; ::_thesis: id X c= R
let x be set ; :: according to RELAT_1:def_3 ::_thesis: for b being set st [x,b] in id X holds
[x,b] in R
let y be set ; ::_thesis: ( [x,y] in id X implies [x,y] in R )
assume  [x,y] in id X ; ::_thesis: [x,y] in R
then  ( x in X & x = y ) by Def10;
hence  [x,y] in R by A1; ::_thesis: verum
end;

theorem Th48: :: RELAT_1:48
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 ) )
proof
let x, y, X be set ; ::_thesis: for R being Relation holds
( [x,y] in (id X) * R iff ( x in X & [x,y] in R ) )
let R be Relation; ::_thesis: ( [x,y] in (id X) * R iff ( x in X & [x,y] in R ) )
thus  ( [x,y] in (id X) * R implies ( x in X & [x,y] in R ) ) ::_thesis: ( x in X & [x,y] in R implies [x,y] in (id X) * R )
proof
assume  [x,y] in (id X) * R ; ::_thesis: ( x in X & [x,y] in R )
then  ex z being set st
( [x,z] in id X & [z,y] in R ) by Def8;
hence  ( x in X & [x,y] in R ) by Def10; ::_thesis: verum
end;
assume  x in X ; ::_thesis: ( not [x,y] in R or [x,y] in (id X) * R )
then  [x,x] in id X by Def10;
hence  ( not [x,y] in R or [x,y] in (id X) * R ) by Def8; ::_thesis: verum
end;

theorem Th49: :: RELAT_1:49
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 ) )
proof
let x, y, Y be set ; ::_thesis: for R being Relation holds
( [x,y] in R * (id Y) iff ( y in Y & [x,y] in R ) )
let R be Relation; ::_thesis: ( [x,y] in R * (id Y) iff ( y in Y & [x,y] in R ) )
thus  ( [x,y] in R * (id Y) implies ( y in Y & [x,y] in R ) ) ::_thesis: ( y in Y & [x,y] in R implies [x,y] in R * (id Y) )
proof
assume  [x,y] in R * (id Y) ; ::_thesis: ( y in Y & [x,y] in R )
then consider z being set  such that
A1: [x,z] in R and
A2: [z,y] in id Y by Def8;
 z = y by A2, Def10;
hence  ( y in Y & [x,y] in R ) by A1, A2, Def10; ::_thesis: verum
end;
 ( y in Y implies [y,y] in id Y ) by Def10;
hence  ( y in Y & [x,y] in R implies [x,y] in R * (id Y) ) by Def8; ::_thesis: verum
end;

theorem Th50: :: RELAT_1:50
for X being set
for R being Relation holds
( R * (id X) c= R & (id X) * R c= R )
proof
let X be set ; ::_thesis: for R being Relation holds
( R * (id X) c= R & (id X) * R c= R )
let R be Relation; ::_thesis: ( R * (id X) c= R & (id X) * R c= R )
thus  for x, y being set st [x,y] in R * (id X) holds
[x,y] in R :: according to RELAT_1:def_3 ::_thesis: (id X) * R c= R
proof
let x, y be set ; ::_thesis: ( [x,y] in R * (id X) implies [x,y] in R )
assume  [x,y] in R * (id X) ; ::_thesis: [x,y] in R
then  ex z being set st
( [x,z] in R & [z,y] in id X ) by Def8;
hence  [x,y] in R by Def10; ::_thesis: verum
end;
thus  for x, y being set st [x,y] in (id X) * R holds
[x,y] in R :: according to RELAT_1:def_3 ::_thesis: verum
proof
let x, y be set ; ::_thesis: ( [x,y] in (id X) * R implies [x,y] in R )
assume  [x,y] in (id X) * R ; ::_thesis: [x,y] in R
then  ex z being set st
( [x,z] in id X & [z,y] in R ) by Def8;
hence  [x,y] in R by Def10; ::_thesis: verum
end;
end;

theorem Th51: :: RELAT_1:51
for X being set
for R being Relation st dom R c= X holds
(id X) * R = R
proof
let X be set ; ::_thesis: for R being Relation st dom R c= X holds
(id X) * R = R
let R be Relation; ::_thesis: ( dom R c= X implies (id X) * R = R )
assume A1: dom R c= X ; ::_thesis: (id X) * R = R
A2: R c= (id X) * R
proof
let x be set ; :: according to RELAT_1:def_3 ::_thesis: for b being set st [x,b] in R holds
[x,b] in (id X) * R
let y be set ; ::_thesis: ( [x,y] in R implies [x,y] in (id X) * R )
assume A3: [x,y] in R ; ::_thesis: [x,y] in (id X) * R
then  x in dom R by XTUPLE_0:def_12;
then  [x,x] in id X by A1, Def10;
hence  [x,y] in (id X) * R by A3, Def8; ::_thesis: verum
end;
 (id X) * R c= R by Th50;
hence  (id X) * R = R by A2, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: RELAT_1:52
for R being Relation holds (id (dom R)) * R = R by Th51;

theorem Th53: :: RELAT_1:53
for Y being set
for R being Relation st rng R c= Y holds
R * (id Y) = R
proof
let Y be set ; ::_thesis: for R being Relation st rng R c= Y holds
R * (id Y) = R
let R be Relation; ::_thesis: ( rng R c= Y implies R * (id Y) = R )
assume A1: rng R c= Y ; ::_thesis: R * (id Y) = R
A2: R c= R * (id Y)
proof
let x be set ; :: according to RELAT_1:def_3 ::_thesis: for b being set st [x,b] in R holds
[x,b] in R * (id Y)
let y be set ; ::_thesis: ( [x,y] in R implies [x,y] in R * (id Y) )
assume A3: [x,y] in R ; ::_thesis: [x,y] in R * (id Y)
then  y in rng R by XTUPLE_0:def_13;
then  [y,y] in id Y by A1, Def10;
hence  [x,y] in R * (id Y) by A3, Def8; ::_thesis: verum
end;
 R * (id Y) c= R by Th50;
hence  R * (id Y) = R by A2, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: RELAT_1:54
for R being Relation holds R * (id (rng R)) = R by Th53;

theorem :: RELAT_1:55
id {} = {}
proof
 dom (id {}) = {} ;
hence  id {} = {} ; ::_thesis: verum
end;

theorem :: RELAT_1:56
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
proof
let X be set ; ::_thesis: for P2, R, P1 being Relation st rng P2 c= X & P2 * R = id (dom P1) & R * P1 = id X holds
P1 = P2
let P2, R, P1 be Relation; ::_thesis: ( rng P2 c= X & P2 * R = id (dom P1) & R * P1 = id X implies P1 = P2 )
 ( (P2 * R) * P1 = P2 * (R * P1) & (id (dom P1)) * P1 = P1 ) by Th36, Th51;
hence  ( rng P2 c= X & P2 * R = id (dom P1) & R * P1 = id X implies P1 = P2 ) by Th53; ::_thesis: verum
end;

definition
let R be Relation;
let X be set ;
funcR | 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 b1 being Relation st
for x, y being set holds
( [x,y] in b1 iff ( x in X & [x,y] in R ) )
proof
defpred S1[ set , set ] means ( $1 in X & [$1,$2] in R );
consider P being Relation such that
A1: for x, y being set holds
( [x,y] in P iff ( x in dom R & y in rng R & S1[x,y] ) ) from RELAT_1:sch_1();
take  P ; ::_thesis: for x, y being set holds
( [x,y] in P iff ( x in X & [x,y] in R ) )
let x, y be set ; ::_thesis: ( [x,y] in P iff ( x in X & [x,y] in R ) )
 ( x in X & [x,y] in R implies ( x in dom R & y in rng R ) ) by XTUPLE_0:def_12, XTUPLE_0:def_13;
hence  ( [x,y] in P iff ( x in X & [x,y] in R ) ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Relation st ( for x, y being set holds
( [x,y] in b1 iff ( x in X & [x,y] in R ) ) ) & ( for x, y being set holds
( [x,y] in b2 iff ( x in X & [x,y] in R ) ) ) holds
b1 = b2
proof
let P1, P2 be Relation; ::_thesis: ( ( for x, y being set holds
( [x,y] in P1 iff ( x in X & [x,y] in R ) ) ) & ( for x, y being set holds
( [x,y] in P2 iff ( x in X & [x,y] in R ) ) ) implies P1 = P2 )
assume that
A2: for x, y being set holds
( [x,y] in P1 iff ( x in X & [x,y] in R ) ) and
A3: for x, y being set holds
( [x,y] in P2 iff ( x in X & [x,y] in R ) ) ; ::_thesis: P1 = P2
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b being set holds
( [x,b] in P1 iff [x,b] in P2 )
let y be set ; ::_thesis: ( [x,y] in P1 iff [x,y] in P2 )
 ( [x,y] in P1 iff ( x in X & [x,y] in R ) ) by A2;
hence  ( [x,y] in P1 iff [x,y] in P2 ) by A3; ::_thesis: verum
end;
end;

:: deftheorem Def11 defines | RELAT_1:def_11_:_
 for R being Relation
for X being set
for b3 being Relation holds
( b3 = R | X iff for x, y being set holds
( [x,y] in b3 iff ( x in X & [x,y] in R ) ) );

registration
let R be Relation;
let X be empty set ;
clusterR | X ->  empty ;
coherence
 R | X is empty
proof
 for x, y being set holds not [x,y] in R | {} by Def11;
hence  R | X is empty by Th37; ::_thesis: verum
end;
end;

theorem Th57: :: RELAT_1:57
for x, X being set
for R being Relation holds
( x in dom (R | X) iff ( x in X & x in dom R ) )
proof
let x, X be set ; ::_thesis: for R being Relation holds
( x in dom (R | X) iff ( x in X & x in dom R ) )
let R be Relation; ::_thesis: ( x in dom (R | X) iff ( x in X & x in dom R ) )
thus  ( x in dom (R | X) implies ( x in X & x in dom R ) ) ::_thesis: ( x in X & x in dom R implies x in dom (R | X) )
proof
assume  x in dom (R | X) ; ::_thesis: ( x in X & x in dom R )
then consider y being set  such that
A1: [x,y] in R | X by XTUPLE_0:def_12;
 [x,y] in R by A1, Def11;
hence  ( x in X & x in dom R ) by A1, Def11, XTUPLE_0:def_12; ::_thesis: verum
end;
assume A2: x in X ; ::_thesis: ( not x in dom R or x in dom (R | X) )
assume  x in dom R ; ::_thesis: x in dom (R | X)
then consider y being set  such that
A3: [x,y] in R by XTUPLE_0:def_12;
 [x,y] in R | X by A2, A3, Def11;
hence  x in dom (R | X) by XTUPLE_0:def_12; ::_thesis: verum
end;

theorem Th58: :: RELAT_1:58
for X being set
for R being Relation holds dom (R | X) c= X
proof
let X be set ; ::_thesis: for R being Relation holds dom (R | X) c= X
let R be Relation; ::_thesis: dom (R | X) c= X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (R | X) or x in X )
thus  ( not x in dom (R | X) or x in X ) by Th57; ::_thesis: verum
end;

theorem Th59: :: RELAT_1:59
for X being set
for R being Relation holds R | X c= R
proof
let X be set ; ::_thesis: for R being Relation holds R | X c= R
let R be Relation; ::_thesis: R | X c= R
thus  for x, y being set st [x,y] in R | X holds
[x,y] in R by Def11; :: according to RELAT_1:def_3 ::_thesis: verum
end;

theorem Th60: :: RELAT_1:60
for X being set
for R being Relation holds dom (R | X) c= dom R
proof
let X be set ; ::_thesis: for R being Relation holds dom (R | X) c= dom R
let R be Relation; ::_thesis: dom (R | X) c= dom R
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (R | X) or x in dom R )
thus  ( not x in dom (R | X) or x in dom R ) by Th57; ::_thesis: verum
end;

theorem Th61: :: RELAT_1:61
for X being set
for R being Relation holds dom (R | X) = (dom R) /\ X
proof
let X be set ; ::_thesis: for R being Relation holds dom (R | X) = (dom R) /\ X
let R be Relation; ::_thesis: dom (R | X) = (dom R) /\ X
 for x being set holds
( x in dom (R | X) iff x in (dom R) /\ X )
proof
let x be set ; ::_thesis: ( x in dom (R | X) iff x in (dom R) /\ X )
 ( x in dom (R | X) iff ( x in dom R & x in X ) ) by Th57;
hence  ( x in dom (R | X) iff x in (dom R) /\ X ) by XBOOLE_0:def_4; ::_thesis: verum
end;
hence  dom (R | X) = (dom R) /\ X by TARSKI:1; ::_thesis: verum
end;

theorem :: RELAT_1:62
for X being set
for R being Relation st X c= dom R holds
dom (R | X) = X
proof
let X be set ; ::_thesis: for R being Relation st X c= dom R holds
dom (R | X) = X
let R be Relation; ::_thesis: ( X c= dom R implies dom (R | X) = X )
 dom (R | X) = (dom R) /\ X by Th61;
hence  ( X c= dom R implies dom (R | X) = X ) by XBOOLE_1:28; ::_thesis: verum
end;

theorem :: RELAT_1:63
for X being set
for R, P being Relation holds (R | X) * P c= R * P by Th30, Th59;

theorem :: RELAT_1:64
for X being set
for P, R being Relation holds P * (R | X) c= P * R by Th29, Th59;

theorem :: RELAT_1:65
for X being set
for R being Relation holds R | X = (id X) * R
proof
let X be set ; ::_thesis: for R being Relation holds R | X = (id X) * R
let R be Relation; ::_thesis: R | X = (id X) * R
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b being set holds
( [x,b] in R | X iff [x,b] in (id X) * R )
let y be set ; ::_thesis: ( [x,y] in R | X iff [x,y] in (id X) * R )
 ( [x,y] in R | X iff ( [x,y] in R & x in X ) ) by Def11;
hence  ( [x,y] in R | X iff [x,y] in (id X) * R ) by Th48; ::_thesis: verum
end;

theorem :: RELAT_1:66
for X being set
for R being Relation holds
( R | X = {} iff dom R misses X )
proof
let X be set ; ::_thesis: for R being Relation holds
( R | X = {} iff dom R misses X )
let R be Relation; ::_thesis: ( R | X = {} iff dom R misses X )
thus  ( R | X = {} implies dom R misses X ) ::_thesis: ( dom R misses X implies R | X = {} )
proof
assume A1: R | X = {} ; ::_thesis: dom R misses X
thus  (dom R) /\ X = {} :: according to XBOOLE_0:def_7 ::_thesis: verum
proof
thus  (dom R) /\ X c= {} :: according to XBOOLE_0:def_10 ::_thesis: {} c= (dom R) /\ X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (dom R) /\ X or x in {} )
assume A2: x in (dom R) /\ X ; ::_thesis: x in {}
then  x in dom R by XBOOLE_0:def_4;
then A3: ex y being set st [x,y] in R by XTUPLE_0:def_12;
 x in X by A2, XBOOLE_0:def_4;
hence  x in {} by A1, A3, Def11; ::_thesis: verum
end;
thus  {} c= (dom R) /\ X by XBOOLE_1:2; ::_thesis: verum
end;
end;
assume A4: (dom R) /\ X = {} ; :: according to XBOOLE_0:def_7 ::_thesis: R | X = {}
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b being set holds
( [x,b] in R | X iff [x,b] in {} )
let y be set ; ::_thesis: ( [x,y] in R | X iff [x,y] in {} )
hereby  ::_thesis: ( [x,y] in {} implies [x,y] in R | X )
assume A5: [x,y] in R | X ; ::_thesis: [x,y] in {}
then  x in X by Def11;
then A6: not x in dom R by A4, XBOOLE_0:def_4;
 [x,y] in R by A5, Def11;
hence  [x,y] in {} by A6, XTUPLE_0:def_12; ::_thesis: verum
end;
thus  ( [x,y] in {} implies [x,y] in R | X ) ; ::_thesis: verum
end;

theorem Th67: :: RELAT_1:67
for X being set
for R being Relation holds R | X = R /\ [:X,(rng R):]
proof
let X be set ; ::_thesis: for R being Relation holds R | X = R /\ [:X,(rng R):]
let R be Relation; ::_thesis: R | X = R /\ [:X,(rng R):]
set P = R /\ [:X,(rng R):];
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b being set holds
( [x,b] in R | X iff [x,b] in R /\ [:X,(rng R):] )
let y be set ; ::_thesis: ( [x,y] in R | X iff [x,y] in R /\ [:X,(rng R):] )
thus  ( [x,y] in R | X implies [x,y] in R /\ [:X,(rng R):] ) ::_thesis: ( [x,y] in R /\ [:X,(rng R):] implies [x,y] in R | X )
proof
assume A1: [x,y] in R | X ; ::_thesis: [x,y] in R /\ [:X,(rng R):]
then A2: x in X by Def11;
A3: [x,y] in R by A1, Def11;
then  y in rng R by XTUPLE_0:def_13;
then  [x,y] in [:X,(rng R):] by A2, ZFMISC_1:def_2;
hence  [x,y] in R /\ [:X,(rng R):] by A3, XBOOLE_0:def_4; ::_thesis: verum
end;
assume A4: [x,y] in R /\ [:X,(rng R):] ; ::_thesis: [x,y] in R | X
then  [x,y] in [:X,(rng R):] by XBOOLE_0:def_4;
then A5: x in X by ZFMISC_1:87;
 [x,y] in R by A4, XBOOLE_0:def_4;
hence  [x,y] in R | X by A5, Def11; ::_thesis: verum
end;

theorem Th68: :: RELAT_1:68
for X being set
for R being Relation st dom R c= X holds
R | X = R
proof
let X be set ; ::_thesis: for R being Relation st dom R c= X holds
R | X = R
let R be Relation; ::_thesis: ( dom R c= X implies R | X = R )
assume  dom R c= X ; ::_thesis: R | X = R
then A1: [:(dom R),(rng R):] c= [:X,(rng R):] by ZFMISC_1:95;
 ( R c= [:(dom R),(rng R):] & R | X = R /\ [:X,(rng R):] ) by Th7, Th67;
hence  R | X = R by A1, XBOOLE_1:1, XBOOLE_1:28; ::_thesis: verum
end;

registration
let R be Relation;
reduceR | (dom R) to R;
reducibility
 R | (dom R) = R by Th68;
end;

theorem :: RELAT_1:69
for R being Relation holds R | (dom R) = R ;

theorem Th70: :: RELAT_1:70
for X being set
for R being Relation holds rng (R | X) c= rng R
proof
let X be set ; ::_thesis: for R being Relation holds rng (R | X) c= rng R
let R be Relation; ::_thesis: rng (R | X) c= rng R
 R | X c= R by Th59;
hence  rng (R | X) c= rng R by Th11; ::_thesis: verum
end;

theorem Th71: :: RELAT_1:71
for X, Y being set
for R being Relation holds (R | X) | Y = R | (X /\ Y)
proof
let X, Y be set ; ::_thesis: for R being Relation holds (R | X) | Y = R | (X /\ Y)
let R be Relation; ::_thesis: (R | X) | Y = R | (X /\ Y)
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b being set holds
( [x,b] in (R | X) | Y iff [x,b] in R | (X /\ Y) )
let y be set ; ::_thesis: ( [x,y] in (R | X) | Y iff [x,y] in R | (X /\ Y) )
A1: ( [x,y] in R | X iff ( [x,y] in R & x in X ) ) by Def11;
A2: ( [x,y] in R | (X /\ Y) iff ( [x,y] in R & x in X /\ Y ) ) by Def11;
 ( [x,y] in (R | X) | Y iff ( [x,y] in R | X & x in Y ) ) by Def11;
hence  ( [x,y] in (R | X) | Y iff [x,y] in R | (X /\ Y) ) by A1, A2, XBOOLE_0:def_4; ::_thesis: verum
end;

registration
let R be Relation;
let X be set ;
reduce(R | X) | X to R | X;
reducibility
 (R | X) | X = R | X
proof
 X /\ X = X ;
hence  (R | X) | X = R | X by Th71; ::_thesis: verum
end;
end;

theorem :: RELAT_1:72
for X being set
for R being Relation holds (R | X) | X = R | X ;

theorem :: RELAT_1:73
for X, Y being set
for R being Relation st X c= Y holds
(R | X) | Y = R | X
proof
let X, Y be set ; ::_thesis: for R being Relation st X c= Y holds
(R | X) | Y = R | X
let R be Relation; ::_thesis: ( X c= Y implies (R | X) | Y = R | X )
 ( X c= Y implies X /\ Y = X ) by XBOOLE_1:28;
hence  ( X c= Y implies (R | X) | Y = R | X ) by Th71; ::_thesis: verum
end;

theorem :: RELAT_1:74
for Y, X being set
for R being Relation st Y c= X holds
(R | X) | Y = R | Y
proof
let Y, X be set ; ::_thesis: for R being Relation st Y c= X holds
(R | X) | Y = R | Y
let R be Relation; ::_thesis: ( Y c= X implies (R | X) | Y = R | Y )
 ( Y c= X implies X /\ Y = Y ) by XBOOLE_1:28;
hence  ( Y c= X implies (R | X) | Y = R | Y ) by Th71; ::_thesis: verum
end;

theorem Th75: :: RELAT_1:75
for X, Y being set
for R being Relation st X c= Y holds
R | X c= R | Y
proof
let X, Y be set ; ::_thesis: for R being Relation st X c= Y holds
R | X c= R | Y
let R be Relation; ::_thesis: ( X c= Y implies R | X c= R | Y )
assume A1: X c= Y ; ::_thesis: R | X c= R | Y
let x be set ; :: according to RELAT_1:def_3 ::_thesis: for b being set st [x,b] in R | X holds
[x,b] in R | Y
let y be set ; ::_thesis: ( [x,y] in R | X implies [x,y] in R | Y )
assume  [x,y] in R | X ; ::_thesis: [x,y] in R | Y
then  ( x in X & [x,y] in R ) by Def11;
hence  [x,y] in R | Y by A1, Def11; ::_thesis: verum
end;

theorem Th76: :: RELAT_1:76
for X being set
for P, R being Relation st P c= R holds
P | X c= R | X
proof
let X be set ; ::_thesis: for P, R being Relation st P c= R holds
P | X c= R | X
let P, R be Relation; ::_thesis: ( P c= R implies P | X c= R | X )
assume A1: P c= R ; ::_thesis: P | X c= R | X
let x be set ; :: according to RELAT_1:def_3 ::_thesis: for b being set st [x,b] in P | X holds
[x,b] in R | X
let y be set ; ::_thesis: ( [x,y] in P | X implies [x,y] in R | X )
assume  [x,y] in P | X ; ::_thesis: [x,y] in R | X
then  ( [x,y] in P & x in X ) by Def11;
hence  [x,y] in R | X by A1, Def11; ::_thesis: verum
end;

theorem Th77: :: RELAT_1:77
for X, Y being set
for P, R being Relation st P c= R & X c= Y holds
P | X c= R | Y
proof
let X, Y be set ; ::_thesis: for P, R being Relation st P c= R & X c= Y holds
P | X c= R | Y
let P, R be Relation; ::_thesis: ( P c= R & X c= Y implies P | X c= R | Y )
assume  ( P c= R & X c= Y ) ; ::_thesis: P | X c= R | Y
then  ( P | X c= R | X & R | X c= R | Y ) by Th75, Th76;
hence  P | X c= R | Y by XBOOLE_1:1; ::_thesis: verum
end;

theorem Th78: :: RELAT_1:78
for X, Y being set
for R being Relation holds R | (X \/ Y) = (R | X) \/ (R | Y)
proof
let X, Y be set ; ::_thesis: for R being Relation holds R | (X \/ Y) = (R | X) \/ (R | Y)
let R be Relation; ::_thesis: R | (X \/ Y) = (R | X) \/ (R | Y)
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b being set holds
( [x,b] in R | (X \/ Y) iff [x,b] in (R | X) \/ (R | Y) )
let y be set ; ::_thesis: ( [x,y] in R | (X \/ Y) iff [x,y] in (R | X) \/ (R | Y) )
hereby  ::_thesis: ( [x,y] in (R | X) \/ (R | Y) implies [x,y] in R | (X \/ Y) )
assume A1: [x,y] in R | (X \/ Y) ; ::_thesis: [x,y] in (R | X) \/ (R | Y)
then  x in X \/ Y by Def11;
then A2: ( x in X or x in Y ) by XBOOLE_0:def_3;
 [x,y] in R by A1, Def11;
then  ( [x,y] in R | X or [x,y] in R | Y ) by A2, Def11;
hence  [x,y] in (R | X) \/ (R | Y) by XBOOLE_0:def_3; ::_thesis: verum
end;
assume A3: [x,y] in (R | X) \/ (R | Y) ; ::_thesis: [x,y] in R | (X \/ Y)
percases ( [x,y] in R | Y or [x,y] in R | X ) by A3, XBOOLE_0:def_3;
supposeA4: [x,y] in R | Y ; ::_thesis: [x,y] in R | (X \/ Y)
then  x in Y by Def11;
then A5: x in X \/ Y by XBOOLE_0:def_3;
 [x,y] in R by A4, Def11;
hence  [x,y] in R | (X \/ Y) by A5, Def11; ::_thesis: verum
end;
supposeA6: [x,y] in R | X ; ::_thesis: [x,y] in R | (X \/ Y)
then  x in X by Def11;
then A7: x in X \/ Y by XBOOLE_0:def_3;
 [x,y] in R by A6, Def11;
hence  [x,y] in R | (X \/ Y) by A7, Def11; ::_thesis: verum
end;
end;
end;

theorem :: RELAT_1:79
for X, Y being set
for R being Relation holds R | (X /\ Y) = (R | X) /\ (R | Y)
proof
let X, Y be set ; ::_thesis: for R being Relation holds R | (X /\ Y) = (R | X) /\ (R | Y)
let R be Relation; ::_thesis: R | (X /\ Y) = (R | X) /\ (R | Y)
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b being set holds
( [x,b] in R | (X /\ Y) iff [x,b] in (R | X) /\ (R | Y) )
let y be set ; ::_thesis: ( [x,y] in R | (X /\ Y) iff [x,y] in (R | X) /\ (R | Y) )
hereby  ::_thesis: ( [x,y] in (R | X) /\ (R | Y) implies [x,y] in R | (X /\ Y) )
assume A1: [x,y] in R | (X /\ Y) ; ::_thesis: [x,y] in (R | X) /\ (R | Y)
then A2: x in X /\ Y by Def11;
A3: [x,y] in R by A1, Def11;
 x in Y by A2, XBOOLE_0:def_4;
then A4: [x,y] in R | Y by A3, Def11;
 x in X by A2, XBOOLE_0:def_4;
then  [x,y] in R | X by A3, Def11;
hence  [x,y] in (R | X) /\ (R | Y) by A4, XBOOLE_0:def_4; ::_thesis: verum
end;
assume A5: [x,y] in (R | X) /\ (R | Y) ; ::_thesis: [x,y] in R | (X /\ Y)
then  [x,y] in R | Y by XBOOLE_0:def_4;
then A6: x in Y by Def11;
A7: [x,y] in R | X by A5, XBOOLE_0:def_4;
then  x in X by Def11;
then A8: x in X /\ Y by A6, XBOOLE_0:def_4;
 [x,y] in R by A7, Def11;
hence  [x,y] in R | (X /\ Y) by A8, Def11; ::_thesis: verum
end;

theorem Th80: :: RELAT_1:80
for X, Y being set
for R being Relation holds R | (X \ Y) = (R | X) \ (R | Y)
proof
let X, Y be set ; ::_thesis: for R being Relation holds R | (X \ Y) = (R | X) \ (R | Y)
let R be Relation; ::_thesis: R | (X \ Y) = (R | X) \ (R | Y)
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b being set holds
( [x,b] in R | (X \ Y) iff [x,b] in (R | X) \ (R | Y) )
let y be set ; ::_thesis: ( [x,y] in R | (X \ Y) iff [x,y] in (R | X) \ (R | Y) )
hereby  ::_thesis: ( [x,y] in (R | X) \ (R | Y) implies [x,y] in R | (X \ Y) )
assume A1: [x,y] in R | (X \ Y) ; ::_thesis: [x,y] in (R | X) \ (R | Y)
then A2: x in X \ Y by Def11;
then  not x in Y by XBOOLE_0:def_5;
then A3: not [x,y] in R | Y by Def11;
 [x,y] in R by A1, Def11;
then  [x,y] in R | X by A2, Def11;
hence  [x,y] in (R | X) \ (R | Y) by A3, XBOOLE_0:def_5; ::_thesis: verum
end;
assume A4: [x,y] in (R | X) \ (R | Y) ; ::_thesis: [x,y] in R | (X \ Y)
then A5: [x,y] in R by Def11;
 not [x,y] in R | Y by A4, XBOOLE_0:def_5;
then A6: ( not x in Y or not [x,y] in R ) by Def11;
 x in X by A4, Def11;
then  x in X \ Y by A4, A6, Def11, XBOOLE_0:def_5;
hence  [x,y] in R | (X \ Y) by A5, Def11; ::_thesis: verum
end;

registration
let R be empty Relation;
let X be set ;
clusterR | X ->  empty ;
coherence
 R | X is empty
proof
 for x, y being set holds not [x,y] in {} | X by Def11;
hence  R | X is empty by Th37; ::_thesis: verum
end;
end;

theorem :: RELAT_1:81
for R being Relation holds R | {} = {} ;

theorem :: RELAT_1:82
for X being set holds {} | X = {} ;

theorem :: RELAT_1:83
for X being set
for P, R being Relation holds (P * R) | X = (P | X) * R
proof
let X be set ; ::_thesis: for P, R being Relation holds (P * R) | X = (P | X) * R
let P, R be Relation; ::_thesis: (P * R) | X = (P | X) * R
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b being set holds
( [x,b] in (P * R) | X iff [x,b] in (P | X) * R )
let y be set ; ::_thesis: ( [x,y] in (P * R) | X iff [x,y] in (P | X) * R )
hereby  ::_thesis: ( [x,y] in (P | X) * R implies [x,y] in (P * R) | X )
assume A1: [x,y] in (P * R) | X ; ::_thesis: [x,y] in (P | X) * R
then  [x,y] in P * R by Def11;
then consider a being set  such that
A2: [x,a] in P and
A3: [a,y] in R by Def8;
 x in X by A1, Def11;
then  [x,a] in P | X by A2, Def11;
hence  [x,y] in (P | X) * R by A3, Def8; ::_thesis: verum
end;
assume  [x,y] in (P | X) * R ; ::_thesis: [x,y] in (P * R) | X
then consider a being set  such that
A4: [x,a] in P | X and
A5: [a,y] in R by Def8;
 [x,a] in P by A4, Def11;
then A6: [x,y] in P * R by A5, Def8;
 x in X by A4, Def11;
hence  [x,y] in (P * R) | X by A6, Def11; ::_thesis: verum
end;

definition
let Y be set ;
let R be Relation;
funcY |` 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 b1 being Relation st
for x, y being set holds
( [x,y] in b1 iff ( y in Y & [x,y] in R ) )
proof
defpred S1[ set , set ] means ( $2 in Y & [$1,$2] in R );
consider P being Relation such that
A1: for x, y being set holds
( [x,y] in P iff ( x in dom R & y in rng R & S1[x,y] ) ) from RELAT_1:sch_1();
take  P ; ::_thesis: for x, y being set holds
( [x,y] in P iff ( y in Y & [x,y] in R ) )
let x, y be set ; ::_thesis: ( [x,y] in P iff ( y in Y & [x,y] in R ) )
 ( y in Y & [x,y] in R implies ( x in dom R & y in rng R ) ) by XTUPLE_0:def_12, XTUPLE_0:def_13;
hence  ( [x,y] in P iff ( y in Y & [x,y] in R ) ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Relation st ( for x, y being set holds
( [x,y] in b1 iff ( y in Y & [x,y] in R ) ) ) & ( for x, y being set holds
( [x,y] in b2 iff ( y in Y & [x,y] in R ) ) ) holds
b1 = b2
proof
let P1, P2 be Relation; ::_thesis: ( ( for x, y being set holds
( [x,y] in P1 iff ( y in Y & [x,y] in R ) ) ) & ( for x, y being set holds
( [x,y] in P2 iff ( y in Y & [x,y] in R ) ) ) implies P1 = P2 )
assume that
A2: for x, y being set holds
( [x,y] in P1 iff ( y in Y & [x,y] in R ) ) and
A3: for x, y being set holds
( [x,y] in P2 iff ( y in Y & [x,y] in R ) ) ; ::_thesis: P1 = P2
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b being set holds
( [x,b] in P1 iff [x,b] in P2 )
let y be set ; ::_thesis: ( [x,y] in P1 iff [x,y] in P2 )
 ( [x,y] in P1 iff ( y in Y & [x,y] in R ) ) by A2;
hence  ( [x,y] in P1 iff [x,y] in P2 ) by A3; ::_thesis: verum
end;
end;

:: deftheorem Def12 defines |` RELAT_1:def_12_:_
 for Y being set
for R, b3 being Relation holds
( b3 = Y |` R iff for x, y being set holds
( [x,y] in b3 iff ( y in Y & [x,y] in R ) ) );

registration
let R be Relation;
let X be empty set ;
clusterX |` R ->  empty ;
coherence
 X |` R is empty
proof
 for x, y being set holds not [x,y] in X |` R by Def12;
hence  X |` R is empty by Th37; ::_thesis: verum
end;
end;

theorem Th84: :: RELAT_1:84
for y, Y being set
for R being Relation holds
( y in rng (Y |` R) iff ( y in Y & y in rng R ) )
proof
let y, Y be set ; ::_thesis: for R being Relation holds
( y in rng (Y |` R) iff ( y in Y & y in rng R ) )
let R be Relation; ::_thesis: ( y in rng (Y |` R) iff ( y in Y & y in rng R ) )
thus  ( y in rng (Y |` R) implies ( y in Y & y in rng R ) ) ::_thesis: ( y in Y & y in rng R implies y in rng (Y |` R) )
proof
assume  y in rng (Y |` R) ; ::_thesis: ( y in Y & y in rng R )
then consider x being set  such that
A1: [x,y] in Y |` R by XTUPLE_0:def_13;
 [x,y] in R by A1, Def12;
hence  ( y in Y & y in rng R ) by A1, Def12, XTUPLE_0:def_13; ::_thesis: verum
end;
assume A2: y in Y ; ::_thesis: ( not y in rng R or y in rng (Y |` R) )
assume  y in rng R ; ::_thesis: y in rng (Y |` R)
then consider x being set  such that
A3: [x,y] in R by XTUPLE_0:def_13;
 [x,y] in Y |` R by A2, A3, Def12;
hence  y in rng (Y |` R) by XTUPLE_0:def_13; ::_thesis: verum
end;

theorem Th85: :: RELAT_1:85
for Y being set
for R being Relation holds rng (Y |` R) c= Y
proof
let Y be set ; ::_thesis: for R being Relation holds rng (Y |` R) c= Y
let R be Relation; ::_thesis: rng (Y |` R) c= Y
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (Y |` R) or y in Y )
thus  ( not y in rng (Y |` R) or y in Y ) by Th84; ::_thesis: verum
end;

theorem Th86: :: RELAT_1:86
for Y being set
for R being Relation holds Y |` R c= R
proof
let Y be set ; ::_thesis: for R being Relation holds Y |` R c= R
let R be Relation; ::_thesis: Y |` R c= R
thus  for x, y being set st [x,y] in Y |` R holds
[x,y] in R by Def12; :: according to RELAT_1:def_3 ::_thesis: verum
end;

theorem Th87: :: RELAT_1:87
for Y being set
for R being Relation holds rng (Y |` R) c= rng R
proof
let Y be set ; ::_thesis: for R being Relation holds rng (Y |` R) c= rng R
let R be Relation; ::_thesis: rng (Y |` R) c= rng R
 Y |` R c= R by Th86;
hence  rng (Y |` R) c= rng R by Th11; ::_thesis: verum
end;

theorem Th88: :: RELAT_1:88
for Y being set
for R being Relation holds rng (Y |` R) = (rng R) /\ Y
proof
let Y be set ; ::_thesis: for R being Relation holds rng (Y |` R) = (rng R) /\ Y
let R be Relation; ::_thesis: rng (Y |` R) = (rng R) /\ Y
 ( rng (Y |` R) c= Y & rng (Y |` R) c= rng R ) by Th85, Th87;
hence  rng (Y |` R) c= (rng R) /\ Y by XBOOLE_1:19; :: according to XBOOLE_0:def_10 ::_thesis: (rng R) /\ Y c= rng (Y |` R)
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (rng R) /\ Y or y in rng (Y |` R) )
assume A1: y in (rng R) /\ Y ; ::_thesis: y in rng (Y |` R)
then  y in rng R by XBOOLE_0:def_4;
then consider x being set  such that
A2: [x,y] in R by XTUPLE_0:def_13;
 y in Y by A1, XBOOLE_0:def_4;
then  [x,y] in Y |` R by A2, Def12;
hence  y in rng (Y |` R) by XTUPLE_0:def_13; ::_thesis: verum
end;

theorem :: RELAT_1:89
for Y being set
for R being Relation st Y c= rng R holds
rng (Y |` R) = Y
proof
let Y be set ; ::_thesis: for R being Relation st Y c= rng R holds
rng (Y |` R) = Y
let R be Relation; ::_thesis: ( Y c= rng R implies rng (Y |` R) = Y )
assume  Y c= rng R ; ::_thesis: rng (Y |` R) = Y
then  (rng R) /\ Y = Y by XBOOLE_1:28;
hence  rng (Y |` R) = Y by Th88; ::_thesis: verum
end;

theorem :: RELAT_1:90
for Y being set
for R, P being Relation holds (Y |` R) * P c= R * P by Th30, Th86;

theorem :: RELAT_1:91
for Y being set
for P, R being Relation holds P * (Y |` R) c= P * R by Th29, Th86;

theorem :: RELAT_1:92
for Y being set
for R being Relation holds Y |` R = R * (id Y)
proof
let Y be set ; ::_thesis: for R being Relation holds Y |` R = R * (id Y)
let R be Relation; ::_thesis: Y |` R = R * (id Y)
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b being set holds
( [x,b] in Y |` R iff [x,b] in R * (id Y) )
let y be set ; ::_thesis: ( [x,y] in Y |` R iff [x,y] in R * (id Y) )
 ( [x,y] in Y |` R iff ( y in Y & [x,y] in R ) ) by Def12;
hence  ( [x,y] in Y |` R iff [x,y] in R * (id Y) ) by Th49; ::_thesis: verum
end;

theorem Th93: :: RELAT_1:93
for Y being set
for R being Relation holds Y |` R = R /\ [:(dom R),Y:]
proof
let Y be set ; ::_thesis: for R being Relation holds Y |` R = R /\ [:(dom R),Y:]
let R be Relation; ::_thesis: Y |` R = R /\ [:(dom R),Y:]
set P = R /\ [:(dom R),Y:];
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b being set holds
( [x,b] in Y |` R iff [x,b] in R /\ [:(dom R),Y:] )
let y be set ; ::_thesis: ( [x,y] in Y |` R iff [x,y] in R /\ [:(dom R),Y:] )
thus  ( [x,y] in Y |` R implies [x,y] in R /\ [:(dom R),Y:] ) ::_thesis: ( [x,y] in R /\ [:(dom R),Y:] implies [x,y] in Y |` R )
proof
assume A1: [x,y] in Y |` R ; ::_thesis: [x,y] in R /\ [:(dom R),Y:]
then A2: y in Y by Def12;
A3: [x,y] in R by A1, Def12;
then  x in dom R by XTUPLE_0:def_12;
then  [x,y] in [:(dom R),Y:] by A2, ZFMISC_1:def_2;
hence  [x,y] in R /\ [:(dom R),Y:] by A3, XBOOLE_0:def_4; ::_thesis: verum
end;
assume A4: [x,y] in R /\ [:(dom R),Y:] ; ::_thesis: [x,y] in Y |` R
then  [x,y] in [:(dom R),Y:] by XBOOLE_0:def_4;
then A5: y in Y by ZFMISC_1:87;
 [x,y] in R by A4, XBOOLE_0:def_4;
hence  [x,y] in Y |` R by A5, Def12; ::_thesis: verum
end;

theorem Th94: :: RELAT_1:94
for Y being set
for R being Relation st rng R c= Y holds
Y |` R = R
proof
let Y be set ; ::_thesis: for R being Relation st rng R c= Y holds
Y |` R = R
let R be Relation; ::_thesis: ( rng R c= Y implies Y |` R = R )
assume  rng R c= Y ; ::_thesis: Y |` R = R
then A1: [:(dom R),(rng R):] c= [:(dom R),Y:] by ZFMISC_1:95;
 ( R c= [:(dom R),(rng R):] & Y |` R = R /\ [:(dom R),Y:] ) by Th7, Th93;
hence  Y |` R = R by A1, XBOOLE_1:1, XBOOLE_1:28; ::_thesis: verum
end;

registration
let R be Relation;
reduce(rng R) |` R to R;
reducibility
 (rng R) |` R = R by Th94;
end;

theorem :: RELAT_1:95
for R being Relation holds (rng R) |` R = R ;

theorem Th96: :: RELAT_1:96
for Y, X being set
for R being Relation holds Y |` (X |` R) = (Y /\ X) |` R
proof
let Y, X be set ; ::_thesis: for R being Relation holds Y |` (X |` R) = (Y /\ X) |` R
let R be Relation; ::_thesis: Y |` (X |` R) = (Y /\ X) |` R
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b being set holds
( [x,b] in Y |` (X |` R) iff [x,b] in (Y /\ X) |` R )
let y be set ; ::_thesis: ( [x,y] in Y |` (X |` R) iff [x,y] in (Y /\ X) |` R )
A1: ( [x,y] in X |` R iff ( [x,y] in R & y in X ) ) by Def12;
A2: ( [x,y] in (Y /\ X) |` R iff ( [x,y] in R & y in Y /\ X ) ) by Def12;
 ( [x,y] in Y |` (X |` R) iff ( [x,y] in X |` R & y in Y ) ) by Def12;
hence  ( [x,y] in Y |` (X |` R) iff [x,y] in (Y /\ X) |` R ) by A1, A2, XBOOLE_0:def_4; ::_thesis: verum
end;

registration
let Y be set ;
let R be Relation;
reduceY |` (Y |` R) to Y |` R;
reducibility
 Y |` (Y |` R) = Y |` R
proof
 Y /\ Y = Y ;
hence  Y |` (Y |` R) = Y |` R by Th96; ::_thesis: verum
end;
end;

theorem :: RELAT_1:97
for Y being set
for R being Relation holds Y |` (Y |` R) = Y |` R ;

theorem :: RELAT_1:98
for X, Y being set
for R being Relation st X c= Y holds
Y |` (X |` R) = X |` R
proof
let X, Y be set ; ::_thesis: for R being Relation st X c= Y holds
Y |` (X |` R) = X |` R
let R be Relation; ::_thesis: ( X c= Y implies Y |` (X |` R) = X |` R )
 ( X c= Y implies Y /\ X = X ) by XBOOLE_1:28;
hence  ( X c= Y implies Y |` (X |` R) = X |` R ) by Th96; ::_thesis: verum
end;

theorem :: RELAT_1:99
for Y, X being set
for R being Relation st Y c= X holds
Y |` (X |` R) = Y |` R
proof
let Y, X be set ; ::_thesis: for R being Relation st Y c= X holds
Y |` (X |` R) = Y |` R
let R be Relation; ::_thesis: ( Y c= X implies Y |` (X |` R) = Y |` R )
 ( Y c= X implies Y /\ X = Y ) by XBOOLE_1:28;
hence  ( Y c= X implies Y |` (X |` R) = Y |` R ) by Th96; ::_thesis: verum
end;

theorem Th100: :: RELAT_1:100
for X, Y being set
for R being Relation st X c= Y holds
X |` R c= Y |` R
proof
let X, Y be set ; ::_thesis: for R being Relation st X c= Y holds
X |` R c= Y |` R
let R be Relation; ::_thesis: ( X c= Y implies X |` R c= Y |` R )
assume A1: X c= Y ; ::_thesis: X |` R c= Y |` R
let x be set ; :: according to RELAT_1:def_3 ::_thesis: for b being set st [x,b] in X |` R holds
[x,b] in Y |` R
let y be set ; ::_thesis: ( [x,y] in X |` R implies [x,y] in Y |` R )
 ( [x,y] in X |` R iff ( [x,y] in R & y in X ) ) by Def12;
hence  ( [x,y] in X |` R implies [x,y] in Y |` R ) by A1, Def12; ::_thesis: verum
end;

theorem Th101: :: RELAT_1:101
for Y being set
for P1, P2 being Relation st P1 c= P2 holds
Y |` P1 c= Y |` P2
proof
let Y be set ; ::_thesis: for P1, P2 being Relation st P1 c= P2 holds
Y |` P1 c= Y |` P2
let P1, P2 be Relation; ::_thesis: ( P1 c= P2 implies Y |` P1 c= Y |` P2 )
assume A1: P1 c= P2 ; ::_thesis: Y |` P1 c= Y |` P2
let x be set ; :: according to RELAT_1:def_3 ::_thesis: for b being set st [x,b] in Y |` P1 holds
[x,b] in Y |` P2
let y be set ; ::_thesis: ( [x,y] in Y |` P1 implies [x,y] in Y |` P2 )
assume  [x,y] in Y |` P1 ; ::_thesis: [x,y] in Y |` P2
then  ( [x,y] in P1 & y in Y ) by Def12;
hence  [x,y] in Y |` P2 by A1, Def12; ::_thesis: verum
end;

theorem :: RELAT_1:102
for Y1, Y2 being set
for P1, P2 being Relation st P1 c= P2 & Y1 c= Y2 holds
Y1 |` P1 c= Y2 |` P2
proof
let Y1, Y2 be set ; ::_thesis: for P1, P2 being Relation st P1 c= P2 & Y1 c= Y2 holds
Y1 |` P1 c= Y2 |` P2
let P1, P2 be Relation; ::_thesis: ( P1 c= P2 & Y1 c= Y2 implies Y1 |` P1 c= Y2 |` P2 )
assume  ( P1 c= P2 & Y1 c= Y2 ) ; ::_thesis: Y1 |` P1 c= Y2 |` P2
then  ( Y1 |` P1 c= Y1 |` P2 & Y1 |` P2 c= Y2 |` P2 ) by Th100, Th101;
hence  Y1 |` P1 c= Y2 |` P2 by XBOOLE_1:1; ::_thesis: verum
end;

theorem :: RELAT_1:103
for X, Y being set
for R being Relation holds (X \/ Y) |` R = (X |` R) \/ (Y |` R)
proof
let X, Y be set ; ::_thesis: for R being Relation holds (X \/ Y) |` R = (X |` R) \/ (Y |` R)
let R be Relation; ::_thesis: (X \/ Y) |` R = (X |` R) \/ (Y |` R)
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b being set holds
( [x,b] in (X \/ Y) |` R iff [x,b] in (X |` R) \/ (Y |` R) )
let y be set ; ::_thesis: ( [x,y] in (X \/ Y) |` R iff [x,y] in (X |` R) \/ (Y |` R) )
A1: ( y in X \/ Y iff ( y in X or y in Y ) ) by XBOOLE_0:def_3;
A2: ( [x,y] in (X |` R) \/ (Y |` R) iff ( [x,y] in X |` R or [x,y] in Y |` R ) ) by XBOOLE_0:def_3;
 ( [x,y] in (X \/ Y) |` R iff ( y in X \/ Y & [x,y] in R ) ) by Def12;
hence  ( [x,y] in (X \/ Y) |` R iff [x,y] in (X |` R) \/ (Y |` R) ) by A1, A2, Def12; ::_thesis: verum
end;

theorem :: RELAT_1:104
for X, Y being set
for R being Relation holds (X /\ Y) |` R = (X |` R) /\ (Y |` R)
proof
let X, Y be set ; ::_thesis: for R being Relation holds (X /\ Y) |` R = (X |` R) /\ (Y |` R)
let R be Relation; ::_thesis: (X /\ Y) |` R = (X |` R) /\ (Y |` R)
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b being set holds
( [x,b] in (X /\ Y) |` R iff [x,b] in (X |` R) /\ (Y |` R) )
let y be set ; ::_thesis: ( [x,y] in (X /\ Y) |` R iff [x,y] in (X |` R) /\ (Y |` R) )
A1: ( y in X /\ Y iff ( y in X & y in Y ) ) by XBOOLE_0:def_4;
A2: ( [x,y] in (X |` R) /\ (Y |` R) iff ( [x,y] in X |` R & [x,y] in Y |` R ) ) by XBOOLE_0:def_4;
 ( [x,y] in (X /\ Y) |` R iff ( y in X /\ Y & [x,y] in R ) ) by Def12;
hence  ( [x,y] in (X /\ Y) |` R iff [x,y] in (X |` R) /\ (Y |` R) ) by A1, A2, Def12; ::_thesis: verum
end;

theorem :: RELAT_1:105
for X, Y being set
for R being Relation holds (X \ Y) |` R = (X |` R) \ (Y |` R)
proof
let X, Y be set ; ::_thesis: for R being Relation holds (X \ Y) |` R = (X |` R) \ (Y |` R)
let R be Relation; ::_thesis: (X \ Y) |` R = (X |` R) \ (Y |` R)
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b being set holds
( [x,b] in (X \ Y) |` R iff [x,b] in (X |` R) \ (Y |` R) )
let y be set ; ::_thesis: ( [x,y] in (X \ Y) |` R iff [x,y] in (X |` R) \ (Y |` R) )
A1: ( y in X \ Y iff ( y in X & not y in Y ) ) by XBOOLE_0:def_5;
A2: ( [x,y] in (X |` R) \ (Y |` R) iff ( [x,y] in X |` R & not [x,y] in Y |` R ) ) by XBOOLE_0:def_5;
 ( [x,y] in X |` R iff ( y in X & [x,y] in R ) ) by Def12;
hence  ( [x,y] in (X \ Y) |` R iff [x,y] in (X |` R) \ (Y |` R) ) by A1, A2, Def12; ::_thesis: verum
end;

theorem :: RELAT_1:106
for R being Relation holds {} |` R = {} ;

theorem :: RELAT_1:107
for Y being set holds Y |` {} = {}
proof
let Y be set ; ::_thesis: Y |` {} = {}
 for x, y being set holds not [x,y] in Y |` {} by Def12;
hence  Y |` {} = {} by Th37; ::_thesis: verum
end;

theorem :: RELAT_1:108
for Y being set
for P, R being Relation holds Y |` (P * R) = P * (Y |` R)
proof
let Y be set ; ::_thesis: for P, R being Relation holds Y |` (P * R) = P * (Y |` R)
let P, R be Relation; ::_thesis: Y |` (P * R) = P * (Y |` R)
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b being set holds
( [x,b] in Y |` (P * R) iff [x,b] in P * (Y |` R) )
let y be set ; ::_thesis: ( [x,y] in Y |` (P * R) iff [x,y] in P * (Y |` R) )
hereby  ::_thesis: ( [x,y] in P * (Y |` R) implies [x,y] in Y |` (P * R) )
assume A1: [x,y] in Y |` (P * R) ; ::_thesis: [x,y] in P * (Y |` R)
then  [x,y] in P * R by Def12;
then consider a being set  such that
A2: [x,a] in P and
A3: [a,y] in R by Def8;
 y in Y by A1, Def12;
then  [a,y] in Y |` R by A3, Def12;
hence  [x,y] in P * (Y |` R) by A2, Def8; ::_thesis: verum
end;
assume  [x,y] in P * (Y |` R) ; ::_thesis: [x,y] in Y |` (P * R)
then consider a being set  such that
A4: [x,a] in P and
A5: [a,y] in Y |` R by Def8;
 [a,y] in R by A5, Def12;
then A6: [x,y] in P * R by A4, Def8;
 y in Y by A5, Def12;
hence  [x,y] in Y |` (P * R) by A6, Def12; ::_thesis: verum
end;

theorem :: RELAT_1:109
for Y, X being set
for R being Relation holds (Y |` R) | X = Y |` (R | X)
proof
let Y, X be set ; ::_thesis: for R being Relation holds (Y |` R) | X = Y |` (R | X)
let R be Relation; ::_thesis: (Y |` R) | X = Y |` (R | X)
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b being set holds
( [x,b] in (Y |` R) | X iff [x,b] in Y |` (R | X) )
let y be set ; ::_thesis: ( [x,y] in (Y |` R) | X iff [x,y] in Y |` (R | X) )
A1: ( ( [x,y] in R & x in X ) iff [x,y] in R | X ) by Def11;
 ( [x,y] in Y |` R iff ( [x,y] in R & y in Y ) ) by Def12;
hence  ( [x,y] in (Y |` R) | X iff [x,y] in Y |` (R | X) ) by A1, Def11, Def12; ::_thesis: verum
end;

definition
let R be Relation;
let X be set ;
funcR .: 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 b1 being set st
for y being set holds
( y in b1 iff ex x being set st
( [x,y] in R & x in X ) )
proof
defpred S1[ set ] means  ex x being set st
( [x,$1] in R & x in X );
consider Y being set  such that
A1: for y being set holds
( y in Y iff ( y in rng R & S1[y] ) ) from XBOOLE_0:sch_1();
take  Y ; ::_thesis: for y being set holds
( y in Y iff ex x being set st
( [x,y] in R & x in X ) )
let y be set ; ::_thesis: ( y in Y iff ex x being set st
( [x,y] in R & x in X ) )
thus  ( y in Y implies ex x being set st
( [x,y] in R & x in X ) ) by A1; ::_thesis: ( ex x being set st
( [x,y] in R & x in X ) implies y in Y )
given x being set  such that A2: [x,y] in R and
A3: x in X ; ::_thesis: y in Y
 y in rng R by A2, XTUPLE_0:def_13;
hence  y in Y by A1, A2, A3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for y being set holds
( y in b1 iff ex x being set st
( [x,y] in R & x in X ) ) ) & ( for y being set holds
( y in b2 iff ex x being set st
( [x,y] in R & x in X ) ) ) holds
b1 = b2
proof
let Y1, Y2 be set ; ::_thesis: ( ( for y being set holds
( y in Y1 iff ex x being set st
( [x,y] in R & x in X ) ) ) & ( for y being set holds
( y in Y2 iff ex x being set st
( [x,y] in R & x in X ) ) ) implies Y1 = Y2 )
assume that
A4: for y being set holds
( y in Y1 iff ex x being set st
( [x,y] in R & x in X ) ) and
A5: for y being set holds
( y in Y2 iff ex x being set st
( [x,y] in R & x in X ) ) ; ::_thesis: Y1 = Y2
now__::_thesis:_for_y_being_set_holds_
(_y_in_Y1_iff_y_in_Y2_)
let y be set ; ::_thesis: ( y in Y1 iff y in Y2 )
 ( y in Y1 iff ex x being set st
( [x,y] in R & x in X ) ) by A4;
hence  ( y in Y1 iff y in Y2 ) by A5; ::_thesis: verum
end;
hence  Y1 = Y2 by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def13 defines .: RELAT_1:def_13_:_
 for R being Relation
for X, b3 being set holds
( b3 = R .: X iff for y being set holds
( y in b3 iff ex x being set st
( [x,y] in R & x in X ) ) );

theorem Th110: :: RELAT_1:110
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 ) )
proof
let y, X be set ; ::_thesis: 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 ) )
let R be Relation; ::_thesis: ( y in R .: X iff ex x being set st
( x in dom R & [x,y] in R & x in X ) )
thus  ( y in R .: X implies ex x being set st
( x in dom R & [x,y] in R & x in X ) ) ::_thesis: ( ex x being set st
( x in dom R & [x,y] in R & x in X ) implies y in R .: X )
proof
assume  y in R .: X ; ::_thesis: ex x being set st
( x in dom R & [x,y] in R & x in X )
then consider x being set  such that
A1: ( [x,y] in R & x in X ) by Def13;
take  x ; ::_thesis: ( x in dom R & [x,y] in R & x in X )
thus  ( x in dom R & [x,y] in R & x in X ) by A1, XTUPLE_0:def_12; ::_thesis: verum
end;
thus  ( ex x being set st
( x in dom R & [x,y] in R & x in X ) implies y in R .: X ) by Def13; ::_thesis: verum
end;

theorem Th111: :: RELAT_1:111
for X being set
for R being Relation holds R .: X c= rng R
proof
let X be set ; ::_thesis: for R being Relation holds R .: X c= rng R
let R be Relation; ::_thesis: R .: X c= rng R
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in R .: X or y in rng R )
assume  y in R .: X ; ::_thesis: y in rng R
then  ex x being set st
( [x,y] in R & x in X ) by Def13;
hence  y in rng R by XTUPLE_0:def_13; ::_thesis: verum
end;

theorem :: RELAT_1:112
for X being set
for R being Relation holds R .: X = R .: ((dom R) /\ X)
proof
let X be set ; ::_thesis: for R being Relation holds R .: X = R .: ((dom R) /\ X)
let R be Relation; ::_thesis: R .: X = R .: ((dom R) /\ X)
 for y being set holds
( y in R .: X iff y in R .: ((dom R) /\ X) )
proof
let y be set ; ::_thesis: ( y in R .: X iff y in R .: ((dom R) /\ X) )
thus  ( y in R .: X implies y in R .: ((dom R) /\ X) ) ::_thesis: ( y in R .: ((dom R) /\ X) implies y in R .: X )
proof
assume  y in R .: X ; ::_thesis: y in R .: ((dom R) /\ X)
then consider x being set  such that
A1: x in dom R and
A2: [x,y] in R and
A3: x in X by Th110;
 x in (dom R) /\ X by A1, A3, XBOOLE_0:def_4;
hence  y in R .: ((dom R) /\ X) by A2, Def13; ::_thesis: verum
end;
assume  y in R .: ((dom R) /\ X) ; ::_thesis: y in R .: X
then consider x being set  such that
 x in dom R and
A4: [x,y] in R and
A5: x in (dom R) /\ X by Th110;
 x in X by A5, XBOOLE_0:def_4;
hence  y in R .: X by A4, Def13; ::_thesis: verum
end;
hence  R .: X = R .: ((dom R) /\ X) by TARSKI:1; ::_thesis: verum
end;

theorem Th113: :: RELAT_1:113
for R being Relation holds R .: (dom R) = rng R
proof
let R be Relation; ::_thesis: R .: (dom R) = rng R
thus  R .: (dom R) c= rng R by Th111; :: according to XBOOLE_0:def_10 ::_thesis: rng R c= R .: (dom R)
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng R or y in R .: (dom R) )
assume  y in rng R ; ::_thesis: y in R .: (dom R)
then consider x being set  such that
A1: [x,y] in R by XTUPLE_0:def_13;
 x in dom R by A1, XTUPLE_0:def_12;
hence  y in R .: (dom R) by A1, Def13; ::_thesis: verum
end;

theorem :: RELAT_1:114
for X being set
for R being Relation holds R .: X c= R .: (dom R)
proof
let X be set ; ::_thesis: for R being Relation holds R .: X c= R .: (dom R)
let R be Relation; ::_thesis: R .: X c= R .: (dom R)
 R .: X c= rng R by Th111;
hence  R .: X c= R .: (dom R) by Th113; ::_thesis: verum
end;

theorem :: RELAT_1:115
for X being set
for R being Relation holds rng (R | X) = R .: X
proof
let X be set ; ::_thesis: for R being Relation holds rng (R | X) = R .: X
let R be Relation; ::_thesis: rng (R | X) = R .: X
 for y being set holds
( y in rng (R | X) iff y in R .: X )
proof
let y be set ; ::_thesis: ( y in rng (R | X) iff y in R .: X )
thus  ( y in rng (R | X) implies y in R .: X ) ::_thesis: ( y in R .: X implies y in rng (R | X) )
proof
assume  y in rng (R | X) ; ::_thesis: y in R .: X
then consider x being set  such that
A1: [x,y] in R | X by XTUPLE_0:def_13;
 ( x in X & [x,y] in R ) by A1, Def11;
hence  y in R .: X by Def13; ::_thesis: verum
end;
assume  y in R .: X ; ::_thesis: y in rng (R | X)
then consider x being set  such that
A2: ( [x,y] in R & x in X ) by Def13;
 [x,y] in R | X by A2, Def11;
hence  y in rng (R | X) by XTUPLE_0:def_13; ::_thesis: verum
end;
hence  rng (R | X) = R .: X by TARSKI:1; ::_thesis: verum
end;

registration
let R be Relation;
let X be empty set ;
clusterR .: X ->  empty ;
coherence
 R .: X is empty
proof
set y = the Element of R .: {};
 ( the Element of R .: {} in R .: {} implies ex x being set st
( [x, the Element of R .: {}] in R & x in {} ) ) by Def13;
hence  R .: X is empty ; ::_thesis: verum
end;
end;

registration
let R be empty Relation;
let X be set ;
clusterR .: X ->  empty ;
coherence
 R .: X is empty
proof
assume  not R .: X is empty ; ::_thesis: contradiction
then  ex x being set st
( [x, the Element of {} .: X] in {} & x in X ) by Def13;
hence  contradiction ; ::_thesis: verum
end;
end;

theorem :: RELAT_1:116
canceled;

theorem :: RELAT_1:117
canceled;

theorem :: RELAT_1:118
for X being set
for R being Relation holds
( R .: X = {} iff dom R misses X )
proof
let X be set ; ::_thesis: for R being Relation holds
( R .: X = {} iff dom R misses X )
let R be Relation; ::_thesis: ( R .: X = {} iff dom R misses X )
set y = the Element of R .: X;
thus  ( R .: X = {} implies dom R misses X ) ::_thesis: ( dom R misses X implies R .: X = {} )
proof
assume A1: R .: X = {} ; ::_thesis: dom R misses X
assume  not dom R misses X ; ::_thesis: contradiction
then consider x being set  such that
A2: x in dom R and
A3: x in X by XBOOLE_0:3;
 ex y being set st [x,y] in R by A2, XTUPLE_0:def_12;
hence  contradiction by A1, A2, A3, Th110; ::_thesis: verum
end;
assume A4: (dom R) /\ X = {} ; :: according to XBOOLE_0:def_7 ::_thesis: R .: X = {}
assume  not R .: X = {} ; ::_thesis: contradiction
then  ex x being set st
( x in dom R & [x, the Element of R .: X] in R & x in X ) by Th110;
hence  contradiction by A4, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem :: RELAT_1:119
for X being set
for R being Relation st X <> {} & X c= dom R holds
R .: X <> {}
proof
let X be set ; ::_thesis: for R being Relation st X <> {} & X c= dom R holds
R .: X <> {}
let R be Relation; ::_thesis: ( X <> {} & X c= dom R implies R .: X <> {} )
assume that
A1: X <> {} and
A2: X c= dom R ; ::_thesis: R .: X <> {}
set x = the Element of X;
A3: the Element of X in dom R by A1, A2, TARSKI:def_3;
then  ex y being set st [ the Element of X,y] in R by XTUPLE_0:def_12;
hence  R .: X <> {} by A1, A3, Th110; ::_thesis: verum
end;

theorem :: RELAT_1:120
for X, Y being set
for R being Relation holds R .: (X \/ Y) = (R .: X) \/ (R .: Y)
proof
let X, Y be set ; ::_thesis: for R being Relation holds R .: (X \/ Y) = (R .: X) \/ (R .: Y)
let R be Relation; ::_thesis: R .: (X \/ Y) = (R .: X) \/ (R .: Y)
thus  R .: (X \/ Y) c= (R .: X) \/ (R .: Y) :: according to XBOOLE_0:def_10 ::_thesis: (R .: X) \/ (R .: Y) c= R .: (X \/ Y)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in R .: (X \/ Y) or y in (R .: X) \/ (R .: Y) )
assume  y in R .: (X \/ Y) ; ::_thesis: y in (R .: X) \/ (R .: Y)
then consider x being set  such that
A1: [x,y] in R and
A2: x in X \/ Y by Def13;
 ( x in X or x in Y ) by A2, XBOOLE_0:def_3;
then  ( y in R .: X or y in R .: Y ) by A1, Def13;
hence  y in (R .: X) \/ (R .: Y) by XBOOLE_0:def_3; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (R .: X) \/ (R .: Y) or y in R .: (X \/ Y) )
assume A3: y in (R .: X) \/ (R .: Y) ; ::_thesis: y in R .: (X \/ Y)
percases ( y in R .: Y or y in R .: X ) by A3, XBOOLE_0:def_3;
suppose y in R .: Y ; ::_thesis: y in R .: (X \/ Y)
then consider x being set  such that
A4: [x,y] in R and
A5: x in Y by Def13;
 x in X \/ Y by A5, XBOOLE_0:def_3;
hence  y in R .: (X \/ Y) by A4, Def13; ::_thesis: verum
end;
suppose y in R .: X ; ::_thesis: y in R .: (X \/ Y)
then consider x being set  such that
A6: [x,y] in R and
A7: x in X by Def13;
 x in X \/ Y by A7, XBOOLE_0:def_3;
hence  y in R .: (X \/ Y) by A6, Def13; ::_thesis: verum
end;
end;
end;

theorem :: RELAT_1:121
for X, Y being set
for R being Relation holds R .: (X /\ Y) c= (R .: X) /\ (R .: Y)
proof
let X, Y be set ; ::_thesis: for R being Relation holds R .: (X /\ Y) c= (R .: X) /\ (R .: Y)
let R be Relation; ::_thesis: R .: (X /\ Y) c= (R .: X) /\ (R .: Y)
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in R .: (X /\ Y) or y in (R .: X) /\ (R .: Y) )
assume  y in R .: (X /\ Y) ; ::_thesis: y in (R .: X) /\ (R .: Y)
then consider x being set  such that
A1: [x,y] in R and
A2: x in X /\ Y by Def13;
 x in Y by A2, XBOOLE_0:def_4;
then A3: y in R .: Y by A1, Def13;
 x in X by A2, XBOOLE_0:def_4;
then  y in R .: X by A1, Def13;
hence  y in (R .: X) /\ (R .: Y) by A3, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem :: RELAT_1:122
for X, Y being set
for R being Relation holds (R .: X) \ (R .: Y) c= R .: (X \ Y)
proof
let X, Y be set ; ::_thesis: for R being Relation holds (R .: X) \ (R .: Y) c= R .: (X \ Y)
let R be Relation; ::_thesis: (R .: X) \ (R .: Y) c= R .: (X \ Y)
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (R .: X) \ (R .: Y) or y in R .: (X \ Y) )
assume A1: y in (R .: X) \ (R .: Y) ; ::_thesis: y in R .: (X \ Y)
then consider x being set  such that
A2: [x,y] in R and
A3: x in X by Def13;
 not y in R .: Y by A1, XBOOLE_0:def_5;
then  ( not x in Y or not [x,y] in R ) by Def13;
then  x in X \ Y by A2, A3, XBOOLE_0:def_5;
hence  y in R .: (X \ Y) by A2, Def13; ::_thesis: verum
end;

theorem Th123: :: RELAT_1:123
for X, Y being set
for R being Relation st X c= Y holds
R .: X c= R .: Y
proof
let X, Y be set ; ::_thesis: for R being Relation st X c= Y holds
R .: X c= R .: Y
let R be Relation; ::_thesis: ( X c= Y implies R .: X c= R .: Y )
assume A1: X c= Y ; ::_thesis: R .: X c= R .: Y
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in R .: X or y in R .: Y )
assume  y in R .: X ; ::_thesis: y in R .: Y
then  ex x being set st
( [x,y] in R & x in X ) by Def13;
hence  y in R .: Y by A1, Def13; ::_thesis: verum
end;

theorem Th124: :: RELAT_1:124
for X being set
for P, R being Relation st P c= R holds
P .: X c= R .: X
proof
let X be set ; ::_thesis: for P, R being Relation st P c= R holds
P .: X c= R .: X
let P, R be Relation; ::_thesis: ( P c= R implies P .: X c= R .: X )
assume A1: P c= R ; ::_thesis: P .: X c= R .: X
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in P .: X or y in R .: X )
assume  y in P .: X ; ::_thesis: y in R .: X
then  ex x being set st
( [x,y] in P & x in X ) by Def13;
hence  y in R .: X by A1, Def13; ::_thesis: verum
end;

theorem :: RELAT_1:125
for X, Y being set
for P, R being Relation st P c= R & X c= Y holds
P .: X c= R .: Y
proof
let X, Y be set ; ::_thesis: for P, R being Relation st P c= R & X c= Y holds
P .: X c= R .: Y
let P, R be Relation; ::_thesis: ( P c= R & X c= Y implies P .: X c= R .: Y )
assume  ( P c= R & X c= Y ) ; ::_thesis: P .: X c= R .: Y
then  ( P .: X c= R .: X & R .: X c= R .: Y ) by Th123, Th124;
hence  P .: X c= R .: Y by XBOOLE_1:1; ::_thesis: verum
end;

theorem :: RELAT_1:126
for X being set
for P, R being Relation holds (P * R) .: X = R .: (P .: X)
proof
let X be set ; ::_thesis: for P, R being Relation holds (P * R) .: X = R .: (P .: X)
let P, R be Relation; ::_thesis: (P * R) .: X = R .: (P .: X)
 for y being set holds
( y in (P * R) .: X iff y in R .: (P .: X) )
proof
let y be set ; ::_thesis: ( y in (P * R) .: X iff y in R .: (P .: X) )
thus  ( y in (P * R) .: X implies y in R .: (P .: X) ) ::_thesis: ( y in R .: (P .: X) implies y in (P * R) .: X )
proof
assume  y in (P * R) .: X ; ::_thesis: y in R .: (P .: X)
then consider x being set  such that
A1: [x,y] in P * R and
A2: x in X by Def13;
consider z being set  such that
A3: [x,z] in P and
A4: [z,y] in R by A1, Def8;
 z in P .: X by A2, A3, Def13;
hence  y in R .: (P .: X) by A4, Def13; ::_thesis: verum
end;
assume  y in R .: (P .: X) ; ::_thesis: y in (P * R) .: X
then consider x being set  such that
A5: [x,y] in R and
A6: x in P .: X by Def13;
consider z being set  such that
A7: [z,x] in P and
A8: z in X by A6, Def13;
 [z,y] in P * R by A5, A7, Def8;
hence  y in (P * R) .: X by A8, Def13; ::_thesis: verum
end;
hence  (P * R) .: X = R .: (P .: X) by TARSKI:1; ::_thesis: verum
end;

theorem Th127: :: RELAT_1:127
for P, R being Relation holds rng (P * R) = R .: (rng P)
proof
let P, R be Relation; ::_thesis: rng (P * R) = R .: (rng P)
 for z being set holds
( z in rng (P * R) iff z in R .: (rng P) )
proof
let z be set ; ::_thesis: ( z in rng (P * R) iff z in R .: (rng P) )
thus  ( z in rng (P * R) implies z in R .: (rng P) ) ::_thesis: ( z in R .: (rng P) implies z in rng (P * R) )
proof
assume  z in rng (P * R) ; ::_thesis: z in R .: (rng P)
then consider x being set  such that
A1: [x,z] in P * R by XTUPLE_0:def_13;
consider y being set  such that
A2: [x,y] in P and
A3: [y,z] in R by A1, Def8;
 y in rng P by A2, XTUPLE_0:def_13;
hence  z in R .: (rng P) by A3, Def13; ::_thesis: verum
end;
assume  z in R .: (rng P) ; ::_thesis: z in rng (P * R)
then consider y being set  such that
A4: [y,z] in R and
A5: y in rng P by Def13;
consider x being set  such that
A6: [x,y] in P by A5, XTUPLE_0:def_13;
 [x,z] in P * R by A4, A6, Def8;
hence  z in rng (P * R) by XTUPLE_0:def_13; ::_thesis: verum
end;
hence  rng (P * R) = R .: (rng P) by TARSKI:1; ::_thesis: verum
end;

theorem :: RELAT_1:128
for X, Y being set
for R being Relation holds (R | X) .: Y c= R .: Y by Th59, Th124;

theorem Th129: :: RELAT_1:129
for R being Relation
for X, Y being set st X c= Y holds
(R | Y) .: X = R .: X
proof
let R be Relation; ::_thesis: for X, Y being set st X c= Y holds
(R | Y) .: X = R .: X
let X, Y be set ; ::_thesis: ( X c= Y implies (R | Y) .: X = R .: X )
assume A1: X c= Y ; ::_thesis: (R | Y) .: X = R .: X
thus  (R | Y) .: X c= R .: X by Th59, Th124; :: according to XBOOLE_0:def_10 ::_thesis: R .: X c= (R | Y) .: X
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in R .: X or y in (R | Y) .: X )
assume  y in R .: X ; ::_thesis: y in (R | Y) .: X
then consider x1 being set  such that
A2: [x1,y] in R and
A3: x1 in X by Def13;
 ex x being set st
( [x,y] in R | Y & x in X )
proof
take  x1 ; ::_thesis: ( [x1,y] in R | Y & x1 in X )
thus  [x1,y] in R | Y by A1, A2, A3, Def11; ::_thesis: x1 in X
thus  x1 in X by A3; ::_thesis: verum
end;
hence  y in (R | Y) .: X by Def13; ::_thesis: verum
end;

theorem :: RELAT_1:130
for X being set
for R being Relation holds (dom R) /\ X c= (R ~) .: (R .: X)
proof
let X be set ; ::_thesis: for R being Relation holds (dom R) /\ X c= (R ~) .: (R .: X)
let R be Relation; ::_thesis: (dom R) /\ X c= (R ~) .: (R .: X)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (dom R) /\ X or x in (R ~) .: (R .: X) )
assume A1: x in (dom R) /\ X ; ::_thesis: x in (R ~) .: (R .: X)
then  x in dom R by XBOOLE_0:def_4;
then consider y being set  such that
A2: [x,y] in R by XTUPLE_0:def_12;
A3: [y,x] in R ~ by A2, Def7;
 x in X by A1, XBOOLE_0:def_4;
then  y in R .: X by A2, Def13;
hence  x in (R ~) .: (R .: X) by A3, Def13; ::_thesis: verum
end;

definition
let R be Relation;
let Y be set ;
funcR " 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 b1 being set st
for x being set holds
( x in b1 iff ex y being set st
( [x,y] in R & y in Y ) )
proof
defpred S1[ set ] means  ex y being set st
( [$1,y] in R & y in Y );
consider X being set  such that
A1: for x being set holds
( x in X iff ( x in dom R & S1[x] ) ) from XBOOLE_0:sch_1();
take  X ; ::_thesis: for x being set holds
( x in X iff ex y being set st
( [x,y] in R & y in Y ) )
let x be set ; ::_thesis: ( x in X iff ex y being set st
( [x,y] in R & y in Y ) )
thus  ( x in X implies ex y being set st
( [x,y] in R & y in Y ) ) by A1; ::_thesis: ( ex y being set st
( [x,y] in R & y in Y ) implies x in X )
given y being set  such that A2: [x,y] in R and
A3: y in Y ; ::_thesis: x in X
 x in dom R by A2, XTUPLE_0:def_12;
hence  x in X by A1, A2, A3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ex y being set st
( [x,y] in R & y in Y ) ) ) & ( for x being set holds
( x in b2 iff ex y being set st
( [x,y] in R & y in Y ) ) ) holds
b1 = b2
proof
let X1, X2 be set ; ::_thesis: ( ( for x being set holds
( x in X1 iff ex y being set st
( [x,y] in R & y in Y ) ) ) & ( for x being set holds
( x in X2 iff ex y being set st
( [x,y] in R & y in Y ) ) ) implies X1 = X2 )
assume that
A4: for x being set holds
( x in X1 iff ex y being set st
( [x,y] in R & y in Y ) ) and
A5: for x being set holds
( x in X2 iff ex y being set st
( [x,y] in R & y in Y ) ) ; ::_thesis: X1 = X2
now__::_thesis:_for_x_being_set_holds_
(_x_in_X1_iff_x_in_X2_)
let x be set ; ::_thesis: ( x in X1 iff x in X2 )
 ( x in X1 iff ex y being set st
( [x,y] in R & y in Y ) ) by A4;
hence  ( x in X1 iff x in X2 ) by A5; ::_thesis: verum
end;
hence  X1 = X2 by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def14 defines " RELAT_1:def_14_:_
 for R being Relation
for Y, b3 being set holds
( b3 = R " Y iff for x being set holds
( x in b3 iff ex y being set st
( [x,y] in R & y in Y ) ) );

theorem Th131: :: RELAT_1:131
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 ) )
proof
let x, Y be set ; ::_thesis: 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 ) )
let R be Relation; ::_thesis: ( x in R " Y iff ex y being set st
( y in rng R & [x,y] in R & y in Y ) )
thus  ( x in R " Y implies ex y being set st
( y in rng R & [x,y] in R & y in Y ) ) ::_thesis: ( ex y being set st
( y in rng R & [x,y] in R & y in Y ) implies x in R " Y )
proof
assume  x in R " Y ; ::_thesis: ex y being set st
( y in rng R & [x,y] in R & y in Y )
then consider y being set  such that
A1: ( [x,y] in R & y in Y ) by Def14;
take  y ; ::_thesis: ( y in rng R & [x,y] in R & y in Y )
thus  ( y in rng R & [x,y] in R & y in Y ) by A1, XTUPLE_0:def_13; ::_thesis: verum
end;
thus  ( ex y being set st
( y in rng R & [x,y] in R & y in Y ) implies x in R " Y ) by Def14; ::_thesis: verum
end;

theorem Th132: :: RELAT_1:132
for Y being set
for R being Relation holds R " Y c= dom R
proof
let Y be set ; ::_thesis: for R being Relation holds R " Y c= dom R
let R be Relation; ::_thesis: R " Y c= dom R
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in R " Y or x in dom R )
assume  x in R " Y ; ::_thesis: x in dom R
then  ex y being set st
( [x,y] in R & y in Y ) by Def14;
hence  x in dom R by XTUPLE_0:def_12; ::_thesis: verum
end;

theorem :: RELAT_1:133
for Y being set
for R being Relation holds R " Y = R " ((rng R) /\ Y)
proof
let Y be set ; ::_thesis: for R being Relation holds R " Y = R " ((rng R) /\ Y)
let R be Relation; ::_thesis: R " Y = R " ((rng R) /\ Y)
 for x being set holds
( x in R " Y iff x in R " ((rng R) /\ Y) )
proof
let x be set ; ::_thesis: ( x in R " Y iff x in R " ((rng R) /\ Y) )
thus  ( x in R " Y implies x in R " ((rng R) /\ Y) ) ::_thesis: ( x in R " ((rng R) /\ Y) implies x in R " Y )
proof
assume  x in R " Y ; ::_thesis: x in R " ((rng R) /\ Y)
then consider y being set  such that
A1: y in rng R and
A2: [x,y] in R and
A3: y in Y by Th131;
 y in (rng R) /\ Y by A1, A3, XBOOLE_0:def_4;
hence  x in R " ((rng R) /\ Y) by A2, Def14; ::_thesis: verum
end;
assume  x in R " ((rng R) /\ Y) ; ::_thesis: x in R " Y
then consider y being set  such that
 y in rng R and
A4: [x,y] in R and
A5: y in (rng R) /\ Y by Th131;
 y in Y by A5, XBOOLE_0:def_4;
hence  x in R " Y by A4, Def14; ::_thesis: verum
end;
hence  R " Y = R " ((rng R) /\ Y) by TARSKI:1; ::_thesis: verum
end;

theorem Th134: :: RELAT_1:134
for R being Relation holds R " (rng R) = dom R
proof
let R be Relation; ::_thesis: R " (rng R) = dom R
thus  R " (rng R) c= dom R by Th132; :: according to XBOOLE_0:def_10 ::_thesis: dom R c= R " (rng R)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom R or x in R " (rng R) )
assume  x in dom R ; ::_thesis: x in R " (rng R)
then consider y being set  such that
A1: [x,y] in R by XTUPLE_0:def_12;
 y in rng R by A1, XTUPLE_0:def_13;
hence  x in R " (rng R) by A1, Def14; ::_thesis: verum
end;

theorem :: RELAT_1:135
for Y being set
for R being Relation holds R " Y c= R " (rng R)
proof
let Y be set ; ::_thesis: for R being Relation holds R " Y c= R " (rng R)
let R be Relation; ::_thesis: R " Y c= R " (rng R)
 R " Y c= dom R by Th132;
hence  R " Y c= R " (rng R) by Th134; ::_thesis: verum
end;

registration
let R be Relation;
let Y be empty set ;
clusterR " Y ->  empty ;
coherence
 R " Y is empty
proof
set x = the Element of R " {};
 ( the Element of R " {} in R " {} implies ex y being set st
( [ the Element of R " {},y] in R & y in {} ) ) by Def14;
hence  R " Y is empty ; ::_thesis: verum
end;
end;

registration
let R be empty Relation;
let Y be set ;
clusterR " Y ->  empty ;
coherence
 R " Y is empty
proof
assume  not R " Y is empty ; ::_thesis: contradiction
then  ex y being set st
( [ the Element of {} " Y,y] in {} & y in Y ) by Def14;
hence  contradiction ; ::_thesis: verum
end;
end;

theorem :: RELAT_1:136
canceled;

theorem :: RELAT_1:137
canceled;

theorem :: RELAT_1:138
for Y being set
for R being Relation holds
( R " Y = {} iff rng R misses Y )
proof
let Y be set ; ::_thesis: for R being Relation holds
( R " Y = {} iff rng R misses Y )
let R be Relation; ::_thesis: ( R " Y = {} iff rng R misses Y )
set x = the Element of R " Y;
thus  ( R " Y = {} implies rng R misses Y ) ::_thesis: ( rng R misses Y implies R " Y = {} )
proof
assume A1: R " Y = {} ; ::_thesis: rng R misses Y
assume  not rng R misses Y ; ::_thesis: contradiction
then consider y being set  such that
A2: y in rng R and
A3: y in Y by XBOOLE_0:3;
 ex x being set st [x,y] in R by A2, XTUPLE_0:def_13;
hence  contradiction by A1, A2, A3, Th131; ::_thesis: verum
end;
assume A4: (rng R) /\ Y = {} ; :: according to XBOOLE_0:def_7 ::_thesis: R " Y = {}
assume  not R " Y = {} ; ::_thesis: contradiction
then  ex y being set st
( y in rng R & [ the Element of R " Y,y] in R & y in Y ) by Th131;
hence  contradiction by A4, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem :: RELAT_1:139
for Y being set
for R being Relation st Y <> {} & Y c= rng R holds
R " Y <> {}
proof
let Y be set ; ::_thesis: for R being Relation st Y <> {} & Y c= rng R holds
R " Y <> {}
let R be Relation; ::_thesis: ( Y <> {} & Y c= rng R implies R " Y <> {} )
assume that
A1: Y <> {} and
A2: Y c= rng R ; ::_thesis: R " Y <> {}
set y = the Element of Y;
A3: the Element of Y in rng R by A1, A2, TARSKI:def_3;
then  ex x being set st [x, the Element of Y] in R by XTUPLE_0:def_13;
hence  R " Y <> {} by A1, A3, Th131; ::_thesis: verum
end;

theorem :: RELAT_1:140
for X, Y being set
for R being Relation holds R " (X \/ Y) = (R " X) \/ (R " Y)
proof
let X, Y be set ; ::_thesis: for R being Relation holds R " (X \/ Y) = (R " X) \/ (R " Y)
let R be Relation; ::_thesis: R " (X \/ Y) = (R " X) \/ (R " Y)
thus  R " (X \/ Y) c= (R " X) \/ (R " Y) :: according to XBOOLE_0:def_10 ::_thesis: (R " X) \/ (R " Y) c= R " (X \/ Y)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in R " (X \/ Y) or x in (R " X) \/ (R " Y) )
assume  x in R " (X \/ Y) ; ::_thesis: x in (R " X) \/ (R " Y)
then consider y being set  such that
A1: [x,y] in R and
A2: y in X \/ Y by Def14;
 ( y in X or y in Y ) by A2, XBOOLE_0:def_3;
then  ( x in R " X or x in R " Y ) by A1, Def14;
hence  x in (R " X) \/ (R " Y) by XBOOLE_0:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (R " X) \/ (R " Y) or x in R " (X \/ Y) )
assume A3: x in (R " X) \/ (R " Y) ; ::_thesis: x in R " (X \/ Y)
percases ( x in R " Y or x in R " X ) by A3, XBOOLE_0:def_3;
suppose x in R " Y ; ::_thesis: x in R " (X \/ Y)
then consider y being set  such that
A4: [x,y] in R and
A5: y in Y by Def14;
 y in X \/ Y by A5, XBOOLE_0:def_3;
hence  x in R " (X \/ Y) by A4, Def14; ::_thesis: verum
end;
suppose x in R " X ; ::_thesis: x in R " (X \/ Y)
then consider y being set  such that
A6: [x,y] in R and
A7: y in X by Def14;
 y in X \/ Y by A7, XBOOLE_0:def_3;
hence  x in R " (X \/ Y) by A6, Def14; ::_thesis: verum
end;
end;
end;

theorem :: RELAT_1:141
for X, Y being set
for R being Relation holds R " (X /\ Y) c= (R " X) /\ (R " Y)
proof
let X, Y be set ; ::_thesis: for R being Relation holds R " (X /\ Y) c= (R " X) /\ (R " Y)
let R be Relation; ::_thesis: R " (X /\ Y) c= (R " X) /\ (R " Y)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in R " (X /\ Y) or x in (R " X) /\ (R " Y) )
assume  x in R " (X /\ Y) ; ::_thesis: x in (R " X) /\ (R " Y)
then consider y being set  such that
A1: [x,y] in R and
A2: y in X /\ Y by Def14;
 y in Y by A2, XBOOLE_0:def_4;
then A3: x in R " Y by A1, Def14;
 y in X by A2, XBOOLE_0:def_4;
then  x in R " X by A1, Def14;
hence  x in (R " X) /\ (R " Y) by A3, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem :: RELAT_1:142
for X, Y being set
for R being Relation holds (R " X) \ (R " Y) c= R " (X \ Y)
proof
let X, Y be set ; ::_thesis: for R being Relation holds (R " X) \ (R " Y) c= R " (X \ Y)
let R be Relation; ::_thesis: (R " X) \ (R " Y) c= R " (X \ Y)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (R " X) \ (R " Y) or x in R " (X \ Y) )
assume A1: x in (R " X) \ (R " Y) ; ::_thesis: x in R " (X \ Y)
then consider y being set  such that
A2: [x,y] in R and
A3: y in X by Def14;
 not x in R " Y by A1, XBOOLE_0:def_5;
then  ( not y in Y or not [x,y] in R ) by Def14;
then  y in X \ Y by A2, A3, XBOOLE_0:def_5;
hence  x in R " (X \ Y) by A2, Def14; ::_thesis: verum
end;

theorem Th143: :: RELAT_1:143
for X, Y being set
for R being Relation st X c= Y holds
R " X c= R " Y
proof
let X, Y be set ; ::_thesis: for R being Relation st X c= Y holds
R " X c= R " Y
let R be Relation; ::_thesis: ( X c= Y implies R " X c= R " Y )
assume A1: X c= Y ; ::_thesis: R " X c= R " Y
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in R " X or x in R " Y )
assume  x in R " X ; ::_thesis: x in R " Y
then  ex y being set st
( [x,y] in R & y in X ) by Def14;
hence  x in R " Y by A1, Def14; ::_thesis: verum
end;

theorem Th144: :: RELAT_1:144
for Y being set
for P, R being Relation st P c= R holds
P " Y c= R " Y
proof
let Y be set ; ::_thesis: for P, R being Relation st P c= R holds
P " Y c= R " Y
let P, R be Relation; ::_thesis: ( P c= R implies P " Y c= R " Y )
assume A1: P c= R ; ::_thesis: P " Y c= R " Y
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P " Y or x in R " Y )
assume  x in P " Y ; ::_thesis: x in R " Y
then  ex y being set st
( [x,y] in P & y in Y ) by Def14;
hence  x in R " Y by A1, Def14; ::_thesis: verum
end;

theorem :: RELAT_1:145
for X, Y being set
for P, R being Relation st P c= R & X c= Y holds
P " X c= R " Y
proof
let X, Y be set ; ::_thesis: for P, R being Relation st P c= R & X c= Y holds
P " X c= R " Y
let P, R be Relation; ::_thesis: ( P c= R & X c= Y implies P " X c= R " Y )
assume  ( P c= R & X c= Y ) ; ::_thesis: P " X c= R " Y
then  ( P " X c= R " X & R " X c= R " Y ) by Th143, Th144;
hence  P " X c= R " Y by XBOOLE_1:1; ::_thesis: verum
end;

theorem :: RELAT_1:146
for Y being set
for P, R being Relation holds (P * R) " Y = P " (R " Y)
proof
let Y be set ; ::_thesis: for P, R being Relation holds (P * R) " Y = P " (R " Y)
let P, R be Relation; ::_thesis: (P * R) " Y = P " (R " Y)
 for x being set holds
( x in (P * R) " Y iff x in P " (R " Y) )
proof
let x be set ; ::_thesis: ( x in (P * R) " Y iff x in P " (R " Y) )
thus  ( x in (P * R) " Y implies x in P " (R " Y) ) ::_thesis: ( x in P " (R " Y) implies x in (P * R) " Y )
proof
assume  x in (P * R) " Y ; ::_thesis: x in P " (R " Y)
then consider y being set  such that
A1: [x,y] in P * R and
A2: y in Y by Def14;
consider z being set  such that
A3: [x,z] in P and
A4: [z,y] in R by A1, Def8;
 z in R " Y by A2, A4, Def14;
hence  x in P " (R " Y) by A3, Def14; ::_thesis: verum
end;
assume  x in P " (R " Y) ; ::_thesis: x in (P * R) " Y
then consider y being set  such that
A5: [x,y] in P and
A6: y in R " Y by Def14;
consider z being set  such that
A7: [y,z] in R and
A8: z in Y by A6, Def14;
 [x,z] in P * R by A5, A7, Def8;
hence  x in (P * R) " Y by A8, Def14; ::_thesis: verum
end;
hence  (P * R) " Y = P " (R " Y) by TARSKI:1; ::_thesis: verum
end;

theorem Th147: :: RELAT_1:147
for P, R being Relation holds dom (P * R) = P " (dom R)
proof
let P, R be Relation; ::_thesis: dom (P * R) = P " (dom R)
 for z being set holds
( z in dom (P * R) iff z in P " (dom R) )
proof
let z be set ; ::_thesis: ( z in dom (P * R) iff z in P " (dom R) )
thus  ( z in dom (P * R) implies z in P " (dom R) ) ::_thesis: ( z in P " (dom R) implies z in dom (P * R) )
proof
assume  z in dom (P * R) ; ::_thesis: z in P " (dom R)
then consider x being set  such that
A1: [z,x] in P * R by XTUPLE_0:def_12;
consider y being set  such that
A2: [z,y] in P and
A3: [y,x] in R by A1, Def8;
 y in dom R by A3, XTUPLE_0:def_12;
hence  z in P " (dom R) by A2, Def14; ::_thesis: verum
end;
assume  z in P " (dom R) ; ::_thesis: z in dom (P * R)
then consider y being set  such that
A4: [z,y] in P and
A5: y in dom R by Def14;
consider x being set  such that
A6: [y,x] in R by A5, XTUPLE_0:def_12;
 [z,x] in P * R by A4, A6, Def8;
hence  z in dom (P * R) by XTUPLE_0:def_12; ::_thesis: verum
end;
hence  dom (P * R) = P " (dom R) by TARSKI:1; ::_thesis: verum
end;

theorem :: RELAT_1:148
for Y being set
for R being Relation holds (rng R) /\ Y c= (R ~) " (R " Y)
proof
let Y be set ; ::_thesis: for R being Relation holds (rng R) /\ Y c= (R ~) " (R " Y)
let R be Relation; ::_thesis: (rng R) /\ Y c= (R ~) " (R " Y)
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (rng R) /\ Y or y in (R ~) " (R " Y) )
assume A1: y in (rng R) /\ Y ; ::_thesis: y in (R ~) " (R " Y)
then  y in rng R by XBOOLE_0:def_4;
then consider x being set  such that
A2: [x,y] in R by XTUPLE_0:def_13;
A3: [y,x] in R ~ by A2, Def7;
 y in Y by A1, XBOOLE_0:def_4;
then  x in R " Y by A2, Def14;
hence  y in (R ~) " (R " Y) by A3, Def14; ::_thesis: verum
end;

begin

definition
let R be Relation;
attrR is empty-yielding  means :Def15: :: RELAT_1:def 15
 rng R c= {{}};
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:149
for R being Relation holds
( R is empty-yielding iff for X being set st X in rng R holds
X = {} )
proof
let R be Relation; ::_thesis: ( R is empty-yielding iff for X being set st X in rng R holds
X = {} )
hereby  ::_thesis: ( ( for X being set st X in rng R holds
X = {} ) implies R is empty-yielding )
assume  R is empty-yielding ; ::_thesis: for X being set st X in rng R holds
X = {}
then  rng R c= {{}} by Def15;
hence  for X being set st X in rng R holds
X = {} by TARSKI:def_1; ::_thesis: verum
end;
assume A1: for X being set st X in rng R holds
X = {} ; ::_thesis: R is empty-yielding
let Y be set ; :: according to TARSKI:def_3,RELAT_1:def_15 ::_thesis: ( not Y in rng R or Y in {{}} )
assume  Y in rng R ; ::_thesis: Y in {{}}
then  Y = {} by A1;
hence  Y in {{}} by TARSKI:def_1; ::_thesis: verum
end;

theorem :: RELAT_1:150
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)
proof
let f, g be Relation; ::_thesis: for A, B being set st f | A = g | A & f | B = g | B holds
f | (A \/ B) = g | (A \/ B)
let A, B be set ; ::_thesis: ( f | A = g | A & f | B = g | B implies f | (A \/ B) = g | (A \/ B) )
assume  ( f | A = g | A & f | B = g | B ) ; ::_thesis: f | (A \/ B) = g | (A \/ B)
hence f | (A \/ B) = (g | A) \/ (g | B) by Th78
.= g | (A \/ B) by Th78 ;
::_thesis: verum
end;

theorem :: RELAT_1:151
for X being set
for f, g being Relation st dom g c= X & g c= f holds
g c= f | X
proof
let X be set ; ::_thesis: for f, g being Relation st dom g c= X & g c= f holds
g c= f | X
let f, g be Relation; ::_thesis: ( dom g c= X & g c= f implies g c= f | X )
assume  ( dom g c= X & g c= f ) ; ::_thesis: g c= f | X
then  g | (dom g) c= f | X by Th77;
hence  g c= f | X ; ::_thesis: verum
end;

theorem :: RELAT_1:152
for f being Relation
for X being set st X misses dom f holds
f | X = {}
proof
let f be Relation; ::_thesis: for X being set st X misses dom f holds
f | X = {}
let X be set ; ::_thesis: ( X misses dom f implies f | X = {} )
assume A1: X /\ (dom f) = {} ; :: according to XBOOLE_0:def_7 ::_thesis: f | X = {}
thus f | X = (f | (dom f)) | X
.= f | {} by A1, Th71
.= {} ; ::_thesis: verum
end;

theorem :: RELAT_1:153
for f, g being Relation
for A, B being set st A c= B & f | B = g | B holds
f | A = g | A
proof
let f, g be Relation; ::_thesis: for A, B being set st A c= B & f | B = g | B holds
f | A = g | A
let A, B be set ; ::_thesis: ( A c= B & f | B = g | B implies f | A = g | A )
assume that
A1: A c= B and
A2: f | B = g | B ; ::_thesis: f | A = g | A
A3: A = B /\ A by A1, XBOOLE_1:28;
hence f | A = (f | B) | A by Th71
.= g | A by A2, A3, Th71 ;
::_thesis: verum
end;

theorem :: RELAT_1:154
for R, S being Relation holds R | (dom S) = R | (dom (S | (dom R)))
proof
let R, S be Relation; ::_thesis: R | (dom S) = R | (dom (S | (dom R)))
thus R | (dom S) = (R | (dom R)) | (dom S)
.= R | ((dom S) /\ (dom R)) by Th71
.= R | (dom (S | (dom R))) by Th61 ; ::_thesis: verum
end;

registration
cluster empty Relation-like  ->  empty-yielding for set ;
coherence
 for b1 being Relation st b1 is empty holds
b1 is empty-yielding
proof
let R be Relation; ::_thesis: ( R is empty implies R is empty-yielding )
assume  R is empty ; ::_thesis: R is empty-yielding
then  rng R = {} ;
hence  rng R c= {{}} by XBOOLE_1:2; :: according to RELAT_1:def_15 ::_thesis: verum
end;
end;

registration
let R be empty-yielding Relation;
let X be set ;
clusterR | X ->  empty-yielding ;
coherence
 R | X is empty-yielding
proof
 ( rng R c= {{}} & rng (R | X) c= rng R ) by Def15, Th70;
hence  rng (R | X) c= {{}} by XBOOLE_1:1; :: according to RELAT_1:def_15 ::_thesis: verum
end;
end;

theorem :: RELAT_1:155
for X being set
for R being Relation st not R | X is empty-yielding holds
not R is empty-yielding ;

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;

:: 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{ F1() ->  Relation, F2() ->  Relation, P1[ set , set ] } :
 F1() = F2()
provided
A1: for a, b being set holds
( [a,b] in F1() iff P1[a,b] ) and
A2: for a, b being set holds
( [a,b] in F2() iff P1[a,b] )
proof
let y, z be set ; :: according to RELAT_1:def_2 ::_thesis: ( [y,z] in F1() iff [y,z] in F2() )
hereby  ::_thesis: ( [y,z] in F2() implies [y,z] in F1() )
assume  [y,z] in F1() ; ::_thesis: [y,z] in F2()
then  P1[y,z] by A1;
hence  [y,z] in F2() by A2; ::_thesis: verum
end;
assume  [y,z] in F2() ; ::_thesis: [y,z] in F1()
then  P1[y,z] by A2;
hence  [y,z] in F1() by A1; ::_thesis: verum
end;

theorem :: RELAT_1:156
for X being set
for R being Relation holds dom (R | ((dom R) \ X)) = (dom R) \ X
proof
let X be set ; ::_thesis: for R being Relation holds dom (R | ((dom R) \ X)) = (dom R) \ X
let R be Relation; ::_thesis: dom (R | ((dom R) \ X)) = (dom R) \ X
thus  dom (R | ((dom R) \ X)) = (dom R) /\ ((dom R) \ X) by Th61
.= ((dom R) /\ (dom R)) \ X by XBOOLE_1:49
.= (dom R) \ X ; ::_thesis: verum
end;

theorem :: RELAT_1:157
for X being set
for R being Relation holds R | X = R | ((dom R) /\ X)
proof
let X be set ; ::_thesis: for R being Relation holds R | X = R | ((dom R) /\ X)
let R be Relation; ::_thesis: R | X = R | ((dom R) /\ X)
thus R | X = (R | (dom R)) | X
.= R | ((dom R) /\ X) by Th71 ; ::_thesis: verum
end;

theorem :: RELAT_1:158
for X, Y being set holds dom [:X,Y:] c= X
proof
let X, Y be set ; ::_thesis: dom [:X,Y:] c= X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom [:X,Y:] or x in X )
assume  x in dom [:X,Y:] ; ::_thesis: x in X
then  ex y being set st [x,y] in [:X,Y:] by XTUPLE_0:def_12;
hence  x in X by ZFMISC_1:87; ::_thesis: verum
end;

theorem :: RELAT_1:159
for X, Y being set holds rng [:X,Y:] c= Y
proof
let X, Y be set ; ::_thesis: rng [:X,Y:] c= Y
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng [:X,Y:] or x in Y )
assume  x in rng [:X,Y:] ; ::_thesis: x in Y
then  ex y being set st [y,x] in [:X,Y:] by XTUPLE_0:def_13;
hence  x in Y by ZFMISC_1:87; ::_thesis: verum
end;

theorem :: RELAT_1:160
for X, Y being set st X <> {} & Y <> {} holds
( dom [:X,Y:] = X & rng [:X,Y:] = Y )
proof
let X, Y be set ; ::_thesis: ( X <> {} & Y <> {} implies ( dom [:X,Y:] = X & rng [:X,Y:] = Y ) )
assume  X <> {} ; ::_thesis: ( not Y <> {} or ( dom [:X,Y:] = X & rng [:X,Y:] = Y ) )
then consider a being set  such that
A1: a in X by XBOOLE_0:def_1;
assume  Y <> {} ; ::_thesis: ( dom [:X,Y:] = X & rng [:X,Y:] = Y )
then consider b being set  such that
A2: b in Y by XBOOLE_0:def_1;
A3: now__::_thesis:_for_x_being_set_st_x_in_X_holds_
ex_y_being_set_st_[x,y]_in_[:X,Y:]
let x be set ; ::_thesis: ( x in X implies ex y being set st [x,y] in [:X,Y:] )
assume  x in X ; ::_thesis: ex y being set st [x,y] in [:X,Y:]
then  [x,b] in [:X,Y:] by A2, ZFMISC_1:87;
hence  ex y being set st [x,y] in [:X,Y:] ; ::_thesis: verum
end;
 for x being set st ex y being set st [x,y] in [:X,Y:] holds
x in X by ZFMISC_1:87;
hence  dom [:X,Y:] = X by A3, XTUPLE_0:def_12; ::_thesis: rng [:X,Y:] = Y
A4: now__::_thesis:_for_y_being_set_st_y_in_Y_holds_
ex_x_being_set_st_[x,y]_in_[:X,Y:]
let y be set ; ::_thesis: ( y in Y implies ex x being set st [x,y] in [:X,Y:] )
assume  y in Y ; ::_thesis: ex x being set st [x,y] in [:X,Y:]
then  [a,y] in [:X,Y:] by A1, ZFMISC_1:87;
hence  ex x being set st [x,y] in [:X,Y:] ; ::_thesis: verum
end;
 for y being set st ex x being set st [x,y] in [:X,Y:] holds
y in Y by ZFMISC_1:87;
hence  rng [:X,Y:] = Y by A4, XTUPLE_0:def_13; ::_thesis: verum
end;

theorem :: RELAT_1:161
for R, Q being Relation st dom R = {} & dom Q = {} holds
R = Q
proof
let R, Q be Relation; ::_thesis: ( dom R = {} & dom Q = {} implies R = Q )
assume that
A1: dom R = {} and
A2: dom Q = {} ; ::_thesis: R = Q
 R = {} by A1;
hence  R = Q by A2; ::_thesis: verum
end;

theorem :: RELAT_1:162
for R, Q being Relation st rng R = {} & rng Q = {} holds
R = Q
proof
let R, Q be Relation; ::_thesis: ( rng R = {} & rng Q = {} implies R = Q )
assume that
A1: rng R = {} and
A2: rng Q = {} ; ::_thesis: R = Q
 R = {} by A1;
hence  R = Q by A2; ::_thesis: verum
end;

theorem :: RELAT_1:163
for R, Q, S being Relation st dom R = dom Q holds
dom (S * R) = dom (S * Q)
proof
let R, Q, S be Relation; ::_thesis: ( dom R = dom Q implies dom (S * R) = dom (S * Q) )
assume A1: dom R = dom Q ; ::_thesis: dom (S * R) = dom (S * Q)
thus  dom (S * R) = S " (dom R) by Th147
.= dom (S * Q) by A1, Th147 ; ::_thesis: verum
end;

theorem :: RELAT_1:164
for R, Q, S being Relation st rng R = rng Q holds
rng (R * S) = rng (Q * S)
proof
let R, Q, S be Relation; ::_thesis: ( rng R = rng Q implies rng (R * S) = rng (Q * S) )
assume A1: rng R = rng Q ; ::_thesis: rng (R * S) = rng (Q * S)
thus  rng (R * S) = S .: (rng R) by Th127
.= rng (Q * S) by A1, Th127 ; ::_thesis: verum
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;

:: deftheorem  defines Coim RELAT_1:def_17_:_
 for R being Relation
for x being set holds Coim (R,x) = R " {x};

registration
let R be trivial Relation;
cluster dom R ->  trivial ;
coherence
 dom R is trivial
proof
let x be set ; :: according to ZFMISC_1:def_10 ::_thesis: for b1 being set holds
( not x in dom R or not b1 in dom R or x = b1 )
let y be set ; ::_thesis: ( not x in dom R or not y in dom R or x = y )
assume  x in dom R ; ::_thesis: ( not y in dom R or x = y )
then consider a being set  such that
A1: [x,a] in R by XTUPLE_0:def_12;
assume  y in dom R ; ::_thesis: x = y
then consider b being set  such that
A2: [y,b] in R by XTUPLE_0:def_12;
 [x,a] = [y,b] by A1, A2, ZFMISC_1:def_10;
hence  x = y by XTUPLE_0:1; ::_thesis: verum
end;
end;

registration
let R be trivial Relation;
cluster rng R ->  trivial ;
coherence
 rng R is trivial
proof
let x be set ; :: according to ZFMISC_1:def_10 ::_thesis: for b1 being set holds
( not x in rng R or not b1 in rng R or x = b1 )
let y be set ; ::_thesis: ( not x in rng R or not y in rng R or x = y )
assume  x in rng R ; ::_thesis: ( not y in rng R or x = y )
then consider a being set  such that
A1: [a,x] in R by XTUPLE_0:def_13;
assume  y in rng R ; ::_thesis: x = y
then consider b being set  such that
A2: [b,y] in R by XTUPLE_0:def_13;
 [a,x] = [b,y] by A1, A2, ZFMISC_1:def_10;
hence  x = y by XTUPLE_0:1; ::_thesis: verum
end;
end;

theorem :: RELAT_1:165
for X being set
for R, S being Relation st rng R c= dom (S | X) holds
R * (S | X) = R * S
proof
let X be set ; ::_thesis: for R, S being Relation st rng R c= dom (S | X) holds
R * (S | X) = R * S
let R, S be Relation; ::_thesis: ( rng R c= dom (S | X) implies R * (S | X) = R * S )
assume A1: rng R c= dom (S | X) ; ::_thesis: R * (S | X) = R * S
let a be set ; :: according to RELAT_1:def_2 ::_thesis: for b being set holds
( [a,b] in R * (S | X) iff [a,b] in R * S )
let b be set ; ::_thesis: ( [a,b] in R * (S | X) iff [a,b] in R * S )
 R * (S | X) c= R * S by Th29, Th59;
hence  ( [a,b] in R * (S | X) implies [a,b] in R * S ) ; ::_thesis: ( [a,b] in R * S implies [a,b] in R * (S | X) )
assume  [a,b] in R * S ; ::_thesis: [a,b] in R * (S | X)
then consider c being set  such that
A2: [a,c] in R and
A3: [c,b] in S by Def8;
 c in rng R by A2, XTUPLE_0:def_13;
then  c in X by A1, Th57;
then  [c,b] in S | X by A3, Def11;
hence  [a,b] in R * (S | X) by A2, Def8; ::_thesis: verum
end;

theorem :: RELAT_1:166
for A being set
for Q, R being Relation st Q | A = R | A holds
Q .: A = R .: A
proof
let A be set ; ::_thesis: for Q, R being Relation st Q | A = R | A holds
Q .: A = R .: A
let Q, R be Relation; ::_thesis: ( Q | A = R | A implies Q .: A = R .: A )
assume  Q | A = R | A ; ::_thesis: Q .: A = R .: A
hence Q .: A = (R | A) .: A by Th129
.= R .: A by Th129 ;
::_thesis: verum
end;

definition
let X be set ;
let R be Relation;
attrR is X -defined  means :Def18: :: RELAT_1:def 18
 dom R c= X;
attrR is X -valued  means :Def19: :: RELAT_1:def 19
 rng R c= X;
end;

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

Lm1:  for X, Y being set holds
( {} is X -defined & {} is Y -valued )
proof
let X, Y be set ; ::_thesis: ( {} is X -defined & {} is Y -valued )
thus  ( dom {} c= X & rng {} c= Y ) by XBOOLE_1:2; :: according to RELAT_1:def_18,RELAT_1:def_19 ::_thesis: verum
end;

registration
let X, Y be set ;
cluster Relation-like X -defined Y -valued for set ;
existence
 ex b1 being Relation st
( b1 is X -defined & b1 is Y -valued )
proof
take  {} ; ::_thesis: ( {} is X -defined & {} is Y -valued )
thus  ( {} is X -defined & {} is Y -valued ) by Lm1; ::_thesis: verum
end;
end;

theorem :: RELAT_1:167
for D being set
for R being b1 -valued Relation
for y being set st y in rng R holds
y in D
proof
let D be set ; ::_thesis: for R being D -valued Relation
for y being set st y in rng R holds
y in D
let R be D -valued Relation; ::_thesis: for y being set st y in rng R holds
y in D
 rng R c= D by Def19;
hence  for y being set st y in rng R holds
y in D ; ::_thesis: verum
end;

registration
let X, A be set ;
let R be A -valued Relation;
clusterR | X -> A -valued ;
coherence
 R | X is A -valued
proof
 ( rng (R | X) c= rng R & rng R c= A ) by Def19, Th70;
hence  rng (R | X) c= A by XBOOLE_1:1; :: according to RELAT_1:def_19 ::_thesis: verum
end;
end;

registration
let X, A be set ;
let R be A -defined Relation;
clusterR | X -> X -defined A -defined ;
coherence
 ( R | X is A -defined & R | X is X -defined )
proof
 ( dom (R | X) c= dom R & dom R c= A ) by Def18, Th60;
hence  dom (R | X) c= A by XBOOLE_1:1; :: according to RELAT_1:def_18 ::_thesis: R | X is X -defined
thus  dom (R | X) c= X by Th58; :: according to RELAT_1:def_18 ::_thesis: verum
end;
end;

registration
let X be set ;
cluster id X -> X -defined X -valued ;
coherence
 ( id X is X -defined & id X is X -valued )
proof
thus  ( dom (id X) c= X & rng (id X) c= X ) ; :: according to RELAT_1:def_18,RELAT_1:def_19 ::_thesis: verum
end;
end;

registration
let A be set ;
let R be A -valued Relation;
let S be Relation;
clusterS (#) R -> A -valued ;
coherence
 S * R is A -valued
proof
 ( rng R c= A & rng (S * R) c= rng R ) by Def19, Th26;
hence  rng (S * R) c= A by XBOOLE_1:1; :: according to RELAT_1:def_19 ::_thesis: verum
end;
end;

registration
let A be set ;
let R be A -defined Relation;
let S be Relation;
clusterR (#) S -> A -defined ;
coherence
 R * S is A -defined
proof
 ( dom R c= A & dom (R * S) c= dom R ) by Def18, Th25;
hence  dom (R * S) c= A by XBOOLE_1:1; :: according to RELAT_1:def_18 ::_thesis: verum
end;
end;

theorem :: RELAT_1:168
for x, X, Y being set st x in X holds
Im ([:X,Y:],x) = Y
proof
let x, X, Y be set ; ::_thesis: ( x in X implies Im ([:X,Y:],x) = Y )
assume A1: x in X ; ::_thesis: Im ([:X,Y:],x) = Y
thus  Im ([:X,Y:],x) c= Y :: according to XBOOLE_0:def_10 ::_thesis: Y c= Im ([:X,Y:],x)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Im ([:X,Y:],x) or y in Y )
assume  y in Im ([:X,Y:],x) ; ::_thesis: y in Y
then  ex z being set st
( [z,y] in [:X,Y:] & z in {x} ) by Def13;
hence  y in Y by ZFMISC_1:87; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Y or y in Im ([:X,Y:],x) )
assume  y in Y ; ::_thesis: y in Im ([:X,Y:],x)
then A2: [x,y] in [:X,Y:] by A1, ZFMISC_1:87;
 x in {x} by TARSKI:def_1;
hence  y in Im ([:X,Y:],x) by A2, Def13; ::_thesis: verum
end;

theorem Th169: :: RELAT_1:169
for x, y being set
for R being Relation holds
( [x,y] in R iff y in Im (R,x) )
proof
let x, y be set ; ::_thesis: for R being Relation holds
( [x,y] in R iff y in Im (R,x) )
let R be Relation; ::_thesis: ( [x,y] in R iff y in Im (R,x) )
thus  ( [x,y] in R implies y in Im (R,x) ) ::_thesis: ( y in Im (R,x) implies [x,y] in R )
proof
 x in {x} by TARSKI:def_1;
hence  ( [x,y] in R implies y in Im (R,x) ) by Def13; ::_thesis: verum
end;
assume  y in Im (R,x) ; ::_thesis: [x,y] in R
then  ex z being set st
( [z,y] in R & z in {x} ) by Def13;
hence  [x,y] in R by TARSKI:def_1; ::_thesis: verum
end;

theorem :: RELAT_1:170
for x being set
for R being Relation holds
( x in dom R iff Im (R,x) <> {} )
proof
let x be set ; ::_thesis: for R being Relation holds
( x in dom R iff Im (R,x) <> {} )
let R be Relation; ::_thesis: ( x in dom R iff Im (R,x) <> {} )
thus  ( x in dom R implies Im (R,x) <> {} ) ::_thesis: ( Im (R,x) <> {} implies x in dom R )
proof
assume  x in dom R ; ::_thesis: Im (R,x) <> {}
then  ex y being set st [x,y] in R by XTUPLE_0:def_12;
hence  Im (R,x) <> {} by Th169; ::_thesis: verum
end;
assume  Im (R,x) <> {} ; ::_thesis: x in dom R
then consider y being set  such that
A1: y in Im (R,x) by XBOOLE_0:def_1;
 [x,y] in R by A1, Th169;
hence  x in dom R by XTUPLE_0:def_12; ::_thesis: verum
end;

theorem :: RELAT_1:171
for X, Y being set holds
( {} is X -defined & {} is Y -valued ) by Lm1;

registration
cluster empty Relation-like  ->  non-empty for set ;
coherence
 for b1 being Relation st b1 is empty holds
b1 is non-empty
proof
let R be Relation; ::_thesis: ( R is empty implies R is non-empty )
assume  R is empty ; ::_thesis: R is non-empty
hence  not {} in rng R ; :: according to RELAT_1:def_9 ::_thesis: verum
end;
end;

registration
let X be set ;
let R be X -defined Relation;
cluster  -> X -defined for Element of bool R;
coherence
 for b1 being Subset of R holds b1 is X -defined
proof
let S be Subset of R; ::_thesis: S is X -defined
A1: dom R c= X by Def18;
 dom S c= dom R by Th11;
hence  dom S c= X by A1, XBOOLE_1:1; :: according to RELAT_1:def_18 ::_thesis: verum
end;
end;

registration
let X be set ;
let R be X -valued Relation;
cluster  -> X -valued for Element of bool R;
coherence
 for b1 being Subset of R holds b1 is X -valued
proof
let S be Subset of R; ::_thesis: S is X -valued
A1: rng R c= X by Def19;
 rng S c= rng R by Th11;
hence  rng S c= X by A1, XBOOLE_1:1; :: according to RELAT_1:def_19 ::_thesis: verum
end;
end;

theorem :: RELAT_1:172
for X, Y being set
for R being Relation st X misses Y holds
(R | X) | Y = {}
proof
let X, Y be set ; ::_thesis: for R being Relation st X misses Y holds
(R | X) | Y = {}
let R be Relation; ::_thesis: ( X misses Y implies (R | X) | Y = {} )
assume  X misses Y ; ::_thesis: (R | X) | Y = {}
then  X /\ Y = {} by XBOOLE_0:def_7;
hence (R | X) | Y = R | {} by Th71
.= {} ;
::_thesis: verum
end;

theorem :: RELAT_1:173
for x being set holds field {[x,x]} = {x}
proof
let x be set ; ::_thesis: field {[x,x]} = {x}
thus  field {[x,x]} = {x,x} by Th17
.= {x} by ENUMSET1:29 ; ::_thesis: verum
end;

registration
let X be set ;
let R be X -defined Relation;
reduceR | X to R;
reducibility
 R | X = R
proof
 dom R c= X by Def18;
hence  R | X = R by Th68; ::_thesis: verum
end;
end;

registration
let Y be set ;
let R be Y -valued Relation;
reduceY |` R to R;
reducibility
 Y |` R = R
proof
 rng R c= Y by Def19;
hence  Y |` R = R by Th94; ::_thesis: verum
end;
end;

theorem :: RELAT_1:174
for X being set
for R being b1 -defined Relation holds R = R | X ;

theorem :: RELAT_1:175
for X being set
for S being Relation
for R being b1 -defined Relation st R c= S holds
R c= S | X
proof
let X be set ; ::_thesis: for S being Relation
for R being X -defined Relation st R c= S holds
R c= S | X
let S be Relation; ::_thesis: for R being X -defined Relation st R c= S holds
R c= S | X
let R be X -defined Relation; ::_thesis: ( R c= S implies R c= S | X )
 R = R | X ;
hence  ( R c= S implies R c= S | X ) by Th76; ::_thesis: verum
end;

theorem Th176: :: RELAT_1:176
for X, A being set
for R being Relation st dom R c= X holds
R \ (R | A) = R | (X \ A)
proof
let X, A be set ; ::_thesis: for R being Relation st dom R c= X holds
R \ (R | A) = R | (X \ A)
let R be Relation; ::_thesis: ( dom R c= X implies R \ (R | A) = R | (X \ A) )
assume  dom R c= X ; ::_thesis: R \ (R | A) = R | (X \ A)
hence R \ (R | A) = (R | X) \ (R | A) by Th68
.= R | (X \ A) by Th80 ;
::_thesis: verum
end;

theorem Th177: :: RELAT_1:177
for A being set
for R being Relation holds dom (R \ (R | A)) = (dom R) \ A
proof
let A be set ; ::_thesis: for R being Relation holds dom (R \ (R | A)) = (dom R) \ A
let R be Relation; ::_thesis: dom (R \ (R | A)) = (dom R) \ A
 R \ (R | A) = R | ((dom R) \ A) by Th176;
hence  dom (R \ (R | A)) = (dom R) /\ ((dom R) \ A) by Th61
.= ((dom R) /\ (dom R)) \ A by XBOOLE_1:49
.= (dom R) \ A ;
::_thesis: verum
end;

theorem :: RELAT_1:178
for A being set
for R being Relation holds (dom R) \ (dom (R | A)) = dom (R \ (R | A))
proof
let A be set ; ::_thesis: for R being Relation holds (dom R) \ (dom (R | A)) = dom (R \ (R | A))
let R be Relation; ::_thesis: (dom R) \ (dom (R | A)) = dom (R \ (R | A))
thus (dom R) \ (dom (R | A)) = (dom R) \ (A /\ (dom R)) by Th61
.= (dom R) \ A by XBOOLE_1:47
.= dom (R \ (R | A)) by Th177 ; ::_thesis: verum
end;

theorem :: RELAT_1:179
for R, S being Relation st dom R misses dom S holds
R misses S
proof
let R, S be Relation; ::_thesis: ( dom R misses dom S implies R misses S )
assume A1: dom R misses dom S ; ::_thesis: R misses S
assume  R meets S ; ::_thesis: contradiction
then consider x being set  such that
A2: x in R and
A3: x in S by XBOOLE_0:3;
consider y, z being set  such that
A4: x = [y,z] by A2, Def1;
 ( y in dom R & y in dom S ) by A2, A3, A4, XTUPLE_0:def_12;
hence  contradiction by A1, XBOOLE_0:3; ::_thesis: verum
end;

theorem :: RELAT_1:180
for R, S being Relation st rng R misses rng S holds
R misses S
proof
let R, S be Relation; ::_thesis: ( rng R misses rng S implies R misses S )
assume A1: rng R misses rng S ; ::_thesis: R misses S
assume  R meets S ; ::_thesis: contradiction
then consider x being set  such that
A2: x in R and
A3: x in S by XBOOLE_0:3;
consider y, z being set  such that
A4: x = [y,z] by A2, Def1;
 ( z in rng R & z in rng S ) by A2, A3, A4, XTUPLE_0:def_13;
hence  contradiction by A1, XBOOLE_0:3; ::_thesis: verum
end;

theorem :: RELAT_1:181
for X, Y being set
for R being Relation st X c= Y holds
(R \ (R | Y)) | X = {}
proof
let X, Y be set ; ::_thesis: for R being Relation st X c= Y holds
(R \ (R | Y)) | X = {}
let R be Relation; ::_thesis: ( X c= Y implies (R \ (R | Y)) | X = {} )
assume A1: X c= Y ; ::_thesis: (R \ (R | Y)) | X = {}
 (dom R) /\ X c= X by XBOOLE_1:17;
then A2: (dom R) /\ X c= Y by A1, XBOOLE_1:1;
 dom (R \ (R | Y)) = (dom R) \ Y by Th177;
then  dom ((R \ (R | Y)) | X) = ((dom R) \ Y) /\ X by Th61
.= ((dom R) /\ X) \ Y by XBOOLE_1:49
.= {} by A2, XBOOLE_1:37 ;
hence  (R \ (R | Y)) | X = {} ; ::_thesis: verum
end;

theorem :: RELAT_1:182
for X, Y being set st X c= Y holds
for R being b1 -defined Relation holds R is Y -defined
proof
let X, Y be set ; ::_thesis: ( X c= Y implies for R being X -defined Relation holds R is Y -defined )
assume A1: X c= Y ; ::_thesis: for R being X -defined Relation holds R is Y -defined
let R be X -defined Relation; ::_thesis: R is Y -defined
 dom R c= X by Def18;
hence  dom R c= Y by A1, XBOOLE_1:1; :: according to RELAT_1:def_18 ::_thesis: verum
end;

theorem :: RELAT_1:183
for X, Y being set st X c= Y holds
for R being b1 -valued Relation holds R is Y -valued
proof
let X, Y be set ; ::_thesis: ( X c= Y implies for R being X -valued Relation holds R is Y -valued )
assume A1: X c= Y ; ::_thesis: for R being X -valued Relation holds R is Y -valued
let R be X -valued Relation; ::_thesis: R is Y -valued
 rng R c= X by Def19;
hence  rng R c= Y by A1, XBOOLE_1:1; :: according to RELAT_1:def_19 ::_thesis: verum
end;

theorem :: RELAT_1:184
for R, S being Relation holds
( R c= S iff R c= S | (dom R) )
proof
let R, S be Relation; ::_thesis: ( R c= S iff R c= S | (dom R) )
thus  ( R c= S implies R c= S | (dom R) ) ::_thesis: ( R c= S | (dom R) implies R c= S )
proof
assume  R c= S ; ::_thesis: R c= S | (dom R)
then  R | (dom R) c= S | (dom R) by Th76;
hence  R c= S | (dom R) ; ::_thesis: verum
end;
 S | (dom R) c= S by Th59;
hence  ( R c= S | (dom R) implies R c= S ) by XBOOLE_1:1; ::_thesis: verum
end;

theorem :: RELAT_1:185
for X, Y being set
for R being b1 -defined b2 -valued Relation holds R c= [:X,Y:]
proof
let X, Y be set ; ::_thesis: for R being X -defined Y -valued Relation holds R c= [:X,Y:]
let R be X -defined Y -valued Relation; ::_thesis: R c= [:X,Y:]
A1: R c= [:(dom R),(rng R):] by Th7;
 ( dom R c= X & rng R c= Y ) by Def18, Def19;
then  [:(dom R),(rng R):] c= [:X,Y:] by ZFMISC_1:96;
hence  R c= [:X,Y:] by A1, XBOOLE_1:1; ::_thesis: verum
end;

theorem Th186: :: RELAT_1:186
for X being set
for R being Relation holds dom (X |` R) c= dom R
proof
let X be set ; ::_thesis: for R being Relation holds dom (X |` R) c= dom R
let R be Relation; ::_thesis: dom (X |` R) c= dom R
 X |` R c= R by Th86;
hence  dom (X |` R) c= dom R by Th11; ::_thesis: verum
end;

registration
let A, X be set ;
let R be A -defined Relation;
clusterX |` R -> A -defined ;
coherence
 X |` R is A -defined
proof
 ( dom (X |` R) c= dom R & dom R c= A ) by Def18, Th186;
hence  dom (X |` R) c= A by XBOOLE_1:1; :: according to RELAT_1:def_18 ::_thesis: verum
end;
end;

registration
let X, A be set ;
let R be A -valued Relation;
clusterX |` R -> X -valued A -valued ;
coherence
 ( X |` R is A -valued & X |` R is X -valued )
proof
 ( rng (X |` R) c= rng R & rng R c= A ) by Def19, Th87;
hence  rng (X |` R) c= A by XBOOLE_1:1; :: according to RELAT_1:def_19 ::_thesis: X |` R is X -valued
thus  rng (X |` R) c= X by Th85; :: according to RELAT_1:def_19 ::_thesis: verum
end;
end;

registration
let X be empty set ;
cluster Relation-like X -defined  ->  empty X -defined for set ;
coherence
 for b1 being X -defined Relation holds b1 is empty
proof
let R be X -defined Relation; ::_thesis: R is empty
 dom R c= X by Def18;
hence  R is empty by XBOOLE_1:3; ::_thesis: verum
end;
cluster Relation-like X -valued  ->  empty X -valued for set ;
coherence
 for b1 being X -valued Relation holds b1 is empty
proof
let R be X -valued Relation; ::_thesis: R is empty
 rng R c= X by Def19;
hence  R is empty by XBOOLE_1:3; ::_thesis: verum
end;
end;