relat_1.miz



    begin

    reserve A,X,X1,X2,Y,Y1,Y2 for set,

a,b,c,d,x,y,z for object;

    definition

      let IT be set;

      :: RELAT_1:def1

      attr IT is Relation-like means

      : Def1: x in IT implies ex y, z st x = [y, z];

    end

    registration

      cluster empty -> Relation-like for set;

      coherence ;

    end

    definition

      mode Relation is Relation-like set;

    end

    reserve P,P1,P2,Q,R,S for Relation;

    registration

      let R be Relation;

      cluster -> Relation-like for Subset of R;

      coherence by Def1;

    end

    scheme :: RELAT_1:sch1

    RelExistence { A,B() -> set , P[ object, object] } :

ex R be Relation st for x, y holds [x, y] in R iff x in A() & y in B() & P[x, y];

      ex R be Relation st for p be object holds p in R iff p in [:A(), B():] & ex x, y st p = [x, y] & P[x, y]

      proof

        defpred Q[ object] means ex x, y st $1 = [x, y] & P[x, y];

        consider B be set such that

         A1: for p be object holds p in B iff p in [:A(), B():] & Q[p] from XBOOLE_0:sch 1;

        for p be object st p in B holds ex x, y st p = [x, y]

        proof

          let p be object;

          assume p in B;

          then ex x, y st p = [x, y] & P[x, y] by A1;

          hence thesis;

        end;

        then B is Relation by Def1;

        hence thesis by A1;

      end;

      then

      consider R be Relation such that

       A2: for p be object holds p in R iff p in [:A(), B():] & ex x, y st p = [x, y] & P[x, y];

      take R;

      let x, y;

      thus [x, y] in R implies x in A() & y in B() & P[x, y]

      proof

        assume

         A3: [x, y] in R;

        then

        consider xx,yy be object such that

         A4: [x, y] = [xx, yy] and

         A5: P[xx, yy] by A2;

        

         A6: [x, y] in [:A(), B():] by A2, A3;

        x = xx by A4, XTUPLE_0: 1;

        hence thesis by A4, A5, A6, XTUPLE_0: 1, ZFMISC_1: 87;

      end;

      thus x in A() & y in B() & P[x, y] implies [x, y] in R

      proof

        assume that

         A7: x in A() & y in B() and

         A8: P[x, y];

         [x, y] in [:A(), B():] by A7, ZFMISC_1: 87;

        hence thesis by A2, A8;

      end;

    end;

    definition

      let P, R;

      :: original: =

      redefine

      :: RELAT_1:def2

      pred P = R means for a, b holds [a, b] in P iff [a, b] in R;

      compatibility

      proof

        thus P = R implies for a, b holds [a, b] in P iff [a, b] in R;

        assume

         A1: for a, b holds [a, b] in P iff [a, b] in R;

        thus P c= R

        proof

          let x be object;

          assume

           A2: x in P;

          then ex y, z st x = [y, z] by Def1;

          hence x in R by A1, A2;

        end;

        let x be object;

        assume

         A3: x in R;

        then ex y, z st x = [y, z] by Def1;

        hence x in P by A1, A3;

      end;

    end

    registration

      let P, X;

      cluster (P /\ X) -> Relation-like;

      coherence

      proof

        (P /\ X) c= P by XBOOLE_1: 17;

        hence thesis;

      end;

      cluster (P \ X) -> Relation-like;

      coherence ;

    end

    registration

      let P, R;

      cluster (P \/ R) -> Relation-like;

      coherence

      proof

        let x;

        

         A1: x in R implies ex y, z st x = [y, z] by Def1;

        x in P implies ex y, z st x = [y, z] by Def1;

        hence x in (P \/ R) implies ex y, z st x = [y, z] by A1, XBOOLE_0:def 3;

      end;

    end

    registration

      let R,S be Relation;

      cluster (R \+\ S) -> Relation-like;

      coherence ;

    end

    registration

      let a,b be object;

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

      coherence

      proof

        let x;

        assume x in { [a, b]};

        then x = [a, b] by TARSKI:def 1;

        hence thesis;

      end;

    end

    registration

      let a,b be set;

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

      coherence

      proof

        let z;

        assume z in [:a, b:];

        then ex x,y be object st x in a & y in b & [x, y] = z by ZFMISC_1:def 2;

        hence thesis;

      end;

    end

    registration

      let a,b,c,d be object;

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

      coherence

      proof

         { [a, b], [c, d]} = ( { [a, b]} \/ { [c, d]}) by ENUMSET1: 1;

        hence thesis;

      end;

    end

    definition

      let P, A;

      :: original: c=

      redefine

      :: RELAT_1:def3

      pred P c= A means for a, b holds [a, b] in P implies [a, b] in A;

      compatibility

      proof

        thus P c= A implies for a, b holds [a, b] in P implies [a, b] in A;

        assume

         A1: for a, b holds [a, b] in P implies [a, b] in A;

        let x be object;

        assume

         A2: x in P;

        then ex y, z st x = [y, z] by Def1;

        hence thesis by A1, A2;

      end;

    end

    notation

      let R be Relation;

      synonym dom R for proj1 R;

    end

    notation

      let R be Relation;

      synonym rng R for proj2 R;

    end

    ::$Canceled

    theorem :: RELAT_1:7

    

     Th1: R c= [:( dom R), ( rng R):]

    proof

      let y, z;

      assume [y, z] in R;

      then y in ( dom R) & z in ( rng R) by XTUPLE_0:def 12, XTUPLE_0:def 13;

      hence thesis by ZFMISC_1: 87;

    end;

    theorem :: RELAT_1:8

    (R /\ [:( dom R), ( rng R):]) = R by Th1, XBOOLE_1: 28;

    theorem :: RELAT_1:9

    

     Th3: ( dom { [x, y]}) = {x} & ( rng { [x, y]}) = {y}

    proof

      set R = { [x, y]};

      for z be object holds z in ( dom R) iff z in {x}

      proof

        let z be object;

        thus z in ( dom R) implies z in {x}

        proof

          assume z in ( dom R);

          then

          consider b be object such that

           A2: [z, b] in R by XTUPLE_0:def 12;

           [z, b] = [x, y] by A2, TARSKI:def 1;

          then z = x by XTUPLE_0: 1;

          hence thesis by TARSKI:def 1;

        end;

        assume z in {x};

        then z = x by TARSKI:def 1;

        then [z, y] in R by TARSKI:def 1;

        hence thesis by XTUPLE_0:def 12;

      end;

      hence ( dom R) = {x} by TARSKI: 2;

      for z be object holds z in ( rng R) iff z in {y}

      proof

        let z be object;

        thus z in ( rng R) implies z in {y}

        proof

          assume z in ( rng R);

          then

          consider a be object such that

           A3: [a, z] in R by XTUPLE_0:def 13;

           [a, z] = [x, y] by A3, TARSKI:def 1;

          then z = y by XTUPLE_0: 1;

          hence thesis by TARSKI:def 1;

        end;

        assume z in {y};

        then z = y by TARSKI:def 1;

        then [x, z] in R by TARSKI:def 1;

        hence thesis by XTUPLE_0:def 13;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: RELAT_1:10

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

    proof

      set R = { [a, b], [x, y]};

      thus ( dom R) = {a, x}

      proof

        thus ( dom R) c= {a, x}

        proof

          let z be object;

          assume z in ( dom R);

          then

          consider c be object such that

           A2: [z, c] in R by XTUPLE_0:def 12;

           [z, c] = [a, b] or [z, c] = [x, y] by A2, TARSKI:def 2;

          then z = a or z = x by XTUPLE_0: 1;

          hence thesis by TARSKI:def 2;

        end;

        let z be object;

        assume z in {a, x};

        then z = a or z = x by TARSKI:def 2;

        then [z, b] in R or [z, y] in R by TARSKI:def 2;

        hence thesis by XTUPLE_0:def 12;

      end;

      thus ( rng R) c= {b, y}

      proof

        let z be object;

        assume z in ( rng R);

        then

        consider d be object such that

         A3: [d, z] in R by XTUPLE_0:def 13;

         [d, z] = [a, b] or [d, z] = [x, y] by A3, TARSKI:def 2;

        then z = b or z = y by XTUPLE_0: 1;

        hence thesis by TARSKI:def 2;

      end;

      let z be object;

      assume z in {b, y};

      then z = b or z = y by TARSKI:def 2;

      then [a, z] in R or [x, z] in R by TARSKI:def 2;

      hence thesis by XTUPLE_0:def 13;

    end;

    theorem :: RELAT_1:11

    P c= R implies ( dom P) c= ( dom R) & ( rng P) c= ( rng R) by XTUPLE_0: 8, XTUPLE_0: 9;

    theorem :: RELAT_1:12

    ( rng (P \/ R)) = (( rng P) \/ ( rng R)) by XTUPLE_0: 27;

    theorem :: RELAT_1:13

    ( rng (P /\ R)) c= (( rng P) /\ ( rng R)) by XTUPLE_0: 28;

    theorem :: RELAT_1:14

    (( rng P) \ ( rng R)) c= ( rng (P \ R)) by XTUPLE_0: 29;

    definition

      ::$Canceled

      let R;

      :: RELAT_1:def6

      func field R -> set equals (( dom R) \/ ( rng R));

      coherence ;

    end

    theorem :: RELAT_1:15

     [a, b] in R implies a in ( field R) & b in ( field R)

    proof

      assume

       A1: [a, b] in R;

      then a in ( dom R) by XTUPLE_0:def 12;

      hence a in ( field R) by XBOOLE_0:def 3;

      b in ( rng R) by A1, XTUPLE_0:def 13;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: RELAT_1:16

    P c= R implies ( field P) c= ( field R)

    proof

      assume P c= R;

      then ( dom P) c= ( dom R) & ( rng P) c= ( rng R) by XTUPLE_0: 8, XTUPLE_0: 9;

      hence thesis by XBOOLE_1: 13;

    end;

    theorem :: RELAT_1:17

    

     Th11: ( field { [x, y]}) = {x, y}

    proof

      ( dom { [x, y]}) = {x} & ( rng { [x, y]}) = {y} by Th3;

      hence thesis by ENUMSET1: 1;

    end;

    theorem :: RELAT_1:18

    ( field (P \/ R)) = (( field P) \/ ( field R))

    proof

      

      thus ( field (P \/ R)) = ((( dom P) \/ ( dom R)) \/ ( rng (P \/ R))) by XTUPLE_0: 23

      .= ((( dom P) \/ ( dom R)) \/ (( rng P) \/ ( rng R))) by XTUPLE_0: 27

      .= (((( 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;

    end;

    theorem :: RELAT_1:19

    ( field (P /\ R)) c= (( field P) /\ ( field R))

    proof

      let x be object;

      assume x in ( field (P /\ 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 XTUPLE_0: 24, XTUPLE_0: 28;

      hence thesis by A1, A2, XBOOLE_0:def 4;

    end;

    definition

      let R;

      :: RELAT_1:def7

      func R ~ -> Relation means

      : Def5: [x, y] in it iff [y, x] in R;

      existence

      proof

        defpred Q[ object, object] means [$2, $1] in R;

        consider P such that

         A1: for x, y holds [x, y] in P iff x in ( rng R) & y in ( dom R) & Q[x, y] from RelExistence;

        take P;

        let x, y;

         [y, x] in R implies y in ( dom R) & x in ( rng R) by XTUPLE_0:def 12, XTUPLE_0:def 13;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let P1, P2;

        assume that

         A2: [x, y] in P1 iff [y, x] in R and

         A3: [x, y] in P2 iff [y, x] in R;

        let x, y;

         [x, y] in P1 iff [y, x] in R by A2;

        hence [x, y] in P1 iff [x, y] in P2 by A3;

      end;

      involutiveness ;

    end

    theorem :: RELAT_1:20

    

     Th14: ( rng R) = ( dom (R ~ )) & ( dom R) = ( rng (R ~ ))

    proof

      thus ( rng R) c= ( dom (R ~ ))

      proof

        let u be object;

        assume u in ( rng R);

        then

        consider x be object such that

         A1: [x, u] in R by XTUPLE_0:def 13;

         [u, x] in (R ~ ) by A1, Def5;

        hence thesis by XTUPLE_0:def 12;

      end;

      thus ( dom (R ~ )) c= ( rng R)

      proof

        let u be object;

        assume u in ( dom (R ~ ));

        then

        consider x be object such that

         A2: [u, x] in (R ~ ) by XTUPLE_0:def 12;

         [x, u] in R by A2, Def5;

        hence thesis by XTUPLE_0:def 13;

      end;

      thus ( dom R) c= ( rng (R ~ ))

      proof

        let u be object;

        assume u in ( dom R);

        then

        consider x be object such that

         A3: [u, x] in R by XTUPLE_0:def 12;

         [x, u] in (R ~ ) by A3, Def5;

        hence thesis by XTUPLE_0:def 13;

      end;

      let u be object;

      assume u in ( rng (R ~ ));

      then

      consider x be object such that

       A4: [x, u] in (R ~ ) by XTUPLE_0:def 13;

       [u, x] in R by A4, Def5;

      hence thesis by XTUPLE_0:def 12;

    end;

    theorem :: RELAT_1:21

    ( field R) = ( field (R ~ ))

    proof

      

      thus ( field R) = (( rng (R ~ )) \/ ( rng R)) by Th14

      .= ( field (R ~ )) by Th14;

    end;

    theorem :: RELAT_1:22

    ((P /\ R) ~ ) = ((P ~ ) /\ (R ~ ))

    proof

      let x, y;

       [x, y] in ((P /\ R) ~ ) iff [y, x] in (P /\ R) by Def5;

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

      hence thesis by XBOOLE_0:def 4;

    end;

    theorem :: RELAT_1:23

    ((P \/ R) ~ ) = ((P ~ ) \/ (R ~ ))

    proof

      let x, y;

       [x, y] in ((P \/ R) ~ ) iff [y, x] in (P \/ R) by Def5;

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

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: RELAT_1:24

    ((P \ R) ~ ) = ((P ~ ) \ (R ~ ))

    proof

      let x, y;

       [x, y] in ((P \ R) ~ ) iff [y, x] in (P \ R) by Def5;

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

      hence thesis by XBOOLE_0:def 5;

    end;

    definition

      let P,R be set;

      :: RELAT_1:def8

      func P (#) R -> Relation means

      : Def6: [x, y] in it iff ex z st [x, z] in P & [z, y] in R;

      existence

      proof

        defpred Z[ object, object] means ex z st [$1, z] in P & [z, $2] in R;

        consider Q such that

         A1: for x, y holds [x, y] in Q iff x in ( proj1 P) & y in ( proj2 R) & Z[x, y] from RelExistence;

        take Q;

        let x, y;

        thus [x, y] in Q implies ex z st [x, z] in P & [z, y] in R by A1;

        given z such that

         A2: [x, z] in P & [z, y] in R;

        x in ( proj1 P) & y in ( proj2 R) by A2, XTUPLE_0:def 12, XTUPLE_0:def 13;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let P1, P2;

        assume that

         A3: [x, y] in P1 iff ex z st [x, z] in P & [z, y] in R and

         A4: [x, y] in P2 iff ex z st [x, z] in P & [z, y] in R;

        let x, y;

         [x, y] in P1 iff ex z st [x, z] in P & [z, y] in R by A3;

        hence [x, y] in P1 iff [x, y] in P2 by A4;

      end;

    end

    notation

      let P, R;

      synonym P * R for P (#) R;

    end

    theorem :: RELAT_1:25

    

     Th19: ( dom (P * R)) c= ( dom P)

    proof

      let x be object;

      assume x in ( dom (P * R));

      then

      consider y be object such that

       A1: [x, y] in (P * R) by XTUPLE_0:def 12;

      ex z st [x, z] in P & [z, y] in R by A1, Def6;

      hence thesis by XTUPLE_0:def 12;

    end;

    theorem :: RELAT_1:26

    

     Th20: ( rng (P * R)) c= ( rng R)

    proof

      let y be object;

      assume y in ( rng (P * R));

      then

      consider x be object such that

       A1: [x, y] in (P * R) by XTUPLE_0:def 13;

      ex z st [x, z] in P & [z, y] in R by A1, Def6;

      hence thesis by XTUPLE_0:def 13;

    end;

    theorem :: RELAT_1:27

    ( rng R) c= ( dom P) implies ( dom (R * P)) = ( dom R)

    proof

      assume

       A1: for y be object holds y in ( rng R) implies y in ( dom P);

      thus ( dom (R * P)) c= ( dom R) by Th19;

      let x be object;

      assume x in ( dom R);

      then

      consider y be object 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 be object such that

       A3: [y, z] in P by XTUPLE_0:def 12;

       [x, z] in (R * P) by A2, A3, Def6;

      hence thesis by XTUPLE_0:def 12;

    end;

    theorem :: RELAT_1:28

    ( dom P) c= ( rng R) implies ( rng (R * P)) = ( rng P)

    proof

      assume

       A1: for y be object st y in ( dom P) holds y in ( rng R);

      thus ( rng (R * P)) c= ( rng P) by Th20;

      let z be object;

      assume z in ( rng P);

      then

      consider y be object 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 be object such that

       A3: [x, y] in R by XTUPLE_0:def 13;

       [x, z] in (R * P) by A2, A3, Def6;

      hence thesis by XTUPLE_0:def 13;

    end;

    theorem :: RELAT_1:29

    

     Th23: P c= R implies (Q * P) c= (Q * R)

    proof

      assume

       A1: P c= R;

      let x, y;

      assume [x, y] in (Q * P);

      then ex z st [x, z] in Q & [z, y] in P by Def6;

      hence thesis by A1, Def6;

    end;

    theorem :: RELAT_1:30

    

     Th24: P c= Q implies (P * R) c= (Q * R)

    proof

      assume

       A1: P c= Q;

      let x, y;

      assume [x, y] in (P * R);

      then ex z st [x, z] in P & [z, y] in R by Def6;

      hence thesis by A1, Def6;

    end;

    theorem :: RELAT_1:31

    P c= R & Q c= S implies (P * Q) c= (R * S)

    proof

      assume

       A1: P c= R & Q c= S;

      let x, y;

      assume [x, y] in (P * Q);

      then ex z st [x, z] in P & [z, y] in Q by Def6;

      hence [x, y] in (R * S) by A1, Def6;

    end;

    theorem :: RELAT_1:32

    (P * (R \/ Q)) = ((P * R) \/ (P * Q))

    proof

      let x, y;

      hereby

        assume [x, y] in (P * (R \/ Q));

        then

        consider z such that

         A1: [x, z] in P and

         A2: [z, y] in (R \/ Q) by Def6;

         [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, Def6;

        hence [x, y] in ((P * R) \/ (P * Q)) by XBOOLE_0:def 3;

      end;

      assume

       A3: [x, y] in ((P * R) \/ (P * Q));

      per cases by A3, XBOOLE_0:def 3;

        suppose [x, y] in (P * Q);

        then

        consider z such that

         A4: [x, z] in P and

         A5: [z, y] in Q by Def6;

         [z, y] in (R \/ Q) by A5, XBOOLE_0:def 3;

        hence [x, y] in (P * (R \/ Q)) by A4, Def6;

      end;

        suppose [x, y] in (P * R);

        then

        consider z such that

         A6: [x, z] in P and

         A7: [z, y] in R by Def6;

         [z, y] in (R \/ Q) by A7, XBOOLE_0:def 3;

        hence [x, y] in (P * (R \/ Q)) by A6, Def6;

      end;

    end;

    theorem :: RELAT_1:33

    (P * (R /\ Q)) c= ((P * R) /\ (P * Q))

    proof

      let x, y;

      assume [x, y] in (P * (R /\ Q));

      then

      consider z such that

       A1: [x, z] in P and

       A2: [z, y] in (R /\ Q) by Def6;

       [z, y] in Q by A2, XBOOLE_0:def 4;

      then

       A3: [x, y] in (P * Q) by A1, Def6;

       [z, y] in R by A2, XBOOLE_0:def 4;

      then [x, y] in (P * R) by A1, Def6;

      hence [x, y] in ((P * R) /\ (P * Q)) by A3, XBOOLE_0:def 4;

    end;

    theorem :: RELAT_1:34

    ((P * R) \ (P * Q)) c= (P * (R \ Q))

    proof

      let a, b;

      assume

       A1: [a, b] in ((P * R) \ (P * Q));

      then

      consider y such that

       A2: [a, y] in P and

       A3: [y, b] in R by Def6;

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

      then [y, b] in (R \ Q) by A2, A3, XBOOLE_0:def 5;

      hence [a, b] in (P * (R \ Q)) by A2, Def6;

    end;

    theorem :: RELAT_1:35

    ((P * R) ~ ) = ((R ~ ) * (P ~ ))

    proof

      let a, b;

      hereby

        assume [a, b] in ((P * R) ~ );

        then [b, a] in (P * R) by Def5;

        then

        consider y such that

         A1: [b, y] in P & [y, a] in R by Def6;

         [y, b] in (P ~ ) & [a, y] in (R ~ ) by A1, Def5;

        hence [a, b] in ((R ~ ) * (P ~ )) by Def6;

      end;

      assume [a, b] in ((R ~ ) * (P ~ ));

      then

      consider y such that

       A2: [a, y] in (R ~ ) & [y, b] in (P ~ ) by Def6;

       [y, a] in R & [b, y] in P by A2, Def5;

      then [b, a] in (P * R) by Def6;

      hence [a, b] in ((P * R) ~ ) by Def5;

    end;

    theorem :: RELAT_1:36

    

     Th30: ((P * R) * Q) = (P * (R * Q))

    proof

      let a, b;

      hereby

        assume [a, b] in ((P * R) * Q);

        then

        consider y such that

         A1: [a, y] in (P * R) and

         A2: [y, b] in Q by Def6;

        consider x such that

         A3: [a, x] in P and

         A4: [x, y] in R by A1, Def6;

         [x, b] in (R * Q) by A2, A4, Def6;

        hence [a, b] in (P * (R * Q)) by A3, Def6;

      end;

      assume [a, b] in (P * (R * Q));

      then

      consider y such that

       A5: [a, y] in P and

       A6: [y, b] in (R * Q) by Def6;

      consider x such that

       A7: [y, x] in R and

       A8: [x, b] in Q by A6, Def6;

       [a, x] in (P * R) by A5, A7, Def6;

      hence [a, b] in ((P * R) * Q) by A8, Def6;

    end;

    registration

      cluster non empty for Relation;

      existence

      proof

         { [ {} , {} ]} is non empty;

        hence thesis;

      end;

    end

    registration

      let f be non empty Relation;

      cluster ( dom f) -> non empty;

      coherence

      proof

        ex x1,x2 be object st the Element of f = [x1, x2] by Def1;

        hence thesis by XTUPLE_0:def 12;

      end;

      cluster ( rng f) -> non empty;

      coherence

      proof

        ex x1,x2 be object st the Element of f = [x1, x2] by Def1;

        hence thesis by XTUPLE_0:def 13;

      end;

    end

    theorem :: RELAT_1:37

    

     Th31: (for x, y holds not [x, y] in R) implies R = {} ;

    theorem :: RELAT_1:38

    

     Th32: ( dom {} ) = {} & ( rng {} ) = {} ;

    theorem :: RELAT_1:39

    

     Th33: ( {} * R) = {} & (R * {} ) = {}

    proof

      thus ( {} * R) = {}

      proof

        let x, y;

        hereby

          assume [x, y] in ( {} * R);

          then ex z st [x, z] in {} & [z, y] in R by Def6;

          hence [x, y] in {} ;

        end;

        thus thesis;

      end;

      let x, y;

      hereby

        assume [x, y] in (R * {} );

        then ex z st [x, z] in R & [z, y] in {} by Def6;

        hence [x, y] in {} ;

      end;

      thus thesis;

    end;

    registration

      let X be empty set;

      cluster ( dom X) -> empty;

      coherence ;

      cluster ( rng X) -> empty;

      coherence ;

      let R;

      cluster (X * R) -> empty;

      coherence by Th33;

      cluster (R * X) -> empty;

      coherence by Th33;

    end

    theorem :: RELAT_1:40

    ( field {} ) = {} ;

    theorem :: RELAT_1:41

    

     Th35: ( dom R) = {} or ( rng R) = {} implies R = {} ;

    theorem :: RELAT_1:42

    ( dom R) = {} iff ( rng R) = {} by Th32, Th35;

    registration

      let X be empty set;

      cluster (X ~ ) -> empty;

      coherence

      proof

        for x, y st [x, y] in ( {} ~ ) holds contradiction by Def5;

        hence thesis by Th31;

      end;

    end

    theorem :: RELAT_1:43

    ( {} ~ ) = {} ;

    theorem :: RELAT_1:44

    ( rng R) misses ( dom P) implies (R * P) = {}

    proof

      assume

       A1: (( rng R) /\ ( dom P)) = {} ;

      assume (R * P) <> {} ;

      then

      consider x, z such that

       A2: [x, z] in (R * P);

      consider y such that

       A3: [x, y] in R & [y, z] in P by A2, Def6;

      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;

    end;

    definition

      let R be Relation;

      :: RELAT_1:def9

      attr R is non-empty means

      : Def7: not {} in ( rng R);

    end

    registration

      cluster non-empty for Relation;

      existence

      proof

        take {} ;

        thus not {} in ( rng {} );

      end;

    end

    registration

      let R be Relation, S be non-empty Relation;

      cluster (R * S) -> non-empty;

      coherence

      proof

        ( rng (R * S)) c= ( rng S) by Th20;

        hence not {} in ( rng (R * S)) by Def7;

      end;

    end

    definition

      let X;

      :: RELAT_1:def10

      func id X -> Relation means

      : Def8: [x, y] in it iff x in X & x = y;

      existence

      proof

        defpred Z[ object, object] means $1 = $2;

        consider R such that

         A1: for x, y holds [x, y] in R iff x in X & y in X & Z[x, y] from RelExistence;

        take R;

        let x, y;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let P1, P2;

        assume that

         A2: [x, y] in P1 iff x in X & x = y and

         A3: [x, y] in P2 iff x in X & x = y;

        let x, y;

         [x, y] in P1 iff x in X & x = y by A2;

        hence [x, y] in P1 iff [x, y] in P2 by A3;

      end;

    end

    registration

      let X;

      reduce ( dom ( id X)) to X;

      reducibility

      proof

        thus ( dom ( id X)) c= X

        proof

          let x be object;

          assume x in ( dom ( id X));

          then ex y be object st [x, y] in ( id X) by XTUPLE_0:def 12;

          hence x in X by Def8;

        end;

        let x be object;

        assume x in X;

        then [x, x] in ( id X) by Def8;

        hence x in ( dom ( id X)) by XTUPLE_0:def 12;

      end;

      reduce ( rng ( id X)) to X;

      reducibility

      proof

        thus ( rng ( id X)) c= X

        proof

          let x be object;

          assume x in ( rng ( id X));

          then

          consider y be object such that

           A1: [y, x] in ( id X) by XTUPLE_0:def 13;

          x = y by A1, Def8;

          hence thesis by A1, Def8;

        end;

        let x be object;

         [x, x] in ( id X) iff x in X by Def8;

        hence thesis by XTUPLE_0:def 13;

      end;

    end

    theorem :: RELAT_1:45

    ( dom ( id X)) = X & ( rng ( id X)) = X;

    registration

      let X;

      reduce (( id X) ~ ) to ( id X);

      reducibility

      proof

        let x, y;

        thus [x, y] in (( id X) ~ ) implies [x, y] in ( id X)

        proof

          assume [x, y] in (( id X) ~ );

          then [y, x] in ( id X) by Def5;

          hence thesis by Def8;

        end;

        assume

         A1: [x, y] in ( id X);

        then x = y by Def8;

        hence thesis by A1, Def5;

      end;

    end

    theorem :: RELAT_1:46

    (( id X) ~ ) = ( id X);

    theorem :: RELAT_1:47

    (for x st x in X holds [x, x] in R) implies ( id X) c= R

    proof

      assume

       A1: for x st x in X holds [x, x] in R;

      let x, y;

      assume [x, y] in ( id X);

      then x in X & x = y by Def8;

      hence thesis by A1;

    end;

    theorem :: RELAT_1:48

    

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

    proof

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

      proof

        assume [x, y] in (( id X) * R);

        then ex z st [x, z] in ( id X) & [z, y] in R by Def6;

        hence thesis by Def8;

      end;

      assume x in X;

      then [x, x] in ( id X) by Def8;

      hence thesis by Def6;

    end;

    theorem :: RELAT_1:49

    

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

    proof

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

      proof

        assume [x, y] in (R * ( id Y));

        then

        consider z such that

         A1: [x, z] in R and

         A2: [z, y] in ( id Y) by Def6;

        z = y by A2, Def8;

        hence thesis by A1, A2, Def8;

      end;

      y in Y implies [y, y] in ( id Y) by Def8;

      hence thesis by Def6;

    end;

    theorem :: RELAT_1:50

    

     Th44: (R * ( id X)) c= R & (( id X) * R) c= R

    proof

      thus [x, y] in (R * ( id X)) implies [x, y] in R

      proof

        assume [x, y] in (R * ( id X));

        then ex z st [x, z] in R & [z, y] in ( id X) by Def6;

        hence thesis by Def8;

      end;

      thus [x, y] in (( id X) * R) implies [x, y] in R

      proof

        assume [x, y] in (( id X) * R);

        then ex z st [x, z] in ( id X) & [z, y] in R by Def6;

        hence thesis by Def8;

      end;

    end;

    theorem :: RELAT_1:51

    

     Th45: ( dom R) c= X implies (( id X) * R) = R

    proof

      assume

       A1: ( dom R) c= X;

      R c= (( id X) * R)

      proof

        let x, y;

        assume

         A2: [x, y] in R;

        then x in ( dom R) by XTUPLE_0:def 12;

        then [x, x] in ( id X) by A1, Def8;

        hence thesis by A2, Def6;

      end;

      hence thesis by Th44;

    end;

    theorem :: RELAT_1:52

    (( id ( dom R)) * R) = R by Th45;

    theorem :: RELAT_1:53

    

     Th47: ( rng R) c= Y implies (R * ( id Y)) = R

    proof

      assume

       A1: ( rng R) c= Y;

      R c= (R * ( id Y))

      proof

        let x, y;

        assume

         A2: [x, y] in R;

        then y in ( rng R) by XTUPLE_0:def 13;

        then [y, y] in ( id Y) by A1, Def8;

        hence thesis by A2, Def6;

      end;

      hence thesis by Th44;

    end;

    theorem :: RELAT_1:54

    (R * ( id ( rng R))) = R by Th47;

    theorem :: RELAT_1:55

    ( id {} ) = {}

    proof

      ( dom ( id {} )) = {} ;

      hence thesis;

    end;

    theorem :: RELAT_1:56

    ( rng P2) c= X & (P2 * R) = ( id ( dom P1)) & (R * P1) = ( id X) implies P1 = P2

    proof

      ((P2 * R) * P1) = (P2 * (R * P1)) & (( id ( dom P1)) * P1) = P1 by Th30, Th45;

      hence thesis by Th47;

    end;

    definition

      let R, X;

      :: RELAT_1:def11

      func R | X -> Relation means

      : Def9: [x, y] in it iff x in X & [x, y] in R;

      existence

      proof

        defpred Z[ object, object] means ($1 in X & [$1, $2] in R);

        consider P such that

         A1: for x, y holds [x, y] in P iff x in ( dom R) & y in ( rng R) & Z[x, y] from RelExistence;

        take P;

        let x, y;

        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 thesis by A1;

      end;

      uniqueness

      proof

        let P1, P2;

        assume that

         A2: [x, y] in P1 iff x in X & [x, y] in R and

         A3: [x, y] in P2 iff x in X & [x, y] in R;

        let x, y;

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

      end;

    end

    registration

      let R be Relation, X be empty set;

      cluster (R | X) -> empty;

      coherence

      proof

         not [x, y] in (R | {} ) by Def9;

        hence thesis by Th31;

      end;

    end

    theorem :: RELAT_1:57

    

     Th51: x in ( dom (R | X)) iff x in X & x in ( dom R)

    proof

      thus x in ( dom (R | X)) implies x in X & x in ( dom R)

      proof

        assume x in ( dom (R | X));

        then

        consider y be object such that

         A1: [x, y] in (R | X) by XTUPLE_0:def 12;

         [x, y] in R by A1, Def9;

        hence thesis by A1, Def9, XTUPLE_0:def 12;

      end;

      assume

       A2: x in X;

      assume x in ( dom R);

      then

      consider y be object such that

       A3: [x, y] in R by XTUPLE_0:def 12;

       [x, y] in (R | X) by A2, A3, Def9;

      hence thesis by XTUPLE_0:def 12;

    end;

    theorem :: RELAT_1:58

    ( dom (R | X)) c= X by Th51;

    theorem :: RELAT_1:59

    

     Th53: (R | X) c= R by Def9;

    theorem :: RELAT_1:60

    ( dom (R | X)) c= ( dom R) by Th51;

    theorem :: RELAT_1:61

    

     Th55: ( dom (R | X)) = (( dom R) /\ X)

    proof

      for x be object holds x in ( dom (R | X)) iff x in (( dom R) /\ X)

      proof

        let x be object;

        x in ( dom (R | X)) iff x in ( dom R) & x in X by Th51;

        hence thesis by XBOOLE_0:def 4;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: RELAT_1:62

    X c= ( dom R) implies ( dom (R | X)) = X

    proof

      ( dom (R | X)) = (( dom R) /\ X) by Th55;

      hence thesis by XBOOLE_1: 28;

    end;

    theorem :: RELAT_1:63

    ((R | X) * P) c= (R * P) by Th24, Th53;

    theorem :: RELAT_1:64

    (P * (R | X)) c= (P * R) by Th23, Th53;

    theorem :: RELAT_1:65

    (R | X) = (( id X) * R)

    proof

      let x, y;

       [x, y] in (R | X) iff [x, y] in R & x in X by Def9;

      hence thesis by Th42;

    end;

    theorem :: RELAT_1:66

    (R | X) = {} iff ( dom R) misses X

    proof

      thus (R | X) = {} implies ( dom R) misses X

      proof

        assume

         A1: (R | X) = {} ;

        thus (( dom R) /\ X) = {}

        proof

          thus (( dom R) /\ X) c= {}

          proof

            let x be object;

            assume

             A2: x in (( dom R) /\ X);

            then x in ( dom R) by XBOOLE_0:def 4;

            then

             A3: ex y be object st [x, y] in R by XTUPLE_0:def 12;

            x in X by A2, XBOOLE_0:def 4;

            hence thesis by A1, A3, Def9;

          end;

          thus thesis;

        end;

      end;

      assume

       A4: (( dom R) /\ X) = {} ;

      let x, y;

      hereby

        assume

         A5: [x, y] in (R | X);

        then x in X by Def9;

        then

         A6: not x in ( dom R) by A4, XBOOLE_0:def 4;

         [x, y] in R by A5, Def9;

        hence [x, y] in {} by A6, XTUPLE_0:def 12;

      end;

      thus thesis;

    end;

    theorem :: RELAT_1:67

    

     Th61: (R | X) = (R /\ [:X, ( rng R):])

    proof

      set P = (R /\ [:X, ( rng R):]);

      let x, y;

      thus [x, y] in (R | X) implies [x, y] in P

      proof

        assume

         A1: [x, y] in (R | X);

        then

         A2: x in X by Def9;

        

         A3: [x, y] in R by A1, Def9;

        then y in ( rng R) by XTUPLE_0:def 13;

        then [x, y] in [:X, ( rng R):] by A2, ZFMISC_1:def 2;

        hence thesis by A3, XBOOLE_0:def 4;

      end;

      assume

       A4: [x, y] in P;

      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 thesis by A5, Def9;

    end;

    theorem :: RELAT_1:68

    

     Th62: ( dom R) c= X implies (R | X) = R

    proof

      assume ( dom R) c= X;

      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 Th1, Th61;

      hence thesis by A1, XBOOLE_1: 1, XBOOLE_1: 28;

    end;

    registration

      let R;

      reduce (R | ( dom R)) to R;

      reducibility by Th62;

    end

    theorem :: RELAT_1:69

    (R | ( dom R)) = R;

    theorem :: RELAT_1:70

    ( rng (R | X)) c= ( rng R) by Th53, XTUPLE_0: 9;

    theorem :: RELAT_1:71

    

     Th65: ((R | X) | Y) = (R | (X /\ Y))

    proof

      let x, y;

      

       A1: [x, y] in (R | X) iff [x, y] in R & x in X by Def9;

      

       A2: [x, y] in (R | (X /\ Y)) iff [x, y] in R & x in (X /\ Y) by Def9;

       [x, y] in ((R | X) | Y) iff [x, y] in (R | X) & x in Y by Def9;

      hence thesis by A1, A2, XBOOLE_0:def 4;

    end;

    registration

      let R, X;

      reduce ((R | X) | X) to (R | X);

      reducibility

      proof

        (X /\ X) = X;

        hence thesis by Th65;

      end;

    end

    theorem :: RELAT_1:72

    ((R | X) | X) = (R | X);

    theorem :: RELAT_1:73

    X c= Y implies ((R | X) | Y) = (R | X)

    proof

      X c= Y implies (X /\ Y) = X by XBOOLE_1: 28;

      hence thesis by Th65;

    end;

    theorem :: RELAT_1:74

    Y c= X implies ((R | X) | Y) = (R | Y)

    proof

      Y c= X implies (X /\ Y) = Y by XBOOLE_1: 28;

      hence thesis by Th65;

    end;

    theorem :: RELAT_1:75

    

     Th69: X c= Y implies (R | X) c= (R | Y)

    proof

      assume

       A1: X c= Y;

      let x, y;

      assume [x, y] in (R | X);

      then x in X & [x, y] in R by Def9;

      hence [x, y] in (R | Y) by A1, Def9;

    end;

    theorem :: RELAT_1:76

    

     Th70: P c= R implies (P | X) c= (R | X)

    proof

      assume

       A1: P c= R;

      let x, y;

      assume [x, y] in (P | X);

      then [x, y] in P & x in X by Def9;

      hence thesis by A1, Def9;

    end;

    theorem :: RELAT_1:77

    

     Th71: P c= R & X c= Y implies (P | X) c= (R | Y)

    proof

      assume P c= R & X c= Y;

      then (P | X) c= (R | X) & (R | X) c= (R | Y) by Th69, Th70;

      hence thesis;

    end;

    theorem :: RELAT_1:78

    

     Th72: (R | (X \/ Y)) = ((R | X) \/ (R | Y))

    proof

      let x, y;

      hereby

        assume

         A1: [x, y] in (R | (X \/ Y));

        then x in (X \/ Y) by Def9;

        then

         A2: x in X or x in Y by XBOOLE_0:def 3;

         [x, y] in R by A1, Def9;

        then [x, y] in (R | X) or [x, y] in (R | Y) by A2, Def9;

        hence [x, y] in ((R | X) \/ (R | Y)) by XBOOLE_0:def 3;

      end;

      assume

       A3: [x, y] in ((R | X) \/ (R | Y));

      per cases by A3, XBOOLE_0:def 3;

        suppose

         A4: [x, y] in (R | Y);

        then x in Y by Def9;

        then

         A5: x in (X \/ Y) by XBOOLE_0:def 3;

         [x, y] in R by A4, Def9;

        hence [x, y] in (R | (X \/ Y)) by A5, Def9;

      end;

        suppose

         A6: [x, y] in (R | X);

        then x in X by Def9;

        then

         A7: x in (X \/ Y) by XBOOLE_0:def 3;

         [x, y] in R by A6, Def9;

        hence [x, y] in (R | (X \/ Y)) by A7, Def9;

      end;

    end;

    theorem :: RELAT_1:79

    (R | (X /\ Y)) = ((R | X) /\ (R | Y))

    proof

      let x, y;

      hereby

        assume

         A1: [x, y] in (R | (X /\ Y));

        then

         A2: x in (X /\ Y) by Def9;

        

         A3: [x, y] in R by A1, Def9;

        x in Y by A2, XBOOLE_0:def 4;

        then

         A4: [x, y] in (R | Y) by A3, Def9;

        x in X by A2, XBOOLE_0:def 4;

        then [x, y] in (R | X) by A3, Def9;

        hence [x, y] in ((R | X) /\ (R | Y)) by A4, XBOOLE_0:def 4;

      end;

      assume

       A5: [x, y] in ((R | X) /\ (R | Y));

      then [x, y] in (R | Y) by XBOOLE_0:def 4;

      then

       A6: x in Y by Def9;

      

       A7: [x, y] in (R | X) by A5, XBOOLE_0:def 4;

      then x in X by Def9;

      then

       A8: x in (X /\ Y) by A6, XBOOLE_0:def 4;

       [x, y] in R by A7, Def9;

      hence [x, y] in (R | (X /\ Y)) by A8, Def9;

    end;

    theorem :: RELAT_1:80

    

     Th74: (R | (X \ Y)) = ((R | X) \ (R | Y))

    proof

      let x, y;

      hereby

        assume

         A1: [x, y] in (R | (X \ Y));

        then

         A2: x in (X \ Y) by Def9;

        then not x in Y by XBOOLE_0:def 5;

        then

         A3: not [x, y] in (R | Y) by Def9;

         [x, y] in R by A1, Def9;

        then [x, y] in (R | X) by A2, Def9;

        hence [x, y] in ((R | X) \ (R | Y)) by A3, XBOOLE_0:def 5;

      end;

      assume

       A4: [x, y] in ((R | X) \ (R | Y));

      then

       A5: [x, y] in R by Def9;

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

      x in X by A4, Def9;

      then x in (X \ Y) by A4, A6, Def9, XBOOLE_0:def 5;

      hence [x, y] in (R | (X \ Y)) by A5, Def9;

    end;

    registration

      let R be empty Relation, X be set;

      cluster (R | X) -> empty;

      coherence

      proof

        for x, y st [x, y] in ( {} | X) holds contradiction by Def9;

        hence thesis by Th31;

      end;

    end

    theorem :: RELAT_1:81

    (R | {} ) = {} ;

    theorem :: RELAT_1:82

    ( {} | X) = {} ;

    theorem :: RELAT_1:83

    ((P * R) | X) = ((P | X) * R)

    proof

      let x, y;

      hereby

        assume

         A1: [x, y] in ((P * R) | X);

        then [x, y] in (P * R) by Def9;

        then

        consider a such that

         A2: [x, a] in P and

         A3: [a, y] in R by Def6;

        x in X by A1, Def9;

        then [x, a] in (P | X) by A2, Def9;

        hence [x, y] in ((P | X) * R) by A3, Def6;

      end;

      assume [x, y] in ((P | X) * R);

      then

      consider a such that

       A4: [x, a] in (P | X) and

       A5: [a, y] in R by Def6;

       [x, a] in P by A4, Def9;

      then

       A6: [x, y] in (P * R) by A5, Def6;

      x in X by A4, Def9;

      hence [x, y] in ((P * R) | X) by A6, Def9;

    end;

    definition

      let Y, R;

      :: RELAT_1:def12

      func Y |` R -> Relation means

      : Def10: [x, y] in it iff y in Y & [x, y] in R;

      existence

      proof

        defpred Z[ object, object] means $2 in Y & [$1, $2] in R;

        consider P such that

         A1: for x, y holds [x, y] in P iff x in ( dom R) & y in ( rng R) & Z[x, y] from RelExistence;

        take P;

        let x, y;

        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 thesis by A1;

      end;

      uniqueness

      proof

        let P1, P2;

        assume that

         A2: [x, y] in P1 iff y in Y & [x, y] in R and

         A3: [x, y] in P2 iff y in Y & [x, y] in R;

        let x, y;

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

      end;

    end

    registration

      let R be Relation, X be empty set;

      cluster (X |` R) -> empty;

      coherence

      proof

         not [x, y] in (X |` R) by Def10;

        hence thesis by Th31;

      end;

    end

    theorem :: RELAT_1:84

    

     Th78: y in ( rng (Y |` R)) iff y in Y & y in ( rng R)

    proof

      thus y in ( rng (Y |` R)) implies y in Y & y in ( rng R)

      proof

        assume y in ( rng (Y |` R));

        then

        consider x be object such that

         A1: [x, y] in (Y |` R) by XTUPLE_0:def 13;

         [x, y] in R by A1, Def10;

        hence thesis by A1, Def10, XTUPLE_0:def 13;

      end;

      assume

       A2: y in Y;

      assume y in ( rng R);

      then

      consider x be object such that

       A3: [x, y] in R by XTUPLE_0:def 13;

       [x, y] in (Y |` R) by A2, A3, Def10;

      hence thesis by XTUPLE_0:def 13;

    end;

    theorem :: RELAT_1:85

    ( rng (Y |` R)) c= Y by Th78;

    theorem :: RELAT_1:86

    

     Th80: (Y |` R) c= R by Def10;

    theorem :: RELAT_1:87

    ( rng (Y |` R)) c= ( rng R) by Th80, XTUPLE_0: 9;

    theorem :: RELAT_1:88

    

     Th82: ( rng (Y |` R)) = (( rng R) /\ Y)

    proof

      ( rng (Y |` R)) c= Y & ( rng (Y |` R)) c= ( rng R) by Th78;

      hence ( rng (Y |` R)) c= (( rng R) /\ Y) by XBOOLE_1: 19;

      let y be object;

      assume

       A1: y in (( rng R) /\ Y);

      then y in ( rng R) by XBOOLE_0:def 4;

      then

      consider x be object 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, Def10;

      hence thesis by XTUPLE_0:def 13;

    end;

    theorem :: RELAT_1:89

    Y c= ( rng R) implies ( rng (Y |` R)) = Y

    proof

      assume Y c= ( rng R);

      then (( rng R) /\ Y) = Y by XBOOLE_1: 28;

      hence thesis by Th82;

    end;

    theorem :: RELAT_1:90

    ((Y |` R) * P) c= (R * P) by Th24, Th80;

    theorem :: RELAT_1:91

    (P * (Y |` R)) c= (P * R) by Th23, Th80;

    theorem :: RELAT_1:92

    (Y |` R) = (R * ( id Y))

    proof

      let x, y;

       [x, y] in (Y |` R) iff y in Y & [x, y] in R by Def10;

      hence thesis by Th43;

    end;

    theorem :: RELAT_1:93

    

     Th87: (Y |` R) = (R /\ [:( dom R), Y:])

    proof

      set P = (R /\ [:( dom R), Y:]);

      let x, y;

      thus [x, y] in (Y |` R) implies [x, y] in P

      proof

        assume

         A1: [x, y] in (Y |` R);

        then

         A2: y in Y by Def10;

        

         A3: [x, y] in R by A1, Def10;

        then x in ( dom R) by XTUPLE_0:def 12;

        then [x, y] in [:( dom R), Y:] by A2, ZFMISC_1:def 2;

        hence thesis by A3, XBOOLE_0:def 4;

      end;

      assume

       A4: [x, y] in P;

      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 thesis by A5, Def10;

    end;

    theorem :: RELAT_1:94

    

     Th88: ( rng R) c= Y implies (Y |` R) = R

    proof

      assume ( rng R) c= Y;

      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 Th1, Th87;

      hence thesis by A1, XBOOLE_1: 1, XBOOLE_1: 28;

    end;

    registration

      let R;

      reduce (( rng R) |` R) to R;

      reducibility by Th88;

    end

    theorem :: RELAT_1:95

    (( rng R) |` R) = R;

    theorem :: RELAT_1:96

    

     Th90: (Y |` (X |` R)) = ((Y /\ X) |` R)

    proof

      let x, y;

      

       A1: [x, y] in (X |` R) iff [x, y] in R & y in X by Def10;

      

       A2: [x, y] in ((Y /\ X) |` R) iff [x, y] in R & y in (Y /\ X) by Def10;

       [x, y] in (Y |` (X |` R)) iff [x, y] in (X |` R) & y in Y by Def10;

      hence thesis by A1, A2, XBOOLE_0:def 4;

    end;

    registration

      let Y, R;

      reduce (Y |` (Y |` R)) to (Y |` R);

      reducibility

      proof

        (Y /\ Y) = Y;

        hence thesis by Th90;

      end;

    end

    theorem :: RELAT_1:97

    (Y |` (Y |` R)) = (Y |` R);

    theorem :: RELAT_1:98

    X c= Y implies (Y |` (X |` R)) = (X |` R)

    proof

      X c= Y implies (Y /\ X) = X by XBOOLE_1: 28;

      hence thesis by Th90;

    end;

    theorem :: RELAT_1:99

    Y c= X implies (Y |` (X |` R)) = (Y |` R)

    proof

      Y c= X implies (Y /\ X) = Y by XBOOLE_1: 28;

      hence thesis by Th90;

    end;

    theorem :: RELAT_1:100

    

     Th94: X c= Y implies (X |` R) c= (Y |` R)

    proof

      assume

       A1: X c= Y;

      let x, y;

       [x, y] in (X |` R) iff [x, y] in R & y in X by Def10;

      hence thesis by A1, Def10;

    end;

    theorem :: RELAT_1:101

    

     Th95: P1 c= P2 implies (Y |` P1) c= (Y |` P2)

    proof

      assume

       A1: P1 c= P2;

      let x, y;

      assume [x, y] in (Y |` P1);

      then [x, y] in P1 & y in Y by Def10;

      hence thesis by A1, Def10;

    end;

    theorem :: RELAT_1:102

    P1 c= P2 & Y1 c= Y2 implies (Y1 |` P1) c= (Y2 |` P2)

    proof

      assume P1 c= P2 & Y1 c= Y2;

      then (Y1 |` P1) c= (Y1 |` P2) & (Y1 |` P2) c= (Y2 |` P2) by Th94, Th95;

      hence thesis;

    end;

    theorem :: RELAT_1:103

    ((X \/ Y) |` R) = ((X |` R) \/ (Y |` R))

    proof

      let x, y;

      

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

      hence thesis by A1, A2, Def10;

    end;

    theorem :: RELAT_1:104

    ((X /\ Y) |` R) = ((X |` R) /\ (Y |` R))

    proof

      let x, y;

      

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

      hence thesis by A1, A2, Def10;

    end;

    theorem :: RELAT_1:105

    ((X \ Y) |` R) = ((X |` R) \ (Y |` R))

    proof

      let x, y;

      

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

      hence thesis by A1, A2, Def10;

    end;

    theorem :: RELAT_1:106

    ( {} |` R) = {} ;

    theorem :: RELAT_1:107

    (Y |` {} ) = {} by Def10;

    theorem :: RELAT_1:108

    (Y |` (P * R)) = (P * (Y |` R))

    proof

      let x, y;

      hereby

        assume

         A1: [x, y] in (Y |` (P * R));

        then [x, y] in (P * R) by Def10;

        then

        consider a such that

         A2: [x, a] in P and

         A3: [a, y] in R by Def6;

        y in Y by A1, Def10;

        then [a, y] in (Y |` R) by A3, Def10;

        hence [x, y] in (P * (Y |` R)) by A2, Def6;

      end;

      assume [x, y] in (P * (Y |` R));

      then

      consider a such that

       A4: [x, a] in P and

       A5: [a, y] in (Y |` R) by Def6;

       [a, y] in R by A5, Def10;

      then

       A6: [x, y] in (P * R) by A4, Def6;

      y in Y by A5, Def10;

      hence [x, y] in (Y |` (P * R)) by A6, Def10;

    end;

    theorem :: RELAT_1:109

    ((Y |` R) | X) = (Y |` (R | X))

    proof

      let x, y;

      

       A1: [x, y] in R & x in X iff [x, y] in (R | X) by Def9;

       [x, y] in (Y |` R) iff [x, y] in R & y in Y by Def10;

      hence thesis by A1, Def9, Def10;

    end;

    definition

      let R, X;

      :: RELAT_1:def13

      func R .: X -> set means

      : Def11: y in it iff ex x st [x, y] in R & x in X;

      existence

      proof

        defpred Z[ object] means ex x st [x, $1] in R & x in X;

        consider Y such that

         A1: for y be object holds y in Y iff y in ( rng R) & Z[y] from XBOOLE_0:sch 1;

        take Y;

        let y;

        thus y in Y implies ex x st [x, y] in R & x in X by A1;

        given x such that

         A2: [x, y] in R and

         A3: x in X;

        y in ( rng R) by A2, XTUPLE_0:def 13;

        hence thesis by A1, A2, A3;

      end;

      uniqueness

      proof

        let Y1, Y2;

        assume that

         A4: y in Y1 iff ex x st [x, y] in R & x in X and

         A5: y in Y2 iff ex x st [x, y] in R & x in X;

        now

          let y be object;

          y in Y1 iff ex x st [x, y] in R & x in X by A4;

          hence y in Y1 iff y in Y2 by A5;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    theorem :: RELAT_1:110

    

     Th104: y in (R .: X) iff ex x st x in ( dom R) & [x, y] in R & x in X

    proof

      thus y in (R .: X) implies ex x st x in ( dom R) & [x, y] in R & x in X

      proof

        assume y in (R .: X);

        then

        consider x such that

         A1: [x, y] in R & x in X by Def11;

        take x;

        thus thesis by A1, XTUPLE_0:def 12;

      end;

      thus thesis by Def11;

    end;

    theorem :: RELAT_1:111

    

     Th105: (R .: X) c= ( rng R)

    proof

      let y be object;

      assume y in (R .: X);

      then ex x st [x, y] in R & x in X by Def11;

      hence thesis by XTUPLE_0:def 13;

    end;

    theorem :: RELAT_1:112

    (R .: X) = (R .: (( dom R) /\ X))

    proof

      for y be object holds y in (R .: X) iff y in (R .: (( dom R) /\ X))

      proof

        let y be object;

        thus y in (R .: X) implies y in (R .: (( dom R) /\ X))

        proof

          assume y in (R .: X);

          then

          consider x such that

           A1: x in ( dom R) and

           A2: [x, y] in R and

           A3: x in X by Th104;

          x in (( dom R) /\ X) by A1, A3, XBOOLE_0:def 4;

          hence thesis by A2, Def11;

        end;

        assume y in (R .: (( dom R) /\ X));

        then

        consider x such that x in ( dom R) and

         A4: [x, y] in R and

         A5: x in (( dom R) /\ X) by Th104;

        x in X by A5, XBOOLE_0:def 4;

        hence thesis by A4, Def11;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: RELAT_1:113

    

     Th107: (R .: ( dom R)) = ( rng R)

    proof

      thus (R .: ( dom R)) c= ( rng R) by Th105;

      let y be object;

      assume y in ( rng R);

      then

      consider x be object such that

       A1: [x, y] in R by XTUPLE_0:def 13;

      x in ( dom R) by A1, XTUPLE_0:def 12;

      hence thesis by A1, Def11;

    end;

    theorem :: RELAT_1:114

    (R .: X) c= (R .: ( dom R))

    proof

      (R .: X) c= ( rng R) by Th105;

      hence thesis by Th107;

    end;

    theorem :: RELAT_1:115

    ( rng (R | X)) = (R .: X)

    proof

      for y be object holds y in ( rng (R | X)) iff y in (R .: X)

      proof

        let y be object;

        thus y in ( rng (R | X)) implies y in (R .: X)

        proof

          assume y in ( rng (R | X));

          then

          consider x be object such that

           A1: [x, y] in (R | X) by XTUPLE_0:def 13;

          x in X & [x, y] in R by A1, Def9;

          hence thesis by Def11;

        end;

        assume y in (R .: X);

        then

        consider x such that

         A2: [x, y] in R & x in X by Def11;

         [x, y] in (R | X) by A2, Def9;

        hence thesis by XTUPLE_0:def 13;

      end;

      hence thesis by TARSKI: 2;

    end;

    registration

      let R;

      let X be empty set;

      cluster (R .: X) -> empty;

      coherence

      proof

        set y = the Element of (R .: {} );

        y in (R .: {} ) implies ex x st [x, y] in R & x in {} by Def11;

        hence thesis;

      end;

    end

    registration

      let R be empty Relation;

      let X;

      cluster (R .: X) -> empty;

      coherence

      proof

        assume not thesis;

        then ex x st [x, the Element of ( {} .: X)] in {} & x in X by Def11;

        hence contradiction;

      end;

    end

    ::$Canceled

    theorem :: RELAT_1:118

    (R .: X) = {} iff ( dom R) misses X

    proof

      set y = the Element of (R .: X);

      thus (R .: X) = {} implies ( dom R) misses X

      proof

        assume

         A1: (R .: X) = {} ;

        assume not thesis;

        then

        consider x be object such that

         A2: x in ( dom R) and

         A3: x in X by XBOOLE_0: 3;

        ex y be object st [x, y] in R by A2, XTUPLE_0:def 12;

        hence contradiction by A1, A2, A3, Th104;

      end;

      assume

       A4: (( dom R) /\ X) = {} ;

      assume not thesis;

      then ex x st x in ( dom R) & [x, y] in R & x in X by Th104;

      hence contradiction by A4, XBOOLE_0:def 4;

    end;

    theorem :: RELAT_1:119

    X <> {} & X c= ( dom R) implies (R .: X) <> {}

    proof

      assume that

       A1: X <> {} and

       A2: X c= ( dom R);

      set x = the Element of X;

      

       A3: x in ( dom R) by A1, A2;

      then ex y be object st [x, y] in R by XTUPLE_0:def 12;

      hence thesis by A1, A3, Th104;

    end;

    theorem :: RELAT_1:120

    (R .: (X \/ Y)) = ((R .: X) \/ (R .: Y))

    proof

      thus (R .: (X \/ Y)) c= ((R .: X) \/ (R .: Y))

      proof

        let y be object;

        assume y in (R .: (X \/ Y));

        then

        consider x such that

         A1: [x, y] in R and

         A2: x in (X \/ Y) by Def11;

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

        hence y in ((R .: X) \/ (R .: Y)) by XBOOLE_0:def 3;

      end;

      let y be object;

      assume

       A3: y in ((R .: X) \/ (R .: Y));

      per cases by A3, XBOOLE_0:def 3;

        suppose y in (R .: Y);

        then

        consider x such that

         A4: [x, y] in R and

         A5: x in Y by Def11;

        x in (X \/ Y) by A5, XBOOLE_0:def 3;

        hence y in (R .: (X \/ Y)) by A4, Def11;

      end;

        suppose y in (R .: X);

        then

        consider x such that

         A6: [x, y] in R and

         A7: x in X by Def11;

        x in (X \/ Y) by A7, XBOOLE_0:def 3;

        hence y in (R .: (X \/ Y)) by A6, Def11;

      end;

    end;

    theorem :: RELAT_1:121

    (R .: (X /\ Y)) c= ((R .: X) /\ (R .: Y))

    proof

      let y be object;

      assume y in (R .: (X /\ Y));

      then

      consider x such that

       A1: [x, y] in R and

       A2: x in (X /\ Y) by Def11;

      x in Y by A2, XBOOLE_0:def 4;

      then

       A3: y in (R .: Y) by A1, Def11;

      x in X by A2, XBOOLE_0:def 4;

      then y in (R .: X) by A1, Def11;

      hence thesis by A3, XBOOLE_0:def 4;

    end;

    theorem :: RELAT_1:122

    ((R .: X) \ (R .: Y)) c= (R .: (X \ Y))

    proof

      let y be object;

      assume

       A1: y in ((R .: X) \ (R .: Y));

      then

      consider x such that

       A2: [x, y] in R and

       A3: x in X by Def11;

       not y in (R .: Y) by A1, XBOOLE_0:def 5;

      then not x in Y or not [x, y] in R by Def11;

      then x in (X \ Y) by A2, A3, XBOOLE_0:def 5;

      hence thesis by A2, Def11;

    end;

    theorem :: RELAT_1:123

    

     Th115: X c= Y implies (R .: X) c= (R .: Y)

    proof

      assume

       A1: X c= Y;

      let y be object;

      assume y in (R .: X);

      then ex x st [x, y] in R & x in X by Def11;

      hence thesis by A1, Def11;

    end;

    theorem :: RELAT_1:124

    

     Th116: P c= R implies (P .: X) c= (R .: X)

    proof

      assume

       A1: P c= R;

      let y be object;

      assume y in (P .: X);

      then ex x st [x, y] in P & x in X by Def11;

      hence thesis by A1, Def11;

    end;

    theorem :: RELAT_1:125

    P c= R & X c= Y implies (P .: X) c= (R .: Y)

    proof

      assume P c= R & X c= Y;

      then (P .: X) c= (R .: X) & (R .: X) c= (R .: Y) by Th115, Th116;

      hence thesis;

    end;

    theorem :: RELAT_1:126

    ((P * R) .: X) = (R .: (P .: X))

    proof

      for y be object holds y in ((P * R) .: X) iff y in (R .: (P .: X))

      proof

        let y be object;

        thus y in ((P * R) .: X) implies y in (R .: (P .: X))

        proof

          assume y in ((P * R) .: X);

          then

          consider x such that

           A1: [x, y] in (P * R) and

           A2: x in X by Def11;

          consider z such that

           A3: [x, z] in P and

           A4: [z, y] in R by A1, Def6;

          z in (P .: X) by A2, A3, Def11;

          hence thesis by A4, Def11;

        end;

        assume y in (R .: (P .: X));

        then

        consider x such that

         A5: [x, y] in R and

         A6: x in (P .: X) by Def11;

        consider z such that

         A7: [z, x] in P and

         A8: z in X by A6, Def11;

         [z, y] in (P * R) by A5, A7, Def6;

        hence thesis by A8, Def11;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: RELAT_1:127

    

     Th119: ( rng (P * R)) = (R .: ( rng P))

    proof

      for z be object holds z in ( rng (P * R)) iff z in (R .: ( rng P))

      proof

        let z be object;

        thus z in ( rng (P * R)) implies z in (R .: ( rng P))

        proof

          assume z in ( rng (P * R));

          then

          consider x be object such that

           A1: [x, z] in (P * R) by XTUPLE_0:def 13;

          consider y such that

           A2: [x, y] in P and

           A3: [y, z] in R by A1, Def6;

          y in ( rng P) by A2, XTUPLE_0:def 13;

          hence thesis by A3, Def11;

        end;

        assume z in (R .: ( rng P));

        then

        consider y such that

         A4: [y, z] in R and

         A5: y in ( rng P) by Def11;

        consider x be object such that

         A6: [x, y] in P by A5, XTUPLE_0:def 13;

         [x, z] in (P * R) by A4, A6, Def6;

        hence thesis by XTUPLE_0:def 13;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: RELAT_1:128

    ((R | X) .: Y) c= (R .: Y) by Th53, Th116;

    theorem :: RELAT_1:129

    

     Th121: for R be Relation, X,Y be set st X c= Y holds ((R | Y) .: X) = (R .: X)

    proof

      let R be Relation, X,Y be set such that

       A1: X c= Y;

      thus ((R | Y) .: X) c= (R .: X) by Th53, Th116;

      let y be object;

      assume y in (R .: X);

      then

      consider x1 be object such that

       A2: [x1, y] in R and

       A3: x1 in X by Def11;

      ex x be object st [x, y] in (R | Y) & x in X

      proof

        take x1;

        thus [x1, y] in (R | Y) by A1, A2, A3, Def9;

        thus thesis by A3;

      end;

      hence thesis by Def11;

    end;

    theorem :: RELAT_1:130

    (( dom R) /\ X) c= ((R ~ ) .: (R .: X))

    proof

      let x be object;

      assume

       A1: x in (( dom R) /\ X);

      then x in ( dom R) by XBOOLE_0:def 4;

      then

      consider y be object such that

       A2: [x, y] in R by XTUPLE_0:def 12;

      

       A3: [y, x] in (R ~ ) by A2, Def5;

      x in X by A1, XBOOLE_0:def 4;

      then y in (R .: X) by A2, Def11;

      hence thesis by A3, Def11;

    end;

    definition

      let R, Y;

      :: RELAT_1:def14

      func R " Y -> set means

      : Def12: x in it iff ex y st [x, y] in R & y in Y;

      existence

      proof

        defpred Z[ object] means ex y st [$1, y] in R & y in Y;

        consider X such that

         A1: for x be object holds x in X iff x in ( dom R) & Z[x] from XBOOLE_0:sch 1;

        take X;

        let x;

        thus x in X implies ex y st [x, y] in R & y in Y by A1;

        given y such that

         A2: [x, y] in R and

         A3: y in Y;

        x in ( dom R) by A2, XTUPLE_0:def 12;

        hence thesis by A1, A2, A3;

      end;

      uniqueness

      proof

        let X1, X2;

        assume that

         A4: x in X1 iff ex y st [x, y] in R & y in Y and

         A5: x in X2 iff ex y st [x, y] in R & y in Y;

        now

          let x be object;

          x in X1 iff ex y st [x, y] in R & y in Y by A4;

          hence x in X1 iff x in X2 by A5;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    theorem :: RELAT_1:131

    

     Th123: x in (R " Y) iff ex y st y in ( rng R) & [x, y] in R & y in Y

    proof

      thus x in (R " Y) implies ex y st y in ( rng R) & [x, y] in R & y in Y

      proof

        assume x in (R " Y);

        then

        consider y such that

         A1: [x, y] in R & y in Y by Def12;

        take y;

        thus thesis by A1, XTUPLE_0:def 13;

      end;

      thus thesis by Def12;

    end;

    theorem :: RELAT_1:132

    

     Th124: (R " Y) c= ( dom R)

    proof

      let x be object;

      assume x in (R " Y);

      then ex y st [x, y] in R & y in Y by Def12;

      hence thesis by XTUPLE_0:def 12;

    end;

    theorem :: RELAT_1:133

    (R " Y) = (R " (( rng R) /\ Y))

    proof

      for x be object holds x in (R " Y) iff x in (R " (( rng R) /\ Y))

      proof

        let x be object;

        thus x in (R " Y) implies x in (R " (( rng R) /\ Y))

        proof

          assume x in (R " Y);

          then

          consider y such that

           A1: y in ( rng R) and

           A2: [x, y] in R and

           A3: y in Y by Th123;

          y in (( rng R) /\ Y) by A1, A3, XBOOLE_0:def 4;

          hence thesis by A2, Def12;

        end;

        assume x in (R " (( rng R) /\ Y));

        then

        consider y such that y in ( rng R) and

         A4: [x, y] in R and

         A5: y in (( rng R) /\ Y) by Th123;

        y in Y by A5, XBOOLE_0:def 4;

        hence thesis by A4, Def12;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: RELAT_1:134

    

     Th126: (R " ( rng R)) = ( dom R)

    proof

      thus (R " ( rng R)) c= ( dom R) by Th124;

      let x be object;

      assume x in ( dom R);

      then

      consider y be object such that

       A1: [x, y] in R by XTUPLE_0:def 12;

      y in ( rng R) by A1, XTUPLE_0:def 13;

      hence thesis by A1, Def12;

    end;

    theorem :: RELAT_1:135

    (R " Y) c= (R " ( rng R))

    proof

      (R " Y) c= ( dom R) by Th124;

      hence thesis by Th126;

    end;

    registration

      let R;

      let Y be empty set;

      cluster (R " Y) -> empty;

      coherence

      proof

        set x = the Element of (R " {} );

        x in (R " {} ) implies ex y st [x, y] in R & y in {} by Def12;

        hence thesis;

      end;

    end

    registration

      let R be empty Relation;

      let Y;

      cluster (R " Y) -> empty;

      coherence

      proof

        assume not thesis;

        then ex y st [ the Element of ( {} " Y), y] in {} & y in Y by Def12;

        hence contradiction;

      end;

    end

    ::$Canceled

    theorem :: RELAT_1:138

    (R " Y) = {} iff ( rng R) misses Y

    proof

      set x = the Element of (R " Y);

      thus (R " Y) = {} implies ( rng R) misses Y

      proof

        assume

         A1: (R " Y) = {} ;

        assume not thesis;

        then

        consider y be object such that

         A2: y in ( rng R) and

         A3: y in Y by XBOOLE_0: 3;

        ex x be object st [x, y] in R by A2, XTUPLE_0:def 13;

        hence contradiction by A1, A2, A3, Th123;

      end;

      assume

       A4: (( rng R) /\ Y) = {} ;

      assume not thesis;

      then ex y st y in ( rng R) & [x, y] in R & y in Y by Th123;

      hence contradiction by A4, XBOOLE_0:def 4;

    end;

    theorem :: RELAT_1:139

    Y <> {} & Y c= ( rng R) implies (R " Y) <> {}

    proof

      assume that

       A1: Y <> {} and

       A2: Y c= ( rng R);

      set y = the Element of Y;

      

       A3: y in ( rng R) by A1, A2;

      then ex x be object st [x, y] in R by XTUPLE_0:def 13;

      hence thesis by A1, A3, Th123;

    end;

    theorem :: RELAT_1:140

    (R " (X \/ Y)) = ((R " X) \/ (R " Y))

    proof

      thus (R " (X \/ Y)) c= ((R " X) \/ (R " Y))

      proof

        let x be object;

        assume x in (R " (X \/ Y));

        then

        consider y such that

         A1: [x, y] in R and

         A2: y in (X \/ Y) by Def12;

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

        hence x in ((R " X) \/ (R " Y)) by XBOOLE_0:def 3;

      end;

      let x be object;

      assume

       A3: x in ((R " X) \/ (R " Y));

      per cases by A3, XBOOLE_0:def 3;

        suppose x in (R " Y);

        then

        consider y such that

         A4: [x, y] in R and

         A5: y in Y by Def12;

        y in (X \/ Y) by A5, XBOOLE_0:def 3;

        hence x in (R " (X \/ Y)) by A4, Def12;

      end;

        suppose x in (R " X);

        then

        consider y such that

         A6: [x, y] in R and

         A7: y in X by Def12;

        y in (X \/ Y) by A7, XBOOLE_0:def 3;

        hence x in (R " (X \/ Y)) by A6, Def12;

      end;

    end;

    theorem :: RELAT_1:141

    (R " (X /\ Y)) c= ((R " X) /\ (R " Y))

    proof

      let x be object;

      assume x in (R " (X /\ Y));

      then

      consider y such that

       A1: [x, y] in R and

       A2: y in (X /\ Y) by Def12;

      y in Y by A2, XBOOLE_0:def 4;

      then

       A3: x in (R " Y) by A1, Def12;

      y in X by A2, XBOOLE_0:def 4;

      then x in (R " X) by A1, Def12;

      hence thesis by A3, XBOOLE_0:def 4;

    end;

    theorem :: RELAT_1:142

    ((R " X) \ (R " Y)) c= (R " (X \ Y))

    proof

      let x be object;

      assume

       A1: x in ((R " X) \ (R " Y));

      then

      consider y such that

       A2: [x, y] in R and

       A3: y in X by Def12;

       not x in (R " Y) by A1, XBOOLE_0:def 5;

      then not y in Y or not [x, y] in R by Def12;

      then y in (X \ Y) by A2, A3, XBOOLE_0:def 5;

      hence thesis by A2, Def12;

    end;

    theorem :: RELAT_1:143

    

     Th133: X c= Y implies (R " X) c= (R " Y)

    proof

      assume

       A1: X c= Y;

      let x be object;

      assume x in (R " X);

      then ex y st [x, y] in R & y in X by Def12;

      hence thesis by A1, Def12;

    end;

    theorem :: RELAT_1:144

    

     Th134: P c= R implies (P " Y) c= (R " Y)

    proof

      assume

       A1: P c= R;

      let x be object;

      assume x in (P " Y);

      then ex y st [x, y] in P & y in Y by Def12;

      hence thesis by A1, Def12;

    end;

    theorem :: RELAT_1:145

    P c= R & X c= Y implies (P " X) c= (R " Y)

    proof

      assume P c= R & X c= Y;

      then (P " X) c= (R " X) & (R " X) c= (R " Y) by Th133, Th134;

      hence thesis;

    end;

    theorem :: RELAT_1:146

    ((P * R) " Y) = (P " (R " Y))

    proof

      for x be object holds x in ((P * R) " Y) iff x in (P " (R " Y))

      proof

        let x be object;

        thus x in ((P * R) " Y) implies x in (P " (R " Y))

        proof

          assume x in ((P * R) " Y);

          then

          consider y such that

           A1: [x, y] in (P * R) and

           A2: y in Y by Def12;

          consider z such that

           A3: [x, z] in P and

           A4: [z, y] in R by A1, Def6;

          z in (R " Y) by A2, A4, Def12;

          hence thesis by A3, Def12;

        end;

        assume x in (P " (R " Y));

        then

        consider y such that

         A5: [x, y] in P and

         A6: y in (R " Y) by Def12;

        consider z such that

         A7: [y, z] in R and

         A8: z in Y by A6, Def12;

         [x, z] in (P * R) by A5, A7, Def6;

        hence thesis by A8, Def12;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: RELAT_1:147

    

     Th137: ( dom (P * R)) = (P " ( dom R))

    proof

      for z be object holds z in ( dom (P * R)) iff z in (P " ( dom R))

      proof

        let z be object;

        thus z in ( dom (P * R)) implies z in (P " ( dom R))

        proof

          assume z in ( dom (P * R));

          then

          consider x be object such that

           A1: [z, x] in (P * R) by XTUPLE_0:def 12;

          consider y such that

           A2: [z, y] in P and

           A3: [y, x] in R by A1, Def6;

          y in ( dom R) by A3, XTUPLE_0:def 12;

          hence thesis by A2, Def12;

        end;

        assume z in (P " ( dom R));

        then

        consider y such that

         A4: [z, y] in P and

         A5: y in ( dom R) by Def12;

        consider x be object such that

         A6: [y, x] in R by A5, XTUPLE_0:def 12;

         [z, x] in (P * R) by A4, A6, Def6;

        hence thesis by XTUPLE_0:def 12;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: RELAT_1:148

    (( rng R) /\ Y) c= ((R ~ ) " (R " Y))

    proof

      let y be object;

      assume

       A1: y in (( rng R) /\ Y);

      then y in ( rng R) by XBOOLE_0:def 4;

      then

      consider x be object such that

       A2: [x, y] in R by XTUPLE_0:def 13;

      

       A3: [y, x] in (R ~ ) by A2, Def5;

      y in Y by A1, XBOOLE_0:def 4;

      then x in (R " Y) by A2, Def12;

      hence thesis by A3, Def12;

    end;

    begin

    definition

      let R;

      :: RELAT_1:def15

      attr R is empty-yielding means

      : Def13: ( rng R) c= { {} };

    end

    theorem :: RELAT_1:149

    R is empty-yielding iff for X st X in ( rng R) holds X = {}

    proof

      thus R is empty-yielding implies for X st X in ( rng R) holds X = {} by TARSKI:def 1;

      assume

       A1: for X st X in ( rng R) holds X = {} ;

      let Y be object;

      assume Y in ( rng R);

      then Y = {} by A1;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: RELAT_1:150

    for f,g be Relation, A,B be set st (f | A) = (g | A) & (f | B) = (g | B) holds (f | (A \/ B)) = (g | (A \/ B))

    proof

      let f,g be Relation, A,B be set;

      assume (f | A) = (g | A) & (f | B) = (g | B);

      

      hence (f | (A \/ B)) = ((g | A) \/ (g | B)) by Th72

      .= (g | (A \/ B)) by Th72;

    end;

    theorem :: RELAT_1:151

    for X be set, f,g be Relation st ( dom g) c= X & g c= f holds g c= (f | X)

    proof

      let X be set, f,g be Relation;

      assume ( dom g) c= X & g c= f;

      then (g | ( dom g)) c= (f | X) by Th71;

      hence thesis;

    end;

    theorem :: RELAT_1:152

    for f be Relation, X be set st X misses ( dom f) holds (f | X) = {}

    proof

      let f be Relation, X be set such that

       A1: (X /\ ( dom f)) = {} ;

      

      thus (f | X) = ((f | ( dom f)) | X)

      .= (f | {} qua set) by A1, Th65

      .= {} ;

    end;

    theorem :: RELAT_1:153

    for f,g be Relation, A,B be set st A c= B & (f | B) = (g | B) holds (f | A) = (g | A)

    proof

      let f,g be Relation, A,B be set;

      assume that

       A1: A c= B and

       A2: (f | B) = (g | B);

      

       A3: A = (B /\ A) by A1, XBOOLE_1: 28;

      

      hence (f | A) = ((f | B) | A) by Th65

      .= (g | A) by A2, A3, Th65;

    end;

    theorem :: RELAT_1:154

    (R | ( dom S)) = (R | ( dom (S | ( dom R))))

    proof

      

      thus (R | ( dom S)) = ((R | ( dom R)) | ( dom S))

      .= (R | (( dom S) /\ ( dom R))) by Th65

      .= (R | ( dom (S | ( dom R)))) by Th55;

    end;

    registration

      cluster empty -> empty-yielding for Relation;

      coherence

      proof

        let R be Relation;

        assume R is empty;

        hence ( rng R) c= { {} };

      end;

    end

    registration

      let R be empty-yielding Relation;

      let X be set;

      cluster (R | X) -> empty-yielding;

      coherence

      proof

        ( rng R) c= { {} } & ( rng (R | X)) c= ( rng R) by Def13, Th53, XTUPLE_0: 9;

        hence ( rng (R | X)) c= { {} };

      end;

    end

    theorem :: RELAT_1:155

    (R | X) is non empty-yielding implies R is non empty-yielding;

    definition

      let R be Relation, x be object;

      :: RELAT_1:def16

      func Im (R,x) -> set equals (R .: {x});

      correctness ;

    end

    scheme :: RELAT_1:sch2

    ExtensionalityR { A,B() -> Relation , P[ object, object] } :

A() = B()

      provided

       A1: for a,b be object holds [a, b] in A() iff P[a, b]

       and

       A2: for a,b be object holds [a, b] in B() iff P[a, b];

      let y,z be object;

      thus [y, z] in A() implies [y, z] in B() by A1, A2;

      assume [y, z] in B();

      hence thesis by A1, A2;

    end;

    theorem :: RELAT_1:156

    ( dom (R | (( dom R) \ X))) = (( dom R) \ X)

    proof

      

      thus ( dom (R | (( dom R) \ X))) = (( dom R) /\ (( dom R) \ X)) by Th55

      .= ((( dom R) /\ ( dom R)) \ X) by XBOOLE_1: 49

      .= (( dom R) \ X);

    end;

    theorem :: RELAT_1:157

    (R | X) = (R | (( dom R) /\ X))

    proof

      

      thus (R | X) = ((R | ( dom R)) | X)

      .= (R | (( dom R) /\ X)) by Th65;

    end;

    theorem :: RELAT_1:158

    ( dom [:X, Y:]) c= X

    proof

      let x be object;

      assume x in ( dom [:X, Y:]);

      then ex y be object st [x, y] in [:X, Y:] by XTUPLE_0:def 12;

      hence thesis by ZFMISC_1: 87;

    end;

    theorem :: RELAT_1:159

    ( rng [:X, Y:]) c= Y

    proof

      let x be object;

      assume x in ( rng [:X, Y:]);

      then ex y be object st [y, x] in [:X, Y:] by XTUPLE_0:def 13;

      hence thesis by ZFMISC_1: 87;

    end;

    theorem :: RELAT_1:160

    X <> {} & Y <> {} implies ( dom [:X, Y:]) = X & ( rng [:X, Y:]) = Y

    proof

      assume X <> {} ;

      then

      consider a be object such that

       A1: a in X by XBOOLE_0:def 1;

      assume Y <> {} ;

      then

      consider b be object such that

       A2: b in Y by XBOOLE_0:def 1;

       A3:

      now

        let x be object;

        assume x in X;

        then [x, b] in [:X, Y:] by A2, ZFMISC_1: 87;

        hence ex y be object st [x, y] in [:X, Y:];

      end;

      (ex y be object st [x, y] in [:X, Y:]) implies x in X by ZFMISC_1: 87;

      hence ( dom [:X, Y:]) = X by A3, XTUPLE_0:def 12;

       A4:

      now

        let y be object;

        assume y in Y;

        then [a, y] in [:X, Y:] by A1, ZFMISC_1: 87;

        hence ex x be object st [x, y] in [:X, Y:];

      end;

      (ex x be object st [x, y] in [:X, Y:]) implies y in Y by ZFMISC_1: 87;

      hence thesis by A4, XTUPLE_0:def 13;

    end;

    theorem :: RELAT_1:161

    ( dom R) = {} & ( dom Q) = {} implies R = Q;

    theorem :: RELAT_1:162

    ( rng R) = {} & ( rng Q) = {} implies R = Q;

    theorem :: RELAT_1:163

    ( dom R) = ( dom Q) implies ( dom (S * R)) = ( dom (S * Q))

    proof

      assume

       A1: ( dom R) = ( dom Q);

      

      thus ( dom (S * R)) = (S " ( dom R)) by Th137

      .= ( dom (S * Q)) by A1, Th137;

    end;

    theorem :: RELAT_1:164

    ( rng R) = ( rng Q) implies ( rng (R * S)) = ( rng (Q * S))

    proof

      assume

       A1: ( rng R) = ( rng Q);

      

      thus ( rng (R * S)) = (S .: ( rng R)) by Th119

      .= ( rng (Q * S)) by A1, Th119;

    end;

    definition

      let R be Relation, x be object;

      :: RELAT_1:def17

      func Coim (R,x) -> set equals (R " {x});

      coherence ;

    end

    registration

      let R be trivial Relation;

      cluster ( dom R) -> trivial;

      coherence

      proof

        let x,y be object;

        assume x in ( dom R);

        then

        consider a be object such that

         A1: [x, a] in R by XTUPLE_0:def 12;

        assume y in ( dom R);

        then

        consider b be object such that

         A2: [y, b] in R by XTUPLE_0:def 12;

         [x, a] = [y, b] by A1, A2, ZFMISC_1:def 10;

        hence thesis by XTUPLE_0: 1;

      end;

    end

    registration

      let R be trivial Relation;

      cluster ( rng R) -> trivial;

      coherence

      proof

        let x,y be object;

        assume x in ( rng R);

        then

        consider a be object such that

         A1: [a, x] in R by XTUPLE_0:def 13;

        assume y in ( rng R);

        then

        consider b be object such that

         A2: [b, y] in R by XTUPLE_0:def 13;

         [a, x] = [b, y] by A1, A2, ZFMISC_1:def 10;

        hence thesis by XTUPLE_0: 1;

      end;

    end

    theorem :: RELAT_1:165

    ( rng R) c= ( dom (S | X)) implies (R * (S | X)) = (R * S)

    proof

      assume

       A1: ( rng R) c= ( dom (S | X));

      let a, b;

      (R * (S | X)) c= (R * S) by Th23, Th53;

      hence [a, b] in (R * (S | X)) implies [a, b] in (R * S);

      assume [a, b] in (R * S);

      then

      consider c such that

       A2: [a, c] in R and

       A3: [c, b] in S by Def6;

      c in ( rng R) by A2, XTUPLE_0:def 13;

      then c in X by A1, Th51;

      then [c, b] in (S | X) by A3, Def9;

      hence thesis by A2, Def6;

    end;

    theorem :: RELAT_1:166

    (Q | A) = (R | A) implies (Q .: A) = (R .: A)

    proof

      assume (Q | A) = (R | A);

      

      hence (Q .: A) = ((R | A) .: A) by Th121

      .= (R .: A) by Th121;

    end;

    definition

      let X, R;

      :: RELAT_1:def18

      attr R is X -defined means

      : Def16: ( dom R) c= X;

      :: RELAT_1:def19

      attr R is X -valued means

      : Def17: ( rng R) c= X;

    end

    

     Lm1: {} is X -definedY -valued

    proof

      thus ( dom {} ) c= X & ( rng {} ) c= Y;

    end;

    registration

      let X, Y;

      cluster X -definedY -valued for Relation;

      existence

      proof

        take {} ;

        thus thesis by Lm1;

      end;

    end

    theorem :: RELAT_1:167

    for D be set, R be D -valued Relation holds for y be object st y in ( rng R) holds y in D

    proof

      let D be set, R be D -valued Relation;

      ( rng R) c= D by Def17;

      hence thesis;

    end;

    registration

      let X, A;

      let R be A -valued Relation;

      cluster (R | X) -> A -valued;

      coherence

      proof

        ( rng (R | X)) c= ( rng R) & ( rng R) c= A by Def17, Th53, XTUPLE_0: 9;

        hence ( rng (R | X)) c= A;

      end;

    end

    registration

      let X, A;

      let R be A -defined Relation;

      cluster (R | X) -> A -definedX -defined;

      coherence

      proof

        ( dom (R | X)) c= ( dom R) & ( dom R) c= A by Def16, Th51;

        hence ( dom (R | X)) c= A;

        thus ( dom (R | X)) c= X by Th51;

      end;

    end

    registration

      let X;

      cluster ( id X) -> X -definedX -valued;

      coherence ;

    end

    registration

      let A be set;

      let R be A -valued Relation, S be Relation;

      cluster (S * R) -> A -valued;

      coherence

      proof

        ( rng R) c= A & ( rng (S * R)) c= ( rng R) by Def17, Th20;

        hence ( rng (S * R)) c= A;

      end;

    end

    registration

      let A be set;

      let R be A -defined Relation, S be Relation;

      cluster (R * S) -> A -defined;

      coherence

      proof

        ( dom R) c= A & ( dom (R * S)) c= ( dom R) by Def16, Th19;

        hence ( dom (R * S)) c= A;

      end;

    end

    theorem :: RELAT_1:168

    x in X implies ( Im ( [:X, Y:],x)) = Y

    proof

      assume

       A1: x in X;

      thus ( Im ( [:X, Y:],x)) c= Y

      proof

        let y be object;

        assume y in ( Im ( [:X, Y:],x));

        then ex z st [z, y] in [:X, Y:] & z in {x} by Def11;

        hence y in Y by ZFMISC_1: 87;

      end;

      let y be object;

      assume y in Y;

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

    end;

    theorem :: RELAT_1:169

    

     Th159: [x, y] in R iff y in ( Im (R,x))

    proof

      thus [x, y] in R implies y in ( Im (R,x))

      proof

        x in {x} by TARSKI:def 1;

        hence thesis by Def11;

      end;

      assume y in ( Im (R,x));

      then ex z st [z, y] in R & z in {x} by Def11;

      hence [x, y] in R by TARSKI:def 1;

    end;

    theorem :: RELAT_1:170

    x in ( dom R) iff ( Im (R,x)) <> {}

    proof

      thus x in ( dom R) implies ( Im (R,x)) <> {}

      proof

        assume x in ( dom R);

        then ex y be object st [x, y] in R by XTUPLE_0:def 12;

        hence ( Im (R,x)) <> {} by Th159;

      end;

      assume ( Im (R,x)) <> {} ;

      then

      consider y be object such that

       A1: y in ( Im (R,x)) by XBOOLE_0:def 1;

       [x, y] in R by A1, Th159;

      hence x in ( dom R) by XTUPLE_0:def 12;

    end;

    theorem :: RELAT_1:171

     {} is X -definedY -valued by Lm1;

    registration

      cluster empty -> non-empty for Relation;

      coherence ;

    end

    registration

      let X be set, R be X -defined Relation;

      cluster -> X -defined for Subset of R;

      coherence

      proof

        let S be Subset of R;

        

         A1: ( dom R) c= X by Def16;

        ( dom S) c= ( dom R) by XTUPLE_0: 8;

        hence ( dom S) c= X by A1;

      end;

    end

    registration

      let X be set, R be X -valued Relation;

      cluster -> X -valued for Subset of R;

      coherence

      proof

        let S be Subset of R;

        

         A1: ( rng R) c= X by Def17;

        ( rng S) c= ( rng R) by XTUPLE_0: 9;

        hence ( rng S) c= X by A1;

      end;

    end

    theorem :: RELAT_1:172

    X misses Y implies ((R | X) | Y) = {}

    proof

      assume X misses Y;

      

      hence ((R | X) | Y) = (R | {} qua set) by Th65

      .= {} ;

    end;

    theorem :: RELAT_1:173

    ( field { [x, x]}) = {x}

    proof

      

      thus ( field { [x, x]}) = {x, x} by Th11

      .= {x} by ENUMSET1: 29;

    end;

    registration

      let X;

      let R be X -defined Relation;

      reduce (R | X) to R;

      reducibility

      proof

        ( dom R) c= X by Def16;

        hence (R | X) = R by Th62;

      end;

    end

    registration

      let Y;

      let R be Y -valued Relation;

      reduce (Y |` R) to R;

      reducibility

      proof

        ( rng R) c= Y by Def17;

        hence (Y |` R) = R by Th88;

      end;

    end

    theorem :: RELAT_1:174

    for R be X -defined Relation holds R = (R | X);

    theorem :: RELAT_1:175

    for S be Relation, R be X -defined Relation st R c= S holds R c= (S | X)

    proof

      let S be Relation, R be X -defined Relation;

      R = (R | X);

      hence thesis by Th70;

    end;

    theorem :: RELAT_1:176

    

     Th166: ( dom R) c= X implies (R \ (R | A)) = (R | (X \ A))

    proof

      assume ( dom R) c= X;

      

      hence (R \ (R | A)) = ((R | X) \ (R | A)) by Th62

      .= (R | (X \ A)) by Th74;

    end;

    theorem :: RELAT_1:177

    

     Th167: ( dom (R \ (R | A))) = (( dom R) \ A)

    proof

      (R \ (R | A)) = (R | (( dom R) \ A)) by Th166;

      

      hence ( dom (R \ (R | A))) = (( dom R) /\ (( dom R) \ A)) by Th55

      .= ((( dom R) /\ ( dom R)) \ A) by XBOOLE_1: 49

      .= (( dom R) \ A);

    end;

    theorem :: RELAT_1:178

    (( dom R) \ ( dom (R | A))) = ( dom (R \ (R | A)))

    proof

      

      thus (( dom R) \ ( dom (R | A))) = (( dom R) \ (A /\ ( dom R))) by Th55

      .= (( dom R) \ A) by XBOOLE_1: 47

      .= ( dom (R \ (R | A))) by Th167;

    end;

    theorem :: RELAT_1:179

    

     Th169: ( dom R) misses ( dom S) implies R misses S

    proof

      assume

       A1: ( dom R) misses ( dom S);

      assume R meets S;

      then

      consider x be object such that

       A2: x in R and

       A3: x in S by XBOOLE_0: 3;

      consider y, z 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;

    end;

    theorem :: RELAT_1:180

    ( rng R) misses ( rng S) implies R misses S

    proof

      assume

       A1: ( rng R) misses ( rng S);

      assume R meets S;

      then

      consider x be object such that

       A2: x in R and

       A3: x in S by XBOOLE_0: 3;

      consider y, z 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;

    end;

    theorem :: RELAT_1:181

    X c= Y implies ((R \ (R | Y)) | X) = {}

    proof

      assume

       A1: X c= Y;

      (( dom R) /\ X) c= X by XBOOLE_1: 17;

      then

       A2: (( dom R) /\ X) c= Y by A1;

      ( dom (R \ (R | Y))) = (( dom R) \ Y) by Th167;

      

      then ( dom ((R \ (R | Y)) | X)) = ((( dom R) \ Y) /\ X) by Th55

      .= ((( dom R) /\ X) \ Y) by XBOOLE_1: 49

      .= {} by A2, XBOOLE_1: 37;

      hence ((R \ (R | Y)) | X) = {} ;

    end;

    theorem :: RELAT_1:182

    X c= Y implies for R be X -defined Relation holds R is Y -defined

    proof

      assume

       A1: X c= Y;

      let R be X -defined Relation;

      ( dom R) c= X by Def16;

      hence ( dom R) c= Y by A1;

    end;

    theorem :: RELAT_1:183

    X c= Y implies for R be X -valued Relation holds R is Y -valued

    proof

      assume

       A1: X c= Y;

      let R be X -valued Relation;

      ( rng R) c= X by Def17;

      hence ( rng R) c= Y by A1;

    end;

    theorem :: RELAT_1:184

    R c= S iff R c= (S | ( dom R))

    proof

      thus R c= S implies R c= (S | ( dom R))

      proof

        assume R c= S;

        then (R | ( dom R)) c= (S | ( dom R)) by Th70;

        hence thesis;

      end;

      thus thesis by Def9;

    end;

    theorem :: RELAT_1:185

    

     Th175: for R be X -definedY -valued Relation holds R c= [:X, Y:]

    proof

      let R be X -definedY -valued Relation;

      

       A1: R c= [:( dom R), ( rng R):] by Th1;

      ( dom R) c= X & ( rng R) c= Y by Def16, Def17;

      then [:( dom R), ( rng R):] c= [:X, Y:] by ZFMISC_1: 96;

      hence thesis by A1;

    end;

    theorem :: RELAT_1:186

    ( dom (X |` R)) c= ( dom R) by Th80, XTUPLE_0: 8;

    registration

      let A, X;

      let R be A -defined Relation;

      cluster (X |` R) -> A -defined;

      coherence

      proof

        ( dom (X |` R)) c= ( dom R) & ( dom R) c= A by Def16, Th80, XTUPLE_0: 8;

        hence ( dom (X |` R)) c= A;

      end;

    end

    registration

      let X, A;

      let R be A -valued Relation;

      cluster (X |` R) -> A -valuedX -valued;

      coherence

      proof

        ( rng (X |` R)) c= ( rng R) & ( rng R) c= A by Def17, Th80, XTUPLE_0: 9;

        hence ( rng (X |` R)) c= A;

        thus ( rng (X |` R)) c= X by Th78;

      end;

    end

    registration

      let X be empty set;

      cluster -> empty for X -defined Relation;

      coherence

      proof

        let R be X -defined Relation;

        ( dom R) c= X by Def16;

        hence thesis by XBOOLE_1: 3;

      end;

      cluster -> empty for X -valued Relation;

      coherence

      proof

        let R be X -valued Relation;

        ( rng R) c= X by Def17;

        hence thesis by XBOOLE_1: 3;

      end;

    end

    theorem :: RELAT_1:187

    for X,Y be set, P,R be Relation st X misses Y holds (P | X) misses (R | Y)

    proof

      let X,Y be set, P,R be Relation;

      assume

       A1: X misses Y;

      

       A2: ( dom (P | X)) = (( dom P) /\ X) by Th55;

      ( dom (R | Y)) = (( dom R) /\ Y) by Th55;

      

      then (( dom (P | X)) /\ ( dom (R | Y))) = (( dom P) /\ (X /\ (( dom R) /\ Y))) by A2, XBOOLE_1: 16

      .= (( dom P) /\ ((X /\ Y) /\ ( dom R))) by XBOOLE_1: 16

      .= {} by A1;

      then ( dom (P | X)) misses ( dom (R | Y));

      hence thesis by Th169;

    end;

    theorem :: RELAT_1:188

    for Y be set, R be Relation holds (Y |` R) c= (R | (R " Y))

    proof

      let Y be set, R be Relation;

      let a,b be object;

      assume

       A1: [a, b] in (Y |` R);

      then

       A2: b in Y by Def10;

      

       A3: [a, b] in R by A1, Def10;

      then a in (R " Y) by A2, Def12;

      hence thesis by A3, Def9;

    end;

    theorem :: RELAT_1:189

    for f be Relation, x, y st ( dom f) = {x} & ( rng f) = {y} holds f = { [x, y]}

    proof

      let f be Relation, x, y;

      

       A1: f c= [:( dom f), ( rng f):] by Th1;

      assume

       A2: ( dom f) = {x} & ( rng f) = {y};

      x in ( dom f) by A2, TARSKI:def 1;

      then

      consider yy be object such that

       A3: [x, yy] in f by XTUPLE_0:def 12;

      yy in ( rng f) by A3, XTUPLE_0:def 13;

      then [x, y] in f by A3, A2, TARSKI:def 1;

      hence thesis by A1, A2, ZFMISC_1: 29, ZFMISC_1: 31;

    end;

    registration

      let X, Y;

      sethood of X -definedY -valued Relation

      proof

        take ( bool [:X, Y:]);

        let R be X -definedY -valued Relation;

        R c= [:X, Y:] by Th175;

        hence thesis by ZFMISC_1:def 1;

      end;

    end