partfun2.miz



    begin

    reserve x,y,X,Y for set;

    reserve C,D,E for non empty set;

    reserve SC for Subset of C;

    reserve SD for Subset of D;

    reserve SE for Subset of E;

    reserve c,c1,c2 for Element of C;

    reserve d,d1,d2 for Element of D;

    reserve e for Element of E;

    reserve f,f1,g for PartFunc of C, D;

    reserve t for PartFunc of D, C;

    reserve s for PartFunc of D, E;

    reserve h for PartFunc of C, E;

    reserve F for PartFunc of D, D;

    theorem :: PARTFUN2:1

    

     Th1: ( dom f) = ( dom g) & (for c st c in ( dom f) holds (f /. c) = (g /. c)) implies f = g

    proof

      assume that

       A1: ( dom f) = ( dom g) and

       A2: for c st c in ( dom f) holds (f /. c) = (g /. c);

      now

        let x be object;

        assume

         A3: x in ( dom f);

        then

        reconsider y = x as Element of C;

        (f /. y) = (g /. y) by A2, A3;

        then (f qua Function . y) = (g /. y) by A3, PARTFUN1:def 6;

        hence (f qua Function . x) = (g qua Function . x) by A1, A3, PARTFUN1:def 6;

      end;

      hence thesis by A1;

    end;

    theorem :: PARTFUN2:2

    

     Th2: y in ( rng f) iff ex c st c in ( dom f) & y = (f /. c)

    proof

      thus y in ( rng f) implies ex c st c in ( dom f) & y = (f /. c)

      proof

        assume y in ( rng f);

        then

        consider x be object such that

         A1: x in ( dom f) and

         A2: y = (f qua Function . x) by FUNCT_1:def 3;

        reconsider x as Element of C by A1;

        take x;

        thus thesis by A1, A2, PARTFUN1:def 6;

      end;

      given c such that

       A3: c in ( dom f) and

       A4: y = (f /. c);

      (f qua Function . c) in ( rng f) by A3, FUNCT_1:def 3;

      hence thesis by A3, A4, PARTFUN1:def 6;

    end;

    theorem :: PARTFUN2:3

    

     Th3: h = (s * f) iff (for c holds c in ( dom h) iff c in ( dom f) & (f /. c) in ( dom s)) & for c st c in ( dom h) holds (h /. c) = (s /. (f /. c))

    proof

      thus h = (s * f) implies (for c holds c in ( dom h) iff c in ( dom f) & (f /. c) in ( dom s)) & for c st c in ( dom h) holds (h /. c) = (s /. (f /. c))

      proof

        assume

         A1: h = (s * f);

         A2:

        now

          let c;

          thus c in ( dom h) implies c in ( dom f) & (f /. c) in ( dom s)

          proof

            assume c in ( dom h);

            then c in ( dom f) & (f qua Function . c) in ( dom s) by A1, FUNCT_1: 11;

            hence thesis by PARTFUN1:def 6;

          end;

          assume that

           A3: c in ( dom f) and

           A4: (f /. c) in ( dom s);

          (f qua Function . c) in ( dom s) by A3, A4, PARTFUN1:def 6;

          hence c in ( dom h) by A1, A3, FUNCT_1: 11;

        end;

        hence for c holds c in ( dom h) iff c in ( dom f) & (f /. c) in ( dom s);

        let c;

        assume

         A5: c in ( dom h);

        then (h qua Function . c) = (s qua Function . (f qua Function . c)) by A1, FUNCT_1: 12;

        then

         A6: (h /. c) = (s qua Function . (f qua Function . c)) by A5, PARTFUN1:def 6;

        c in ( dom f) by A2, A5;

        then

         A7: (h /. c) = (s qua Function . (f /. c)) by A6, PARTFUN1:def 6;

        (f /. c) in ( dom s) by A2, A5;

        hence thesis by A7, PARTFUN1:def 6;

      end;

      assume that

       A8: for c holds c in ( dom h) iff c in ( dom f) & (f /. c) in ( dom s) and

       A9: for c st c in ( dom h) holds (h /. c) = (s /. (f /. c));

       A10:

      now

        let x be object;

        thus x in ( dom h) implies x in ( dom f) & (f qua Function . x) in ( dom s)

        proof

          assume

           A11: x in ( dom h);

          then

          reconsider y = x as Element of C;

          y in ( dom f) & (f /. y) in ( dom s) by A8, A11;

          hence thesis by PARTFUN1:def 6;

        end;

        thus x in ( dom f) & (f qua Function . x) in ( dom s) implies x in ( dom h)

        proof

          assume that

           A12: x in ( dom f) and

           A13: (f qua Function . x) in ( dom s);

          reconsider y = x as Element of C by A12;

          (f /. y) in ( dom s) by A12, A13, PARTFUN1:def 6;

          hence thesis by A8, A12;

        end;

      end;

      now

        let x be object;

        assume

         A14: x in ( dom h);

        then

        reconsider y = x as Element of C;

        (h /. y) = (s /. (f /. y)) by A9, A14;

        then

         A15: (h qua Function . y) = (s /. (f /. y)) by A14, PARTFUN1:def 6;

        (f /. y) in ( dom s) by A8, A14;

        then

         A16: (h qua Function . x) = (s qua Function . (f /. y)) by A15, PARTFUN1:def 6;

        y in ( dom f) by A8, A14;

        hence (h qua Function . x) = (s qua Function . (f qua Function . x)) by A16, PARTFUN1:def 6;

      end;

      hence thesis by A10, FUNCT_1: 10;

    end;

    theorem :: PARTFUN2:4

    

     Th4: c in ( dom f) & (f /. c) in ( dom s) implies ((s * f) /. c) = (s /. (f /. c))

    proof

      assume c in ( dom f) & (f /. c) in ( dom s);

      then c in ( dom (s * f)) by Th3;

      hence thesis by Th3;

    end;

    theorem :: PARTFUN2:5

    ( rng f) c= ( dom s) & c in ( dom f) implies ((s * f) /. c) = (s /. (f /. c))

    proof

      assume that

       A1: ( rng f) c= ( dom s) and

       A2: c in ( dom f);

      (f /. c) in ( rng f) by A2, Th2;

      hence thesis by A1, A2, Th4;

    end;

    definition

      let D;

      let SD;

      :: original: id

      redefine

      func id SD -> PartFunc of D, D ;

      coherence

      proof

        ( dom ( id SD)) = SD & ( rng ( id SD)) = SD by RELAT_1: 45;

        hence thesis by RELSET_1: 4;

      end;

    end

    theorem :: PARTFUN2:6

    

     Th6: F = ( id SD) iff ( dom F) = SD & for d st d in SD holds (F /. d) = d

    proof

      thus F = ( id SD) implies ( dom F) = SD & for d st d in SD holds (F /. d) = d

      proof

        assume

         A1: F = ( id SD);

        hence

         A2: ( dom F) = SD by RELAT_1: 45;

        let d;

        assume

         A3: d in SD;

        then (F qua Function . d) = d by A1, FUNCT_1: 18;

        hence thesis by A2, A3, PARTFUN1:def 6;

      end;

      assume that

       A4: ( dom F) = SD and

       A5: for d st d in SD holds (F /. d) = d;

      now

        let x be object;

        assume

         A6: x in SD;

        then

        reconsider x1 = x as Element of D;

        (F /. x1) = x1 by A5, A6;

        hence (F qua Function . x) = x by A4, A6, PARTFUN1:def 6;

      end;

      hence thesis by A4, FUNCT_1: 17;

    end;

    theorem :: PARTFUN2:7

    d in (( dom F) /\ SD) implies (F /. d) = ((F * ( id SD)) /. d)

    proof

      assume

       A1: d in (( dom F) /\ SD);

      then

       A2: d in ( dom F) by XBOOLE_0:def 4;

      (F qua Function . d) = ((F * ( id SD)) qua Function . d) by A1, FUNCT_1: 20;

      then

       A3: (F /. d) = ((F * ( id SD)) qua Function . d) by A2, PARTFUN1:def 6;

      

       A4: d in SD by A1, XBOOLE_0:def 4;

      then

       A5: d in ( dom ( id SD)) by RELAT_1: 45;

      (( id SD) /. d) in ( dom F) by A2, A4, Th6;

      then d in ( dom (F * ( id SD))) by A5, Th3;

      hence thesis by A3, PARTFUN1:def 6;

    end;

    theorem :: PARTFUN2:8

    d in ( dom (( id SD) * F)) iff d in ( dom F) & (F /. d) in SD

    proof

      thus d in ( dom (( id SD) * F)) implies d in ( dom F) & (F /. d) in SD

      proof

        assume

         A1: d in ( dom (( id SD) * F));

        then (F /. d) in ( dom ( id SD)) by Th3;

        hence thesis by A1, Th3, RELAT_1: 45;

      end;

      assume that

       A2: d in ( dom F) and

       A3: (F /. d) in SD;

      (F /. d) in ( dom ( id SD)) by A3, RELAT_1: 45;

      hence thesis by A2, Th3;

    end;

    theorem :: PARTFUN2:9

    (for c1, c2 st c1 in ( dom f) & c2 in ( dom f) & (f /. c1) = (f /. c2) holds c1 = c2) implies f is one-to-one

    proof

      assume

       A1: for c1, c2 st c1 in ( dom f) & c2 in ( dom f) & (f /. c1) = (f /. c2) holds c1 = c2;

      now

        let x,y be object;

        assume that

         A2: x in ( dom f) and

         A3: y in ( dom f) and

         A4: (f qua Function . x) = (f qua Function . y);

        reconsider y1 = y as Element of C by A3;

        reconsider x1 = x as Element of C by A2;

        (f /. x1) = (f qua Function . y1) by A2, A4, PARTFUN1:def 6;

        then (f /. x1) = (f /. y1) by A3, PARTFUN1:def 6;

        hence x = y by A1, A2, A3;

      end;

      hence thesis;

    end;

    theorem :: PARTFUN2:10

    f is one-to-one & x in ( dom f) & y in ( dom f) & (f /. x) = (f /. y) implies x = y

    proof

      assume that

       A1: f is one-to-one and

       A2: x in ( dom f) and

       A3: y in ( dom f);

      assume (f /. x) = (f /. y);

      

      then (f . x) = (f /. y) by A2, PARTFUN1:def 6

      .= (f . y) by A3, PARTFUN1:def 6;

      hence thesis by A1, A2, A3;

    end;

    definition

      let X, Y;

      let f be one-to-one PartFunc of X, Y;

      :: original: "

      redefine

      func f " -> PartFunc of Y, X ;

      coherence by PARTFUN1: 9;

    end

    theorem :: PARTFUN2:11

    

     Th11: for f be one-to-one PartFunc of C, D holds for g be PartFunc of D, C holds g = (f " ) iff ( dom g) = ( rng f) & for d, c holds d in ( rng f) & c = (g /. d) iff c in ( dom f) & d = (f /. c)

    proof

      let f be one-to-one PartFunc of C, D;

      let g be PartFunc of D, C;

      thus g = (f " ) implies ( dom g) = ( rng f) & for d, c holds d in ( rng f) & c = (g /. d) iff c in ( dom f) & d = (f /. c)

      proof

        assume

         A1: g = (f " );

        hence ( dom g) = ( rng f) by FUNCT_1: 32;

        let d, c;

        

         A2: ( dom g) = ( rng f) by A1, FUNCT_1: 32;

        thus d in ( rng f) & c = (g /. d) implies c in ( dom f) & d = (f /. c)

        proof

          assume that

           A3: d in ( rng f) and

           A4: c = (g /. d);

          c = (g qua Function . d) by A2, A3, A4, PARTFUN1:def 6;

          then c in ( dom f) & d = (f qua Function . c) by A1, A3, FUNCT_1: 32;

          hence thesis by PARTFUN1:def 6;

        end;

        assume that

         A5: c in ( dom f) and

         A6: d = (f /. c);

        d = (f qua Function . c) by A5, A6, PARTFUN1:def 6;

        then d in ( rng f) & c = (g qua Function . d) by A1, A5, FUNCT_1: 32;

        hence thesis by A2, PARTFUN1:def 6;

      end;

      assume that

       A7: ( dom g) = ( rng f) and

       A8: for d, c holds d in ( rng f) & c = (g /. d) iff c in ( dom f) & d = (f /. c) and

       A9: g <> (f " );

      now

        per cases by A9, Th1;

          suppose ( dom (f " )) <> ( dom g);

          hence contradiction by A7, FUNCT_1: 33;

        end;

          suppose ex d st d in ( dom (f " )) & ((f " ) /. d) <> (g /. d);

          then

          consider d such that

           A10: d in ( dom (f " )) and

           A11: ((f " ) /. d) <> (g /. d);

          ((f " ) /. d) in ( rng (f " )) by A10, Th2;

          then

           A12: ((f " ) /. d) in ( dom f) by FUNCT_1: 33;

          d in ( rng f) by A10, FUNCT_1: 33;

          then d = (f qua Function . ((f " ) qua Function . d)) by FUNCT_1: 35;

          then d = (f qua Function . ((f " ) /. d)) by A10, PARTFUN1:def 6;

          then d = (f /. ((f " ) /. d)) by A12, PARTFUN1:def 6;

          hence contradiction by A8, A11, A12;

        end;

      end;

      hence contradiction;

    end;

    theorem :: PARTFUN2:12

    for f be one-to-one PartFunc of C, D st c in ( dom f) holds c = ((f " ) /. (f /. c)) & c = (((f " ) * f) /. c)

    proof

      let f be one-to-one PartFunc of C, D;

      assume

       A1: c in ( dom f);

      hence

       A2: c = ((f " ) /. (f /. c)) by Th11;

      (f " ) = (f " );

      then (f /. c) in ( rng f) by A1, Th11;

      then (f /. c) in ( dom (f " )) by FUNCT_1: 33;

      hence thesis by A1, A2, Th4;

    end;

    theorem :: PARTFUN2:13

    for f be one-to-one PartFunc of C, D st d in ( rng f) holds d = (f /. ((f " ) /. d)) & d = ((f * (f " )) /. d)

    proof

      let f be one-to-one PartFunc of C, D;

      assume

       A1: d in ( rng f);

      then d = ((f * (f " )) qua Function . d) & d in ( dom (f * (f " ))) by FUNCT_1: 35, FUNCT_1: 37;

      hence thesis by A1, Th11, PARTFUN1:def 6;

    end;

    theorem :: PARTFUN2:14

    f is one-to-one & ( dom f) = ( rng t) & ( rng f) = ( dom t) & (for c, d st c in ( dom f) & d in ( dom t) holds (f /. c) = d iff (t /. d) = c) implies t = (f " )

    proof

      assume that

       A1: f is one-to-one & ( dom f) = ( rng t) & ( rng f) = ( dom t) and

       A2: for c, d st c in ( dom f) & d in ( dom t) holds (f /. c) = d iff (t /. d) = c;

      now

        let x,y be object;

        assume that

         A3: x in ( dom f) and

         A4: y in ( dom t);

        reconsider y1 = y as Element of D by A4;

        reconsider x1 = x as Element of C by A3;

        thus (f qua Function . x) = y implies (t qua Function . y) = x

        proof

          assume (f qua Function . x) = y;

          then (f /. x1) = y1 by A3, PARTFUN1:def 6;

          then (t /. y1) = x1 by A2, A3, A4;

          hence thesis by A4, PARTFUN1:def 6;

        end;

        assume (t qua Function . y) = x;

        then (t /. y1) = x1 by A4, PARTFUN1:def 6;

        then (f /. x1) = y1 by A2, A3, A4;

        hence (f qua Function . x) = y by A3, PARTFUN1:def 6;

      end;

      hence thesis by A1, FUNCT_1: 38;

    end;

    theorem :: PARTFUN2:15

    

     Th15: g = (f | X) iff ( dom g) = (( dom f) /\ X) & for c st c in ( dom g) holds (g /. c) = (f /. c)

    proof

      thus g = (f | X) implies ( dom g) = (( dom f) /\ X) & for c st c in ( dom g) holds (g /. c) = (f /. c)

      proof

        assume

         A1: g = (f | X);

        hence ( dom g) = (( dom f) /\ X) by RELAT_1: 61;

        let c;

        assume

         A2: c in ( dom g);

        then (g qua Function . c) = (f qua Function . c) by A1, FUNCT_1: 47;

        then

         A3: (g /. c) = (f qua Function . c) by A2, PARTFUN1:def 6;

        ( dom g) = (( dom f) /\ X) by A1, RELAT_1: 61;

        then c in ( dom f) by A2, XBOOLE_0:def 4;

        hence thesis by A3, PARTFUN1:def 6;

      end;

      assume that

       A4: ( dom g) = (( dom f) /\ X) and

       A5: for c st c in ( dom g) holds (g /. c) = (f /. c);

      now

        let x be object;

        assume

         A6: x in ( dom g);

        then

        reconsider y = x as Element of C;

        (g /. y) = (f /. y) by A5, A6;

        then

         A7: (g qua Function . y) = (f /. y) by A6, PARTFUN1:def 6;

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

        hence (g qua Function . x) = (f qua Function . x) by A7, PARTFUN1:def 6;

      end;

      hence thesis by A4, FUNCT_1: 46;

    end;

    theorem :: PARTFUN2:16

    

     Th16: c in (( dom f) /\ X) implies ((f | X) /. c) = (f /. c)

    proof

      assume c in (( dom f) /\ X);

      then c in ( dom (f | X)) by RELAT_1: 61;

      hence thesis by Th15;

    end;

    theorem :: PARTFUN2:17

    c in ( dom f) & c in X implies ((f | X) /. c) = (f /. c)

    proof

      assume c in ( dom f) & c in X;

      then c in (( dom f) /\ X) by XBOOLE_0:def 4;

      hence thesis by Th16;

    end;

    theorem :: PARTFUN2:18

    c in ( dom f) & c in X implies (f /. c) in ( rng (f | X))

    proof

      assume that

       A1: c in ( dom f) and

       A2: c in X;

      (f qua Function . c) in ( rng (f | X)) by A1, A2, FUNCT_1: 50;

      hence thesis by A1, PARTFUN1:def 6;

    end;

    definition

      let C, D;

      let X, f;

      :: original: |`

      redefine

      func X |` f -> PartFunc of C, D ;

      coherence by PARTFUN1: 13;

    end

    theorem :: PARTFUN2:19

    

     Th19: g = (X |` f) iff (for c holds c in ( dom g) iff c in ( dom f) & (f /. c) in X) & for c st c in ( dom g) holds (g /. c) = (f /. c)

    proof

      thus g = (X |` f) implies (for c holds c in ( dom g) iff c in ( dom f) & (f /. c) in X) & for c st c in ( dom g) holds (g /. c) = (f /. c)

      proof

        assume

         A1: g = (X |` f);

        now

          let c;

          thus c in ( dom g) implies c in ( dom f) & (f /. c) in X

          proof

            assume c in ( dom g);

            then c in ( dom f) & (f qua Function . c) in X by A1, FUNCT_1: 54;

            hence thesis by PARTFUN1:def 6;

          end;

          assume that

           A2: c in ( dom f) and

           A3: (f /. c) in X;

          (f qua Function . c) in X by A2, A3, PARTFUN1:def 6;

          hence c in ( dom g) by A1, A2, FUNCT_1: 54;

        end;

        hence for c holds c in ( dom g) iff c in ( dom f) & (f /. c) in X;

        let c;

        assume

         A4: c in ( dom g);

        then (g qua Function . c) = (f qua Function . c) by A1, FUNCT_1: 55;

        then

         A5: (g /. c) = (f qua Function . c) by A4, PARTFUN1:def 6;

        c in ( dom f) by A1, A4, FUNCT_1: 54;

        hence thesis by A5, PARTFUN1:def 6;

      end;

      assume that

       A6: for c holds c in ( dom g) iff c in ( dom f) & (f /. c) in X and

       A7: for c st c in ( dom g) holds (g /. c) = (f /. c);

       A8:

      now

        let x be object;

        thus x in ( dom g) implies x in ( dom f) & (f qua Function . x) in X

        proof

          assume

           A9: x in ( dom g);

          then

          reconsider x1 = x as Element of C;

          x1 in ( dom f) & (f /. x1) in X by A6, A9;

          hence thesis by PARTFUN1:def 6;

        end;

        assume that

         A10: x in ( dom f) and

         A11: (f qua Function . x) in X;

        reconsider x1 = x as Element of C by A10;

        (f /. x1) in X by A10, A11, PARTFUN1:def 6;

        hence x in ( dom g) by A6, A10;

      end;

      now

        let x be object;

        assume

         A12: x in ( dom g);

        then

        reconsider x1 = x as Element of C;

        (g /. x1) = (f /. x1) by A7, A12;

        then

         A13: (g qua Function . x1) = (f /. x1) by A12, PARTFUN1:def 6;

        x1 in ( dom f) by A6, A12;

        hence (g qua Function . x) = (f qua Function . x) by A13, PARTFUN1:def 6;

      end;

      hence thesis by A8, FUNCT_1: 53;

    end;

    theorem :: PARTFUN2:20

    c in ( dom (X |` f)) iff c in ( dom f) & (f /. c) in X by Th19;

    theorem :: PARTFUN2:21

    c in ( dom (X |` f)) implies ((X |` f) /. c) = (f /. c) by Th19;

    theorem :: PARTFUN2:22

    

     Th22: SD = (f .: X) iff for d holds d in SD iff ex c st c in ( dom f) & c in X & d = (f /. c)

    proof

      thus SD = (f .: X) implies for d holds d in SD iff ex c st c in ( dom f) & c in X & d = (f /. c)

      proof

        assume

         A1: SD = (f .: X);

        let d;

        thus d in SD implies ex c st c in ( dom f) & c in X & d = (f /. c)

        proof

          assume d in SD;

          then

          consider x be object such that

           A2: x in ( dom f) and

           A3: x in X and

           A4: d = (f qua Function . x) by A1, FUNCT_1:def 6;

          reconsider x as Element of C by A2;

          take x;

          thus x in ( dom f) & x in X by A2, A3;

          thus thesis by A2, A4, PARTFUN1:def 6;

        end;

        given c such that

         A5: c in ( dom f) and

         A6: c in X & d = (f /. c);

        (f /. c) = (f qua Function . c) by A5, PARTFUN1:def 6;

        hence thesis by A1, A5, A6, FUNCT_1:def 6;

      end;

      assume that

       A7: for d holds d in SD iff ex c st c in ( dom f) & c in X & d = (f /. c) and

       A8: SD <> (f .: X);

      consider x be object such that

       A9: not (x in SD iff x in (f .: X)) by A8, TARSKI: 2;

      now

        per cases by A9;

          suppose

           A10: x in SD & not x in (f .: X);

          then

          reconsider x as Element of D;

          consider c such that

           A11: c in ( dom f) and

           A12: c in X and

           A13: x = (f /. c) by A7, A10;

          x = (f qua Function . c) by A11, A13, PARTFUN1:def 6;

          hence contradiction by A10, A11, A12, FUNCT_1:def 6;

        end;

          suppose

           A14: x in (f .: X) & not x in SD;

          then

          consider y be object such that

           A15: y in ( dom f) and

           A16: y in X and

           A17: x = (f qua Function . y) by FUNCT_1:def 6;

          reconsider y as Element of C by A15;

          x = (f /. y) by A15, A17, PARTFUN1:def 6;

          hence contradiction by A7, A14, A15, A16;

        end;

      end;

      hence contradiction;

    end;

    theorem :: PARTFUN2:23

    d in (f qua Relation of C, D .: X) iff ex c st c in ( dom f) & c in X & d = (f /. c) by Th22;

    theorem :: PARTFUN2:24

    c in ( dom f) implies ( Im (f,c)) = {(f /. c)}

    proof

      assume

       A1: c in ( dom f);

      

      hence ( Im (f,c)) = {(f qua Function . c)} by FUNCT_1: 59

      .= {(f /. c)} by A1, PARTFUN1:def 6;

    end;

    theorem :: PARTFUN2:25

    c1 in ( dom f) & c2 in ( dom f) implies (f .: {c1, c2}) = {(f /. c1), (f /. c2)}

    proof

      assume that

       A1: c1 in ( dom f) and

       A2: c2 in ( dom f);

      

      thus (f .: {c1, c2}) = {(f qua Function . c1), (f qua Function . c2)} by A1, A2, FUNCT_1: 60

      .= {(f /. c1), (f qua Function . c2)} by A1, PARTFUN1:def 6

      .= {(f /. c1), (f /. c2)} by A2, PARTFUN1:def 6;

    end;

    theorem :: PARTFUN2:26

    

     Th26: SC = (f " X) iff for c holds c in SC iff c in ( dom f) & (f /. c) in X

    proof

      thus SC = (f " X) implies for c holds c in SC iff c in ( dom f) & (f /. c) in X

      proof

        assume

         A1: SC = (f " X);

        let c;

        thus c in SC implies c in ( dom f) & (f /. c) in X

        proof

          assume c in SC;

          then c in ( dom f) & (f qua Function . c) in X by A1, FUNCT_1:def 7;

          hence thesis by PARTFUN1:def 6;

        end;

        assume that

         A2: c in ( dom f) and

         A3: (f /. c) in X;

        (f qua Function . c) in X by A2, A3, PARTFUN1:def 6;

        hence thesis by A1, A2, FUNCT_1:def 7;

      end;

      assume

       A4: for c holds c in SC iff c in ( dom f) & (f /. c) in X;

      now

        let x be object;

        thus x in SC implies x in ( dom f) & (f qua Function . x) in X

        proof

          assume

           A5: x in SC;

          then

          reconsider x1 = x as Element of C;

          x1 in ( dom f) & (f /. x1) in X by A4, A5;

          hence thesis by PARTFUN1:def 6;

        end;

        assume that

         A6: x in ( dom f) and

         A7: (f qua Function . x) in X;

        reconsider x1 = x as Element of C by A6;

        (f /. x1) in X by A6, A7, PARTFUN1:def 6;

        hence x in SC by A4, A6;

      end;

      hence thesis by FUNCT_1:def 7;

    end;

    theorem :: PARTFUN2:27

    for f holds ex g be Function of C, D st for c st c in ( dom f) holds (g . c) = (f /. c)

    proof

      let f;

      consider g be Function of C, D such that

       A1: for x be object st x in ( dom f) holds (g . x) = (f qua Function . x) by FUNCT_2: 71;

      take g;

      let c;

      assume

       A2: c in ( dom f);

      then (g . c) = (f qua Function . c) by A1;

      hence thesis by A2, PARTFUN1:def 6;

    end;

    theorem :: PARTFUN2:28

    f tolerates g iff for c st c in (( dom f) /\ ( dom g)) holds (f /. c) = (g /. c)

    proof

      thus f tolerates g implies for c st c in (( dom f) /\ ( dom g)) holds (f /. c) = (g /. c)

      proof

        assume

         A1: f tolerates g;

        let c;

        assume

         A2: c in (( dom f) /\ ( dom g));

        then

         A3: c in ( dom f) by XBOOLE_0:def 4;

        (f qua Function . c) = (g qua Function . c) by A1, A2, PARTFUN1:def 4;

        then

         A4: (f /. c) = (g qua Function . c) by A3, PARTFUN1:def 6;

        c in ( dom g) by A2, XBOOLE_0:def 4;

        hence thesis by A4, PARTFUN1:def 6;

      end;

      assume

       A5: for c st c in (( dom f) /\ ( dom g)) holds (f /. c) = (g /. c);

      now

        let x be object;

        assume

         A6: x in (( dom f) /\ ( dom g));

        then

        reconsider x1 = x as Element of C;

        x in ( dom f) & (f /. x1) = (g /. x1) by A5, A6, XBOOLE_0:def 4;

        then

         A7: (f qua Function . x) = (g /. x1) by PARTFUN1:def 6;

        x in ( dom g) by A6, XBOOLE_0:def 4;

        hence (f qua Function . x) = (g qua Function . x) by A7, PARTFUN1:def 6;

      end;

      hence thesis by PARTFUN1:def 4;

    end;

    scheme :: PARTFUN2:sch1

    PartFuncExD { D,C() -> non empty set , P[ object, object] } :

ex f be PartFunc of D(), C() st (for d be Element of D() holds d in ( dom f) iff (ex c be Element of C() st P[d, c])) & for d be Element of D() st d in ( dom f) holds P[d, (f /. d)];

      defpred R[ object] means ex c be Element of C() st P[$1, c];

      set x = the Element of C();

      defpred Q[ object, object] means ((ex c be Element of C() st P[$1, c]) implies P[$1, $2]) & ((for c be Element of C() holds not P[$1, c]) implies $2 = x);

      consider X be set such that

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

      for x be object holds x in X implies x in D() by A1;

      then

      reconsider X as Subset of D() by TARSKI:def 3;

      

       A2: for d be Element of D() holds ex z be Element of C() st Q[d, z]

      proof

        let d be Element of D();

        (for c be Element of C() holds not P[d, c]) implies ex z be Element of C() st ((ex c be Element of C() st P[d, c]) implies P[d, z]) & ((for c be Element of C() holds not P[d, c]) implies z = x);

        hence thesis;

      end;

      consider g be Function of D(), C() such that

       A3: for d be Element of D() holds Q[d, (g . d)] from FUNCT_2:sch 3( A2);

      reconsider f = (g | X) as PartFunc of D(), C();

      take f;

      

       A4: ( dom g) = D() by FUNCT_2:def 1;

      thus for d be Element of D() holds d in ( dom f) iff ex c be Element of C() st P[d, c]

      proof

        let d be Element of D();

        ( dom f) c= X by RELAT_1: 58;

        hence d in ( dom f) implies ex c be Element of C() st P[d, c] by A1;

        assume ex c be Element of C() st P[d, c];

        then d in X by A1;

        then d in (( dom g) /\ X) by A4, XBOOLE_0:def 4;

        hence thesis by RELAT_1: 61;

      end;

      let d be Element of D();

      assume

       A5: d in ( dom f);

      ( dom f) c= X by RELAT_1: 58;

      then ex c be Element of C() st P[d, c] by A1, A5;

      then P[d, (g . d)] by A3;

      then P[d, (f qua Function . d)] by A5, FUNCT_1: 47;

      hence thesis by A5, PARTFUN1:def 6;

    end;

    scheme :: PARTFUN2:sch2

    LambdaPFD { D,C() -> non empty set , F( set) -> Element of C() , P[ set] } :

ex f be PartFunc of D(), C() st (for d be Element of D() holds d in ( dom f) iff P[d]) & for d be Element of D() st d in ( dom f) holds (f /. d) = F(d);

      defpred Q[ set, set] means P[$1] & $2 = F($1);

      consider f be PartFunc of D(), C() such that

       A1: for d be Element of D() holds d in ( dom f) iff ex c be Element of C() st Q[d, c] and

       A2: for d be Element of D() st d in ( dom f) holds Q[d, (f /. d)] from PartFuncExD;

      take f;

      thus for d be Element of D() holds d in ( dom f) iff P[d]

      proof

        let d be Element of D();

        thus d in ( dom f) implies P[d]

        proof

          assume d in ( dom f);

          then ex c be Element of C() st P[d] & c = F(d) by A1;

          hence thesis;

        end;

        assume P[d];

        then ex c be Element of C() st P[d] & c = F(d);

        hence thesis by A1;

      end;

      thus thesis by A2;

    end;

    scheme :: PARTFUN2:sch3

    UnPartFuncD { C,D() -> non empty set , X() -> set , F( set) -> Element of D() } :

for f,g be PartFunc of C(), D() st (( dom f) = X() & for c be Element of C() st c in ( dom f) holds (f /. c) = F(c)) & (( dom g) = X() & for c be Element of C() st c in ( dom g) holds (g /. c) = F(c)) holds f = g;

      let f,g be PartFunc of C(), D();

      assume that

       A1: ( dom f) = X() and

       A2: for c be Element of C() st c in ( dom f) holds (f /. c) = F(c) and

       A3: ( dom g) = X() and

       A4: for c be Element of C() st c in ( dom g) holds (g /. c) = F(c);

      now

        let c be Element of C();

        assume

         A5: c in ( dom f);

        

        hence (f /. c) = F(c) by A2

        .= (g /. c) by A1, A3, A4, A5;

      end;

      hence thesis by A1, A3, Th1;

    end;

    definition

      let C, D;

      let SC, d;

      :: original: -->

      redefine

      func SC --> d -> PartFunc of C, D ;

      coherence

      proof

        ( dom (SC --> d)) = SC by FUNCOP_1: 13;

        hence thesis by RELSET_1: 7;

      end;

    end

    theorem :: PARTFUN2:29

    

     Th29: c in SC implies ((SC --> d) /. c) = d

    proof

      assume

       A1: c in SC;

      then ( dom (SC --> d)) = SC & ((SC --> d) qua Function . c) = d by FUNCOP_1: 7, FUNCOP_1: 13;

      hence thesis by A1, PARTFUN1:def 6;

    end;

    theorem :: PARTFUN2:30

    (for c st c in ( dom f) holds (f /. c) = d) implies f = (( dom f) --> d)

    proof

      assume

       A1: for c st c in ( dom f) holds (f /. c) = d;

      now

        let x be object;

        assume

         A2: x in ( dom f);

        then

        reconsider x1 = x as Element of C;

        (f /. x1) = d by A1, A2;

        hence (f qua Function . x) = d by A2, PARTFUN1:def 6;

      end;

      hence thesis by FUNCOP_1: 11;

    end;

    theorem :: PARTFUN2:31

    c in ( dom f) implies (f * (SE --> c)) = (SE --> (f /. c))

    proof

      assume

       A1: c in ( dom f);

      then (f * (SE --> c)) = (SE --> (f qua Function . c)) by FUNCOP_1: 17;

      hence thesis by A1, PARTFUN1:def 6;

    end;

    theorem :: PARTFUN2:32

    ( id SC) is total iff SC = C

    proof

      thus ( id SC) is total implies SC = C

      proof

        assume ( id SC) is total;

        then ( dom ( id SC)) = C by PARTFUN1:def 2;

        hence thesis by RELAT_1: 45;

      end;

      assume SC = C;

      then ( dom ( id SC)) = C by RELAT_1: 45;

      hence thesis by PARTFUN1:def 2;

    end;

    theorem :: PARTFUN2:33

    (SC --> d) is total implies SC <> {}

    proof

      assume that

       A1: (SC --> d) is total and

       A2: SC = {} ;

      ( dom (SC --> d)) = C by A1, PARTFUN1:def 2;

      hence contradiction by A2, FUNCOP_1: 10;

    end;

    theorem :: PARTFUN2:34

    (SC --> d) is total iff SC = C

    proof

      thus (SC --> d) is total implies SC = C

      proof

        assume (SC --> d) is total;

        then ( dom (SC --> d)) = C by PARTFUN1:def 2;

        hence thesis by FUNCOP_1: 13;

      end;

      assume SC = C;

      then ( dom (SC --> d)) = C by FUNCOP_1: 13;

      hence thesis by PARTFUN1:def 2;

    end;

    definition

      let C, D, f;

      :: original: constant

      redefine

      :: PARTFUN2:def1

      attr f is constant means ex d st for c st c in ( dom f) holds (f . c) = d;

      compatibility

      proof

        thus f is constant implies ex d st for c st c in ( dom f) holds (f . c) = d

        proof

          assume

           A1: f is constant;

          per cases ;

            suppose

             A2: ( dom f) = {} ;

            set d = the Element of D;

            take d;

            thus thesis by A2;

          end;

            suppose ( dom f) <> {} ;

            then

            consider c0 be object such that

             A3: c0 in ( dom f) by XBOOLE_0:def 1;

            reconsider c0 as Element of C by A3;

            take d = (f /. c0);

            let c;

            assume c in ( dom f);

            

            hence (f . c) = (f . c0) by A1, A3

            .= d by A3, PARTFUN1:def 6;

          end;

        end;

        given d such that

         A4: for c st c in ( dom f) holds (f . c) = d;

        let x,y be object such that

         A5: x in ( dom f) and

         A6: y in ( dom f);

        

        thus (f . x) = d by A4, A5

        .= (f . y) by A4, A6;

      end;

    end

    theorem :: PARTFUN2:35

    

     Th35: (f | X) is constant iff ex d st for c st c in (X /\ ( dom f)) holds (f /. c) = d

    proof

      thus (f | X) is constant implies ex d st for c st c in (X /\ ( dom f)) holds (f /. c) = d

      proof

        given d such that

         A1: for c st c in ( dom (f | X)) holds ((f | X) . c) = d;

        take d;

        let c;

        assume

         A2: c in (X /\ ( dom f));

        then

         A3: c in ( dom (f | X)) by RELAT_1: 61;

        c in ( dom f) by A2, XBOOLE_0:def 4;

        

        hence (f /. c) = (f . c) by PARTFUN1:def 6

        .= ((f | X) . c) by A3, FUNCT_1: 47

        .= d by A1, A3;

      end;

      given d such that

       A4: for c st c in (X /\ ( dom f)) holds (f /. c) = d;

      take d;

      let c;

      assume

       A5: c in ( dom (f | X));

      then

       A6: c in (X /\ ( dom f)) by RELAT_1: 61;

      then

       A7: c in ( dom f) by XBOOLE_0:def 4;

      

      thus ((f | X) . c) = (f . c) by A5, FUNCT_1: 47

      .= (f /. c) by A7, PARTFUN1:def 6

      .= d by A4, A6;

    end;

    theorem :: PARTFUN2:36

    (f | X) is constant iff for c1, c2 st c1 in (X /\ ( dom f)) & c2 in (X /\ ( dom f)) holds (f /. c1) = (f /. c2)

    proof

      thus (f | X) is constant implies for c1, c2 st c1 in (X /\ ( dom f)) & c2 in (X /\ ( dom f)) holds (f /. c1) = (f /. c2)

      proof

        assume (f | X) is constant;

        then

        consider d such that

         A1: for c st c in (X /\ ( dom f)) holds (f /. c) = d by Th35;

        let c1, c2;

        assume that

         A2: c1 in (X /\ ( dom f)) and

         A3: c2 in (X /\ ( dom f));

        (f /. c1) = d by A1, A2;

        hence thesis by A1, A3;

      end;

      assume

       A4: for c1, c2 st c1 in (X /\ ( dom f)) & c2 in (X /\ ( dom f)) holds (f /. c1) = (f /. c2);

      now

        per cases ;

          suppose

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

          now

            set d = the Element of D;

            take d;

            let c;

            thus c in (X /\ ( dom f)) implies (f /. c) = d by A5;

          end;

          hence thesis by Th35;

        end;

          suppose

           A6: (X /\ ( dom f)) <> {} ;

          set x = the Element of (X /\ ( dom f));

          x in ( dom f) by A6, XBOOLE_0:def 4;

          then

          reconsider x as Element of C;

          for c holds c in (X /\ ( dom f)) implies (f /. c) = (f /. x) by A4;

          hence thesis by Th35;

        end;

      end;

      hence thesis;

    end;

    theorem :: PARTFUN2:37

    X meets ( dom f) implies ((f | X) is constant iff ex d st ( rng (f | X)) = {d})

    proof

      assume

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

      thus (f | X) is constant implies ex d st ( rng (f | X)) = {d}

      proof

        assume (f | X) is constant;

        then

        consider d such that

         A2: for c st c in (X /\ ( dom f)) holds (f /. c) = d by Th35;

        take d;

        thus ( rng (f | X)) c= {d}

        proof

          let x be object;

          assume x in ( rng (f | X));

          then

          consider y be object such that

           A3: y in ( dom (f | X)) and

           A4: ((f | X) qua Function . y) = x by FUNCT_1:def 3;

          reconsider y as Element of C by A3;

          ( dom (f | X)) = (X /\ ( dom f)) by RELAT_1: 61;

          

          then d = (f /. y) by A2, A3

          .= ((f | X) /. y) by A3, Th15

          .= x by A3, A4, PARTFUN1:def 6;

          hence thesis by TARSKI:def 1;

        end;

        thus {d} c= ( rng (f | X))

        proof

          set y = the Element of (X /\ ( dom f));

          y in ( dom f) by A1, XBOOLE_0:def 4;

          then

          reconsider y as Element of C;

          let x be object such that

           A5: x in {d};

          

           A6: ( dom (f | X)) = (X /\ ( dom f)) by RELAT_1: 61;

          

          then ((f | X) /. y) = (f /. y) by A1, Th15

          .= d by A1, A2

          .= x by A5, TARSKI:def 1;

          hence thesis by A1, A6, Th2;

        end;

      end;

      given d such that

       A7: ( rng (f | X)) = {d};

      take d;

      let c;

      assume

       A8: c in ( dom (f | X));

      then ((f | X) /. c) in {d} by A7, Th2;

      then ((f | X) . c) in {d} by A8, PARTFUN1:def 6;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: PARTFUN2:38

    (f | X) is constant & Y c= X implies (f | Y) is constant

    proof

      assume that

       A1: (f | X) is constant and

       A2: Y c= X;

      consider d such that

       A3: for c st c in (X /\ ( dom f)) holds (f /. c) = d by A1, Th35;

      now

        let c;

        assume c in (Y /\ ( dom f));

        then c in Y & c in ( dom f) by XBOOLE_0:def 4;

        then c in (X /\ ( dom f)) by A2, XBOOLE_0:def 4;

        hence (f /. c) = d by A3;

      end;

      hence thesis by Th35;

    end;

    theorem :: PARTFUN2:39

    

     Th39: X misses ( dom f) implies (f | X) is constant

    proof

      assume

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

      now

        set d = the Element of D;

        take d;

        let c;

        thus c in (X /\ ( dom f)) implies (f /. c) = d by A1;

      end;

      hence thesis by Th35;

    end;

    theorem :: PARTFUN2:40

    (f | SC) = (( dom (f | SC)) --> d) implies (f | SC) is constant

    proof

      assume

       A1: (f | SC) = (( dom (f | SC)) --> d);

      now

        let c;

        assume c in (SC /\ ( dom f));

        then

         A2: c in ( dom (f | SC)) by RELAT_1: 61;

        then ((f | SC) /. c) = d by A1, Th29;

        hence (f /. c) = d by A2, Th15;

      end;

      hence thesis by Th35;

    end;

    theorem :: PARTFUN2:41

    (f | {x}) is constant

    proof

      now

        per cases ;

          suppose ( {x} /\ ( dom f)) = {} ;

          then {x} misses ( dom f);

          hence thesis by Th39;

        end;

          suppose

           A1: ( {x} /\ ( dom f)) <> {} ;

          set y = the Element of ( {x} /\ ( dom f));

          y in {x} & y in ( dom f) by A1, XBOOLE_0:def 4;

          then

          reconsider x1 = x as Element of C by TARSKI:def 1;

          now

            take d = (f /. x1);

            let c;

            assume c in ( {x} /\ ( dom f));

            then c in {x} by XBOOLE_0:def 4;

            hence (f /. c) = (f /. x1) by TARSKI:def 1;

          end;

          hence thesis by Th35;

        end;

      end;

      hence thesis;

    end;

    theorem :: PARTFUN2:42

    (f | X) is constant & (f | Y) is constant & (X /\ Y) meets ( dom f) implies (f | (X \/ Y)) is constant

    proof

      assume that

       A1: (f | X) is constant and

       A2: (f | Y) is constant and

       A3: ((X /\ Y) /\ ( dom f)) <> {} ;

      consider d1 such that

       A4: for c st c in (X /\ ( dom f)) holds (f /. c) = d1 by A1, Th35;

      set x = the Element of ((X /\ Y) /\ ( dom f));

      

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

      

       A6: x in ( dom f) by A3, XBOOLE_0:def 4;

      then

      reconsider x as Element of C;

      x in Y by A5, XBOOLE_0:def 4;

      then

       A7: x in (Y /\ ( dom f)) by A6, XBOOLE_0:def 4;

      consider d2 such that

       A8: for c st c in (Y /\ ( dom f)) holds (f /. c) = d2 by A2, Th35;

      x in X by A5, XBOOLE_0:def 4;

      then x in (X /\ ( dom f)) by A6, XBOOLE_0:def 4;

      then (f /. x) = d1 by A4;

      then

       A9: d1 = d2 by A8, A7;

      take d1;

      let c;

      assume

       A10: c in ( dom (f | (X \/ Y)));

      then

       A11: c in ((X \/ Y) /\ ( dom f)) by RELAT_1: 61;

      then

       A12: c in ( dom f) by XBOOLE_0:def 4;

      

       A13: c in (X \/ Y) by A11, XBOOLE_0:def 4;

      now

        per cases by A13, XBOOLE_0:def 3;

          suppose c in X;

          then c in (X /\ ( dom f)) by A12, XBOOLE_0:def 4;

          hence (f /. c) = d1 by A4;

        end;

          suppose c in Y;

          then c in (Y /\ ( dom f)) by A12, XBOOLE_0:def 4;

          hence (f /. c) = d1 by A8, A9;

        end;

      end;

      then ((f | (X \/ Y)) /. c) = d1 by A11, Th16;

      hence thesis by A10, PARTFUN1:def 6;

    end;

    theorem :: PARTFUN2:43

    (f | Y) is constant implies ((f | X) | Y) is constant

    proof

      assume (f | Y) is constant;

      then

      consider d such that

       A1: for c st c in (Y /\ ( dom f)) holds (f /. c) = d by Th35;

      take d;

      let c;

      assume

       A2: c in ( dom ((f | X) | Y));

      then

       A3: c in (Y /\ ( dom (f | X))) by RELAT_1: 61;

      then

       A4: c in Y by XBOOLE_0:def 4;

      

       A5: c in ( dom (f | X)) by A3, XBOOLE_0:def 4;

      then c in (( dom f) /\ X) by RELAT_1: 61;

      then c in ( dom f) by XBOOLE_0:def 4;

      then c in (Y /\ ( dom f)) by A4, XBOOLE_0:def 4;

      then (f /. c) = d by A1;

      then ((f | X) /. c) = d by A5, Th15;

      then (((f | X) | Y) /. c) = d by A3, Th16;

      hence thesis by A2, PARTFUN1:def 6;

    end;

    theorem :: PARTFUN2:44

    ((SC --> d) | SC) is constant

    proof

      take d;

      let c;

      assume

       A1: c in ( dom ((SC --> d) | SC));

      then

       A2: c in (SC /\ ( dom (SC --> d))) by RELAT_1: 61;

      then c in SC by XBOOLE_0:def 4;

      then ((SC --> d) /. c) = d by Th29;

      then (((SC --> d) | SC) /. c) = d by A2, Th16;

      hence thesis by A1, PARTFUN1:def 6;

    end;

    theorem :: PARTFUN2:45

    ( dom f) c= ( dom g) & (for c st c in ( dom f) holds (f /. c) = (g /. c)) implies f c= g

    proof

      assume that

       A1: ( dom f) c= ( dom g) and

       A2: for c st c in ( dom f) holds (f /. c) = (g /. c);

      now

        let x be object;

        assume

         A3: x in ( dom f);

        then

        reconsider x1 = x as Element of C;

        (f /. x1) = (g /. x1) by A2, A3;

        then (f qua Function . x) = (g /. x1) by A3, PARTFUN1:def 6;

        hence (f qua Function . x) = (g qua Function . x) by A1, A3, PARTFUN1:def 6;

      end;

      hence thesis by A1, GRFUNC_1: 2;

    end;

    theorem :: PARTFUN2:46

    

     Th46: c in ( dom f) & d = (f /. c) iff [c, d] in f

    proof

      thus c in ( dom f) & d = (f /. c) implies [c, d] in f

      proof

        assume that

         A1: c in ( dom f) and

         A2: d = (f /. c);

        d = (f qua Function . c) by A1, A2, PARTFUN1:def 6;

        hence thesis by A1, FUNCT_1: 1;

      end;

      assume [c, d] in f;

      then c in ( dom f) & d = (f qua Function . c) by FUNCT_1: 1;

      hence thesis by PARTFUN1:def 6;

    end;

    theorem :: PARTFUN2:47

     [c, e] in (s * f) implies [c, (f /. c)] in f & [(f /. c), e] in s

    proof

      assume

       A1: [c, e] in (s * f);

      then

       A2: [(f qua Function . c), e] in s by GRFUNC_1: 4;

      

       A3: [c, (f qua Function . c)] in f by A1, GRFUNC_1: 4;

      then c in ( dom f) by FUNCT_1: 1;

      hence thesis by A3, A2, PARTFUN1:def 6;

    end;

    theorem :: PARTFUN2:48

    f = { [c, d]} implies (f /. c) = d

    proof

      assume

       A1: f = { [c, d]};

      then [c, d] in f by TARSKI:def 1;

      then

       A2: c in ( dom f) by FUNCT_1: 1;

      (f qua Function . c) = d by A1, GRFUNC_1: 6;

      hence thesis by A2, PARTFUN1:def 6;

    end;

    theorem :: PARTFUN2:49

    ( dom f) = {c} implies f = { [c, (f /. c)]}

    proof

      assume ( dom f) = {c};

      then c in ( dom f) & f = { [c, (f qua Function . c)]} by GRFUNC_1: 7, TARSKI:def 1;

      hence thesis by PARTFUN1:def 6;

    end;

    theorem :: PARTFUN2:50

    f1 = (f /\ g) & c in ( dom f1) implies (f1 /. c) = (f /. c) & (f1 /. c) = (g /. c)

    proof

      assume that

       A1: f1 = (f /\ g) and

       A2: c in ( dom f1);

      (f1 qua Function . c) = (g qua Function . c) by A1, A2, GRFUNC_1: 11;

      then

       A3: (f1 /. c) = (g qua Function . c) by A2, PARTFUN1:def 6;

      

       A4: [c, (f1 qua Function . c)] in f1 by A2, FUNCT_1: 1;

      then [c, (f1 qua Function . c)] in f by A1, XBOOLE_0:def 4;

      then

       A5: c in ( dom f) by FUNCT_1: 1;

       [c, (f1 qua Function . c)] in g by A1, A4, XBOOLE_0:def 4;

      then

       A6: c in ( dom g) by FUNCT_1: 1;

      (f1 qua Function . c) = (f qua Function . c) by A1, A2, GRFUNC_1: 11;

      then (f1 /. c) = (f qua Function . c) by A2, PARTFUN1:def 6;

      hence thesis by A5, A6, A3, PARTFUN1:def 6;

    end;

    theorem :: PARTFUN2:51

    c in ( dom f) & f1 = (f \/ g) implies (f1 /. c) = (f /. c)

    proof

      assume that

       A1: c in ( dom f) and

       A2: f1 = (f \/ g);

       [c, (f qua Function . c)] in f by A1, FUNCT_1: 1;

      then [c, (f qua Function . c)] in f1 by A2, XBOOLE_0:def 3;

      then

       A3: c in ( dom f1) by FUNCT_1: 1;

      (f1 qua Function . c) = (f qua Function . c) by A1, A2, GRFUNC_1: 15;

      then (f1 /. c) = (f qua Function . c) by A3, PARTFUN1:def 6;

      hence thesis by A1, PARTFUN1:def 6;

    end;

    theorem :: PARTFUN2:52

    c in ( dom g) & f1 = (f \/ g) implies (f1 /. c) = (g /. c)

    proof

      assume that

       A1: c in ( dom g) and

       A2: f1 = (f \/ g);

       [c, (g qua Function . c)] in g by A1, FUNCT_1: 1;

      then [c, (g qua Function . c)] in f1 by A2, XBOOLE_0:def 3;

      then

       A3: c in ( dom f1) by FUNCT_1: 1;

      (f1 qua Function . c) = (g qua Function . c) by A1, A2, GRFUNC_1: 15;

      then (f1 /. c) = (g qua Function . c) by A3, PARTFUN1:def 6;

      hence thesis by A1, PARTFUN1:def 6;

    end;

    theorem :: PARTFUN2:53

    c in ( dom f1) & f1 = (f \/ g) implies (f1 /. c) = (f /. c) or (f1 /. c) = (g /. c)

    proof

      assume that

       A1: c in ( dom f1) and

       A2: f1 = (f \/ g);

       [c, (f1 /. c)] in f1 by A1, Th46;

      then

       A3: [c, (f1 /. c)] in f or [c, (f1 /. c)] in g by A2, XBOOLE_0:def 3;

      now

        per cases by A3, FUNCT_1: 1;

          suppose c in ( dom f);

          then [c, (f /. c)] in f by Th46;

          then [c, (f /. c)] in f1 by A2, XBOOLE_0:def 3;

          hence thesis by Th46;

        end;

          suppose c in ( dom g);

          then [c, (g /. c)] in g by Th46;

          then [c, (g /. c)] in f1 by A2, XBOOLE_0:def 3;

          hence thesis by Th46;

        end;

      end;

      hence thesis;

    end;

    theorem :: PARTFUN2:54

    c in ( dom f) & c in SC iff [c, (f /. c)] in (f | SC)

    proof

      thus c in ( dom f) & c in SC implies [c, (f /. c)] in (f | SC)

      proof

        assume that

         A1: c in ( dom f) and

         A2: c in SC;

         [c, (f qua Function . c)] in (f | SC) by A1, A2, GRFUNC_1: 22;

        hence thesis by A1, PARTFUN1:def 6;

      end;

      assume [c, (f /. c)] in (f | SC);

      then c in ( dom (f | SC)) by FUNCT_1: 1;

      then c in (( dom f) /\ SC) by RELAT_1: 61;

      hence thesis by XBOOLE_0:def 4;

    end;

    theorem :: PARTFUN2:55

    c in ( dom f) & (f /. c) in SD iff [c, (f /. c)] in (SD |` f)

    proof

      thus c in ( dom f) & (f /. c) in SD implies [c, (f /. c)] in (SD |` f)

      proof

        assume that

         A1: c in ( dom f) and

         A2: (f /. c) in SD;

        (f qua Function . c) in SD by A1, A2, PARTFUN1:def 6;

        then [c, (f qua Function . c)] in (SD |` f) by A1, GRFUNC_1: 24;

        hence thesis by A1, PARTFUN1:def 6;

      end;

      assume [c, (f /. c)] in (SD |` f);

      then c in ( dom (SD |` f)) by FUNCT_1: 1;

      then c in ( dom f) & (f qua Function . c) in SD by FUNCT_1: 54;

      hence thesis by PARTFUN1:def 6;

    end;

    theorem :: PARTFUN2:56

    c in (f " SD) iff [c, (f /. c)] in f & (f /. c) in SD

    proof

      thus c in (f " SD) implies [c, (f /. c)] in f & (f /. c) in SD

      proof

        assume

         A1: c in (f " SD);

        then

         A2: (f qua Function . c) in SD by GRFUNC_1: 26;

        

         A3: [c, (f qua Function . c)] in f by A1, GRFUNC_1: 26;

        then c in ( dom f) by FUNCT_1: 1;

        hence thesis by A3, A2, PARTFUN1:def 6;

      end;

      assume that

       A4: [c, (f /. c)] in f and

       A5: (f /. c) in SD;

      c in ( dom f) by A4, Th46;

      hence thesis by A5, Th26;

    end;

    theorem :: PARTFUN2:57

    

     Th57: (f | X) is constant iff ex d st for c st c in (X /\ ( dom f)) holds (f . c) = d

    proof

      hereby

        assume (f | X) is constant;

        then

        consider d such that

         A1: for c st c in (X /\ ( dom f)) holds (f /. c) = d by Th35;

        take d;

        let c;

        assume

         A2: c in (X /\ ( dom f));

        then c in ( dom f) by XBOOLE_0:def 4;

        

        hence (f . c) = (f /. c) by PARTFUN1:def 6

        .= d by A1, A2;

      end;

      given d such that

       A3: for c st c in (X /\ ( dom f)) holds (f . c) = d;

      take d;

      let c;

      assume

       A4: c in ( dom (f | X));

      then

       A5: c in (X /\ ( dom f)) by RELAT_1: 61;

      then

       A6: c in ( dom f) by XBOOLE_0:def 4;

      

      thus ((f | X) . c) = ((f | X) /. c) by A4, PARTFUN1:def 6

      .= (f /. c) by A5, Th16

      .= (f . c) by A6, PARTFUN1:def 6

      .= d by A3, A5;

    end;

    theorem :: PARTFUN2:58

    (f | X) is constant iff for c1, c2 st c1 in (X /\ ( dom f)) & c2 in (X /\ ( dom f)) holds (f . c1) = (f . c2)

    proof

      thus (f | X) is constant implies for c1, c2 st c1 in (X /\ ( dom f)) & c2 in (X /\ ( dom f)) holds (f . c1) = (f . c2)

      proof

        assume (f | X) is constant;

        then

        consider d such that

         A1: for c st c in (X /\ ( dom f)) holds (f . c) = d by Th57;

        let c1, c2;

        assume that

         A2: c1 in (X /\ ( dom f)) and

         A3: c2 in (X /\ ( dom f));

        (f . c1) = d by A1, A2;

        hence thesis by A1, A3;

      end;

      assume

       A4: for c1, c2 st c1 in (X /\ ( dom f)) & c2 in (X /\ ( dom f)) holds (f . c1) = (f . c2);

      now

        per cases ;

          suppose

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

          now

            set d = the Element of D;

            take d;

            let c;

            thus c in (X /\ ( dom f)) implies (f . c) = d by A5;

          end;

          hence thesis by Th57;

        end;

          suppose

           A6: (X /\ ( dom f)) <> {} ;

          set x = the Element of (X /\ ( dom f));

          now

            let c;

            

             A7: x in ( dom f) by A6, XBOOLE_0:def 4;

            assume c in (X /\ ( dom f));

            

            hence (f . c) = (f . x) by A4, A7

            .= (f /. x) by A7, PARTFUN1:def 6;

          end;

          hence thesis by Th57;

        end;

      end;

      hence thesis;

    end;

    theorem :: PARTFUN2:59

    d in (f .: X) implies ex c st c in ( dom f) & c in X & d = (f . c)

    proof

      assume d in (f .: X);

      then

      consider x be object such that

       A1: x in ( dom f) and

       A2: x in X & d = (f qua Function . x) by FUNCT_1:def 6;

      reconsider x as Element of C by A1;

      take x;

      thus thesis by A1, A2;

    end;

    theorem :: PARTFUN2:60

    f is one-to-one implies (d in ( rng f) & c = ((f " ) . d) iff c in ( dom f) & d = (f . c))

    proof

      

       A1: (f " ) = (f qua Function " );

      assume f is one-to-one;

      hence thesis by A1, FUNCT_1: 32;

    end;

    theorem :: PARTFUN2:61

    for Y holds for f,g be Y -valued Function st f c= g holds for x st x in ( dom f) holds (f /. x) = (g /. x)

    proof

      let Y;

      let f,g be Y -valued Function;

      assume

       A1: f c= g;

      then

       A2: ( dom f) c= ( dom g) by GRFUNC_1: 2;

      let x;

      assume

       A3: x in ( dom f);

      then (f . x) = (g . x) by A1, GRFUNC_1: 2;

      then (f /. x) = (g qua Function . x) by A3, PARTFUN1:def 6;

      hence thesis by A2, A3, PARTFUN1:def 6;

    end;