partfun1.miz



    begin

    reserve x,x1,x2,y,y9,y1,y2,z,z1,z2 for object,

P,X,X1,X2,Y,Y1,Y2,V,Z for set;

    theorem :: PARTFUN1:1

    

     Th1: for f,g be Function st for x be object st x in (( dom f) /\ ( dom g)) holds (f . x) = (g . x) holds (f \/ g) is Function

    proof

      let f,g be Function such that

       A1: for x be object st x in (( dom f) /\ ( dom g)) holds (f . x) = (g . x);

      defpred P[ object, object] means [$1, $2] in (f \/ g);

      

       A2: for x,y1,y2 be object st P[x, y1] & P[x, y2] holds y1 = y2

      proof

        let x,y1,y2 be object such that

         A3: [x, y1] in (f \/ g) and

         A4: [x, y2] in (f \/ g);

        now

           [x, y1] in f or [x, y1] in g by A3, XBOOLE_0:def 3;

          then

           A5: x in ( dom f) & (f . x) = y1 or x in ( dom g) & (g . x) = y1 by FUNCT_1: 1;

          

           A6: [x, y2] in f or [x, y2] in g by A4, XBOOLE_0:def 3;

          then

           A7: x in ( dom f) & (f . x) = y2 or x in ( dom g) & (g . x) = y2 by FUNCT_1: 1;

          per cases by A6, XTUPLE_0:def 12;

            suppose x in ( dom f) & x in ( dom g);

            then x in (( dom f) /\ ( dom g)) by XBOOLE_0:def 4;

            hence thesis by A1, A5, A7;

          end;

            suppose x in ( dom f) & not x in ( dom g);

            hence thesis by A6, A5, FUNCT_1: 1;

          end;

            suppose not x in ( dom f) & x in ( dom g);

            hence thesis by A6, A5, FUNCT_1: 1;

          end;

        end;

        hence thesis;

      end;

      consider h be Function such that

       A8: for x,y be object holds [x, y] in h iff x in (( dom f) \/ ( dom g)) & P[x, y] from FUNCT_1:sch 1( A2);

      h = (f \/ g)

      proof

        let x,y be object;

        thus [x, y] in h implies [x, y] in (f \/ g) by A8;

        assume

         A9: [x, y] in (f \/ g);

         [x, y] in f or [x, y] in g by A9, XBOOLE_0:def 3;

        then x in ( dom f) or x in ( dom g) by XTUPLE_0:def 12;

        then x in (( dom f) \/ ( dom g)) by XBOOLE_0:def 3;

        hence thesis by A8, A9;

      end;

      hence thesis;

    end;

    theorem :: PARTFUN1:2

    

     Th2: for f,g,h be Function st (f \/ g) = h holds for x be object st x in (( dom f) /\ ( dom g)) holds (f . x) = (g . x)

    proof

      let f,g,h be Function such that

       A1: (f \/ g) = h;

      let x be object;

      assume

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

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

      then

       A3: (h . x) = (f . x) by A1, GRFUNC_1: 15;

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

      hence thesis by A1, A3, GRFUNC_1: 15;

    end;

    scheme :: PARTFUN1:sch1

    LambdaC { A() -> set , C[ object], F,G( object) -> object } :

ex f be Function st ( dom f) = A() & for x be object st x in A() holds (C[x] implies (f . x) = F(x)) & ( not C[x] implies (f . x) = G(x));

      defpred P[ object, object] means (C[$1] implies $2 = F($1)) & ( not C[$1] implies $2 = G($1));

      

       A1: for x be object st x in A() holds ex y be object st P[x, y]

      proof

        let x be object;

         not C[x] implies (C[x] implies G(x) = F(x)) & ( not C[x] implies G(x) = G(x));

        hence thesis;

      end;

      

       A2: for x,y1,y2 be object st x in A() & P[x, y1] & P[x, y2] holds y1 = y2;

      thus ex f be Function st ( dom f) = A() & for x be object st x in A() holds P[x, (f . x)] from FUNCT_1:sch 2( A2, A1);

    end;

     Lm1:

    now

      let X, Y;

      take E = {} ;

      thus ( dom E) c= X & ( rng E) c= Y;

    end;

    registration

      let X, Y;

      cluster Function-like for Relation of X, Y;

      existence

      proof

        consider E be Function such that

         A1: ( dom E) c= X & ( rng E) c= Y by Lm1;

        reconsider E as Relation of X, Y by A1, RELSET_1: 4;

        take E;

        thus thesis;

      end;

    end

    definition

      let X, Y;

      mode PartFunc of X,Y is Function-like Relation of X, Y;

    end

    theorem :: PARTFUN1:3

    for f be PartFunc of X, Y st y in ( rng f) holds ex x be Element of X st x in ( dom f) & y = (f . x)

    proof

      let f be PartFunc of X, Y;

      assume y in ( rng f);

      then ex x be object st x in ( dom f) & y = (f . x) by FUNCT_1:def 3;

      hence thesis;

    end;

    theorem :: PARTFUN1:4

    

     Th4: for f be Y -valued Function st x in ( dom f) holds (f . x) in Y

    proof

      let f be Y -valued Function;

      assume x in ( dom f);

      then

       A1: (f . x) in ( rng f) by FUNCT_1:def 3;

      ( rng f) c= Y by RELAT_1:def 19;

      hence thesis by A1;

    end;

    theorem :: PARTFUN1:5

    for f1,f2 be PartFunc of X, Y st ( dom f1) = ( dom f2) & for x be Element of X st x in ( dom f1) holds (f1 . x) = (f2 . x) holds f1 = f2;

    scheme :: PARTFUN1:sch2

    PartFuncEx { X,Y() -> set , P[ object, object] } :

ex f be PartFunc of X(), Y() st (for x be object holds x in ( dom f) iff x in X() & ex y be object st P[x, y]) & for x be object st x in ( dom f) holds P[x, (f . x)]

      provided

       A1: for x,y be object st x in X() & P[x, y] holds y in Y()

       and

       A2: for x,y1,y2 be object st x in X() & P[x, y1] & P[x, y2] holds y1 = y2;

       A3:

      now

        defpred R[ object] means ex y be object st P[$1, y];

        set y1 = the set;

        assume Y() <> {} ;

        defpred Q[ object, object] means ((ex y be object st P[$1, y]) implies P[$1, $2]) & ((for y be object holds not P[$1, y]) implies $2 = y1);

        

         A4: for x be object st x in X() holds ex z be object st Q[x, z]

        proof

          let x be object such that x in X();

          (for y be object holds not P[x, y]) implies ((ex y be object st P[x, y]) implies P[x, y1]) & ((for y be object holds not P[x, y]) implies y1 = y1);

          hence thesis;

        end;

        

         A5: for x,z1,z2 be object st x in X() & Q[x, z1] & Q[x, z2] holds z1 = z2 by A2;

        consider g be Function such that

         A6: ( dom g) = X() and

         A7: for x be object st x in X() holds Q[x, (g . x)] from FUNCT_1:sch 2( A5, A4);

        consider X be set such that

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

        set f = (g | X);

        

         A9: ( dom f) c= X() by A6, RELAT_1: 60;

        ( rng f) c= Y()

        proof

          let y be object;

          assume y in ( rng f);

          then

          consider x be object such that

           A10: x in ( dom f) and

           A11: y = (f . x) by FUNCT_1:def 3;

          

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

          then x in X() & ex y be object st P[x, y] by A8, A10;

          then P[x, (g . x)] by A7;

          then

           A13: P[x, y] by A10, A11, FUNCT_1: 47;

          x in X() by A8, A10, A12;

          hence thesis by A1, A13;

        end;

        then

        reconsider f as PartFunc of X(), Y() by A9, RELSET_1: 4;

        take f;

        thus for x be object holds x in ( dom f) iff x in X() & ex y be object st P[x, y]

        proof

          let x be object;

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

          hence x in ( dom f) implies x in X() & ex y be object st P[x, y] by A8;

          assume that

           A14: x in X() and

           A15: ex y be object st P[x, y];

          x in X by A8, A14, A15;

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

          hence thesis by RELAT_1: 61;

        end;

        let x be object;

        assume

         A16: x in ( dom f);

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

        then ex y be object st P[x, y] by A8, A16;

        then P[x, (g . x)] by A7, A16;

        hence P[x, (f . x)] by A16, FUNCT_1: 47;

      end;

      now

        consider f be Function such that

         A17: ( dom f) c= X() & ( rng f) c= Y() by Lm1;

        reconsider f as PartFunc of X(), Y() by A17, RELSET_1: 4;

        assume

         A18: Y() = {} ;

        take f;

        thus for x be object holds x in ( dom f) iff x in X() & ex y be object st P[x, y] by A1, A18;

        thus for x be object st x in ( dom f) holds P[x, (f . x)] by A18;

      end;

      hence thesis by A3;

    end;

    scheme :: PARTFUN1:sch3

    LambdaR { X,Y() -> set , F( object) -> object , P[ object] } :

ex f be PartFunc of X(), Y() st (for x be object holds x in ( dom f) iff x in X() & P[x]) & for x be object st x in ( dom f) holds (f . x) = F(x)

      provided

       A1: for x be object st P[x] holds F(x) in Y();

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

      

       A2: for x,y1,y2 be object st x in X() & Q[x, y1] & Q[x, y2] holds y1 = y2;

      

       A3: for x,y be object st x in X() & Q[x, y] holds y in Y() by A1;

      consider f be PartFunc of X(), Y() such that

       A4: for x be object holds x in ( dom f) iff x in X() & ex y be object st Q[x, y] and

       A5: for x be object st x in ( dom f) holds Q[x, (f . x)] from PartFuncEx( A3, A2);

      take f;

      thus for x be object holds x in ( dom f) iff x in X() & P[x]

      proof

        let x be object;

        thus x in ( dom f) implies x in X() & P[x]

        proof

          assume

           A6: x in ( dom f);

          then ex y be object st P[x] & y = F(x) by A4;

          hence thesis by A6;

        end;

        assume that

         A7: x in X() and

         A8: P[x];

        ex y st P[x] & y = F(x) by A8;

        hence thesis by A4, A7;

      end;

      thus thesis by A5;

    end;

    definition

      let X, Y, V, Z;

      let f be PartFunc of X, Y;

      let g be PartFunc of V, Z;

      :: original: *

      redefine

      func g * f -> PartFunc of X, Z ;

      coherence

      proof

        

         A1: ( dom (g * f)) c= X;

        ( rng (g * f)) c= Z by RELAT_1:def 19;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    theorem :: PARTFUN1:6

    for f be Relation of X, Y holds (( id X) * f) = f

    proof

      let f be Relation of X, Y;

      ( dom f) c= X;

      hence thesis by RELAT_1: 51;

    end;

    theorem :: PARTFUN1:7

    for f be Relation of X, Y holds (f * ( id Y)) = f

    proof

      let f be Relation of X, Y;

      ( rng f) c= Y;

      hence thesis by RELAT_1: 53;

    end;

    theorem :: PARTFUN1:8

    for f be PartFunc of X, Y st (for x1,x2 be Element of X st x1 in ( dom f) & x2 in ( dom f) & (f . x1) = (f . x2) holds x1 = x2) holds f is one-to-one;

    theorem :: PARTFUN1:9

    for f be PartFunc of X, Y st f is one-to-one holds (f " ) is PartFunc of Y, X

    proof

      let f be PartFunc of X, Y such that

       A1: f is one-to-one;

      ( rng f) c= Y by RELAT_1:def 19;

      then

       A2: ( dom (f " )) c= Y by A1, FUNCT_1: 33;

      ( dom f) c= X;

      then ( rng (f " )) c= X by A1, FUNCT_1: 33;

      hence thesis by A2, RELSET_1: 4;

    end;

    theorem :: PARTFUN1:10

    for f be PartFunc of X, Y holds (f | Z) is PartFunc of Z, Y

    proof

      let f be PartFunc of X, Y;

      ( dom (f | Z)) c= Z & ( rng (f | Z)) c= Y by RELAT_1: 58, RELAT_1:def 19;

      hence thesis by RELSET_1: 4;

    end;

    theorem :: PARTFUN1:11

    

     Th11: for f be PartFunc of X, Y holds (f | Z) is PartFunc of X, Y;

    definition

      let X, Y;

      let f be PartFunc of X, Y;

      let Z be set;

      :: original: |

      redefine

      func f | Z -> PartFunc of X, Y ;

      coherence by Th11;

    end

    theorem :: PARTFUN1:12

    for f be PartFunc of X, Y holds (Z |` f) is PartFunc of X, Z

    proof

      let f be PartFunc of X, Y;

      ( dom (Z |` f)) c= X & ( rng (Z |` f)) c= Z by RELAT_1: 85;

      hence thesis by RELSET_1: 4;

    end;

    theorem :: PARTFUN1:13

    for f be PartFunc of X, Y holds (Z |` f) is PartFunc of X, Y;

    theorem :: PARTFUN1:14

    

     Th14: for f be Function holds ((Y |` f) | X) is PartFunc of X, Y

    proof

      let f be Function;

      ((Y |` f) | X) = (Y |` (f | X)) by RELAT_1: 109;

      then ( dom ((Y |` f) | X)) c= X & ( rng ((Y |` f) | X)) c= Y by RELAT_1: 58, RELAT_1: 85;

      hence thesis by RELSET_1: 4;

    end;

    theorem :: PARTFUN1:15

    for f be PartFunc of X, Y st y in (f .: X) holds ex x be Element of X st x in ( dom f) & y = (f . x)

    proof

      let f be PartFunc of X, Y;

      assume y in (f .: X);

      then ex x be object st x in ( dom f) & x in X & y = (f . x) by FUNCT_1:def 6;

      hence thesis;

    end;

    theorem :: PARTFUN1:16

    

     Th16: for f be PartFunc of {x}, Y holds ( rng f) c= {(f . x)}

    proof

      let f be PartFunc of {x}, Y;

      ( dom f) = {} or ( dom f) = {x} by ZFMISC_1: 33;

      hence thesis by FUNCT_1: 4, RELAT_1: 42;

    end;

    theorem :: PARTFUN1:17

    for f be PartFunc of {x}, Y holds f is one-to-one

    proof

      let f be PartFunc of {x}, Y;

      let x1,x2 be object;

      assume that

       A1: x1 in ( dom f) and

       A2: x2 in ( dom f);

      ( dom f) <> {} implies x1 = x & x2 = x by A1, A2, TARSKI:def 1;

      hence thesis by A1;

    end;

    theorem :: PARTFUN1:18

    for f be PartFunc of {x}, Y holds (f .: P) c= {(f . x)}

    proof

      let f be PartFunc of {x}, Y;

      (f .: P) c= ( rng f) & ( rng f) c= {(f . x)} by Th16, RELAT_1: 111;

      hence thesis;

    end;

    theorem :: PARTFUN1:19

    for f be Function st ( dom f) = {x} & x in X & (f . x) in Y holds f is PartFunc of X, Y

    proof

      let f be Function;

      assume that

       A1: ( dom f) = {x} and

       A2: x in X and

       A3: (f . x) in Y;

      ( rng f) = {(f . x)} by A1, FUNCT_1: 4;

      then

       A4: ( rng f) c= Y by A3, ZFMISC_1: 31;

      ( dom f) c= X by A1, A2, ZFMISC_1: 31;

      hence thesis by A4, RELSET_1: 4;

    end;

    theorem :: PARTFUN1:20

    

     Th20: for f be PartFunc of X, {y} st x in ( dom f) holds (f . x) = y

    proof

      let f be PartFunc of X, {y};

      x in ( dom f) implies (f . x) in {y} by Th4;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: PARTFUN1:21

    for f1,f2 be PartFunc of X, {y} st ( dom f1) = ( dom f2) holds f1 = f2

    proof

      let f1,f2 be PartFunc of X, {y} such that

       A1: ( dom f1) = ( dom f2);

      for x be object holds x in ( dom f1) implies (f1 . x) = (f2 . x)

      proof

        let x be object;

        assume

         A2: x in ( dom f1);

        then (f1 . x) = y by Th20;

        hence thesis by A1, A2, Th20;

      end;

      hence thesis by A1;

    end;

    definition

      let f be Function;

      let X,Y be set;

      :: PARTFUN1:def1

      func <:f,X,Y:> -> PartFunc of X, Y equals ((Y |` f) | X);

      coherence by Th14;

    end

    theorem :: PARTFUN1:22

    

     Th22: for f be Function holds <:f, X, Y:> c= f

    proof

      let f be Function;

      ((Y |` f) | X) c= (Y |` f) & (Y |` f) c= f by RELAT_1: 59, RELAT_1: 86;

      hence thesis;

    end;

    theorem :: PARTFUN1:23

    

     Th23: for f be Function holds ( dom <:f, X, Y:>) c= ( dom f) & ( rng <:f, X, Y:>) c= ( rng f)

    proof

      let f be Function;

       <:f, X, Y:> c= f by Th22;

      hence thesis by RELAT_1: 11;

    end;

    theorem :: PARTFUN1:24

    

     Th24: for f be Function holds x in ( dom <:f, X, Y:>) iff x in ( dom f) & x in X & (f . x) in Y

    proof

      let f be Function;

      thus x in ( dom <:f, X, Y:>) implies x in ( dom f) & x in X & (f . x) in Y

      proof

        assume

         A1: x in ( dom <:f, X, Y:>);

        then x in (( dom (Y |` f)) /\ X) by RELAT_1: 61;

        then x in ( dom (Y |` f)) by XBOOLE_0:def 4;

        hence thesis by A1, FUNCT_1: 54;

      end;

      assume that

       A2: x in ( dom f) and

       A3: x in X and

       A4: (f . x) in Y;

      x in ( dom (Y |` f)) by A2, A4, FUNCT_1: 54;

      then x in (( dom (Y |` f)) /\ X) by A3, XBOOLE_0:def 4;

      hence thesis by RELAT_1: 61;

    end;

    theorem :: PARTFUN1:25

    

     Th25: for f be Function st x in ( dom f) & x in X & (f . x) in Y holds ( <:f, X, Y:> . x) = (f . x)

    proof

      let f be Function such that

       A1: x in ( dom f) and

       A2: x in X and

       A3: (f . x) in Y;

      x in ( dom (Y |` f)) by A1, A3, FUNCT_1: 54;

      

      then (f . x) = ((Y |` f) . x) by FUNCT_1: 55

      .= (((Y |` f) | X) . x) by A2, FUNCT_1: 49;

      hence thesis;

    end;

    theorem :: PARTFUN1:26

    

     Th26: for f be Function st x in ( dom <:f, X, Y:>) holds ( <:f, X, Y:> . x) = (f . x)

    proof

      let f be Function;

      assume

       A1: x in ( dom <:f, X, Y:>);

      then x in ( dom f) & (f . x) in Y by Th24;

      hence thesis by A1, Th25;

    end;

    theorem :: PARTFUN1:27

    for f,g be Function st f c= g holds <:f, X, Y:> c= <:g, X, Y:>

    proof

      let f,g be Function such that

       A1: f c= g;

      

       A2: ( dom <:f, X, Y:>) c= ( dom f) by Th23;

      now

        thus

         A3: ( dom <:f, X, Y:>) c= ( dom <:g, X, Y:>)

        proof

          let x be object;

          

           A4: ( dom f) c= ( dom g) by A1, RELAT_1: 11;

          assume

           A5: x in ( dom <:f, X, Y:>);

          then

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

          x in ( dom f) & (f . x) in Y by A5, Th24;

          hence thesis by A5, A4, A6, Th24;

        end;

        let x be object;

        assume

         A7: x in ( dom <:f, X, Y:>);

        then

         A8: ( <:f, X, Y:> . x) = (f . x) by Th26;

        ( <:g, X, Y:> . x) = (g . x) by A3, A7, Th26;

        hence ( <:f, X, Y:> . x) = ( <:g, X, Y:> . x) by A1, A2, A7, A8, GRFUNC_1: 2;

      end;

      hence thesis by GRFUNC_1: 2;

    end;

    theorem :: PARTFUN1:28

    

     Th28: for f be Function st Z c= X holds <:f, Z, Y:> c= <:f, X, Y:>

    proof

      let f be Function such that

       A1: Z c= X;

      

       A2: ( dom <:f, Z, Y:>) c= ( dom <:f, X, Y:>)

      proof

        let x be object;

        assume

         A3: x in ( dom <:f, Z, Y:>);

        then

         A4: (f . x) in Y by Th24;

        x in Z & x in ( dom f) by A3, Th24;

        hence thesis by A1, A4, Th24;

      end;

      now

        let x be object;

        assume

         A5: x in ( dom <:f, Z, Y:>);

        then ( <:f, Z, Y:> . x) = (f . x) by Th26;

        hence ( <:f, Z, Y:> . x) = ( <:f, X, Y:> . x) by A2, A5, Th26;

      end;

      hence thesis by A2, GRFUNC_1: 2;

    end;

    theorem :: PARTFUN1:29

    

     Th29: for f be Function st Z c= Y holds <:f, X, Z:> c= <:f, X, Y:>

    proof

      let f be Function such that

       A1: Z c= Y;

      

       A2: ( dom <:f, X, Z:>) c= ( dom <:f, X, Y:>)

      proof

        let x be object;

        assume

         A3: x in ( dom <:f, X, Z:>);

        then (f . x) in Z & x in ( dom f) by Th24;

        hence thesis by A1, A3, Th24;

      end;

      now

        let x be object;

        assume

         A4: x in ( dom <:f, X, Z:>);

        then ( <:f, X, Z:> . x) = (f . x) by Th26;

        hence ( <:f, X, Z:> . x) = ( <:f, X, Y:> . x) by A2, A4, Th26;

      end;

      hence thesis by A2, GRFUNC_1: 2;

    end;

    theorem :: PARTFUN1:30

    for f be Function st X1 c= X2 & Y1 c= Y2 holds <:f, X1, Y1:> c= <:f, X2, Y2:>

    proof

      let f be Function;

      assume X1 c= X2 & Y1 c= Y2;

      then <:f, X1, Y1:> c= <:f, X2, Y1:> & <:f, X2, Y1:> c= <:f, X2, Y2:> by Th28, Th29;

      hence thesis;

    end;

    theorem :: PARTFUN1:31

    

     Th31: for f be Function st ( dom f) c= X & ( rng f) c= Y holds f = <:f, X, Y:>

    proof

      let f be Function such that

       A1: ( dom f) c= X & ( rng f) c= Y;

      

       A2: ( dom f) c= ( dom <:f, X, Y:>)

      proof

        let x be object;

        assume

         A3: x in ( dom f);

        then (f . x) in ( rng f) by FUNCT_1:def 3;

        hence thesis by A1, A3, Th24;

      end;

      ( dom <:f, X, Y:>) c= ( dom f) by Th23;

      then

       A4: ( dom f) = ( dom <:f, X, Y:>) by A2;

      for x be object st x in ( dom f) holds (f . x) = ( <:f, X, Y:> . x) by A2, Th26;

      hence thesis by A4;

    end;

    theorem :: PARTFUN1:32

    for f be Function holds f = <:f, ( dom f), ( rng f):>;

    theorem :: PARTFUN1:33

    for f be PartFunc of X, Y holds <:f, X, Y:> = f;

    theorem :: PARTFUN1:34

    

     Th34: <: {} , X, Y:> = {}

    proof

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

      hence thesis by Th31;

    end;

    theorem :: PARTFUN1:35

    

     Th35: for f,g be Function holds ( <:g, Y, Z:> * <:f, X, Y:>) c= <:(g * f), X, Z:>

    proof

      let f,g be Function;

      

       A1: for x be object st x in ( dom ( <:g, Y, Z:> * <:f, X, Y:>)) holds (( <:g, Y, Z:> * <:f, X, Y:>) . x) = ( <:(g * f), X, Z:> . x)

      proof

        let x be object;

        assume

         A2: x in ( dom ( <:g, Y, Z:> * <:f, X, Y:>));

        then

         A3: x in ( dom <:f, X, Y:>) by FUNCT_1: 11;

        then

         A4: x in ( dom f) by Th24;

        ( <:f, X, Y:> . x) in ( dom <:g, Y, Z:>) by A2, FUNCT_1: 11;

        then

         A5: (f . x) in ( dom <:g, Y, Z:>) by A3, Th26;

        then (g . (f . x)) in Z by Th24;

        then

         A6: ((g * f) . x) in Z by A4, FUNCT_1: 13;

        (f . x) in ( dom g) by A5, Th24;

        then x in ( dom (g * f)) by A4, FUNCT_1: 11;

        then

         A7: x in ( dom <:(g * f), X, Z:>) by A2, A6, Th24;

        

        thus (( <:g, Y, Z:> * <:f, X, Y:>) . x) = ( <:g, Y, Z:> . ( <:f, X, Y:> . x)) by A2, FUNCT_1: 12

        .= ( <:g, Y, Z:> . (f . x)) by A3, Th26

        .= (g . (f . x)) by A5, Th26

        .= ((g * f) . x) by A4, FUNCT_1: 13

        .= ( <:(g * f), X, Z:> . x) by A7, Th26;

      end;

      ( dom ( <:g, Y, Z:> * <:f, X, Y:>)) c= ( dom <:(g * f), X, Z:>)

      proof

        let x be object;

        assume

         A8: x in ( dom ( <:g, Y, Z:> * <:f, X, Y:>));

        then

         A9: x in ( dom <:f, X, Y:>) by FUNCT_1: 11;

        then

         A10: x in ( dom f) by Th24;

        ( <:f, X, Y:> . x) in ( dom <:g, Y, Z:>) by A8, FUNCT_1: 11;

        then

         A11: (f . x) in ( dom <:g, Y, Z:>) by A9, Th26;

        then (g . (f . x)) in Z by Th24;

        then

         A12: ((g * f) . x) in Z by A10, FUNCT_1: 13;

        (f . x) in ( dom g) by A11, Th24;

        then x in ( dom (g * f)) by A10, FUNCT_1: 11;

        hence thesis by A8, A12, Th24;

      end;

      hence thesis by A1, GRFUNC_1: 2;

    end;

    theorem :: PARTFUN1:36

    for f,g be Function st (( rng f) /\ ( dom g)) c= Y holds ( <:g, Y, Z:> * <:f, X, Y:>) = <:(g * f), X, Z:>

    proof

      let f,g be Function such that

       A1: (( rng f) /\ ( dom g)) c= Y;

      

       A2: ( dom <:(g * f), X, Z:>) c= ( dom ( <:g, Y, Z:> * <:f, X, Y:>))

      proof

        let x be object;

        assume

         A3: x in ( dom <:(g * f), X, Z:>);

        then

         A4: x in ( dom (g * f)) by Th24;

        then

         A5: (f . x) in ( dom g) by FUNCT_1: 11;

        

         A6: x in ( dom f) by A4, FUNCT_1: 11;

        then (f . x) in ( rng f) by FUNCT_1:def 3;

        then

         A7: (f . x) in (( rng f) /\ ( dom g)) by A5, XBOOLE_0:def 4;

        ((g * f) . x) in Z by A3, Th24;

        then (g . (f . x)) in Z by A4, FUNCT_1: 12;

        then

         A8: (f . x) in ( dom <:g, Y, Z:>) by A1, A5, A7, Th24;

        x in ( dom <:f, X, Y:>) & ( <:f, X, Y:> . x) = (f . x) by A1, A3, A6, A7, Th24, Th25;

        hence thesis by A8, FUNCT_1: 11;

      end;

      for x be object st x in ( dom <:(g * f), X, Z:>) holds ( <:(g * f), X, Z:> . x) = (( <:g, Y, Z:> * <:f, X, Y:>) . x)

      proof

        let x be object;

        assume

         A9: x in ( dom <:(g * f), X, Z:>);

        then

         A10: x in ( dom (g * f)) by Th24;

        then

         A11: (f . x) in ( dom g) by FUNCT_1: 11;

        x in ( dom f) by A10, FUNCT_1: 11;

        then (f . x) in ( rng f) by FUNCT_1:def 3;

        then

         A12: (f . x) in (( rng f) /\ ( dom g)) by A11, XBOOLE_0:def 4;

        ((g * f) . x) in Z by A9, Th24;

        then (g . (f . x)) in Z by A10, FUNCT_1: 12;

        then

         A13: (f . x) in ( dom <:g, Y, Z:>) by A1, A11, A12, Th24;

        x in ( dom f) by A10, FUNCT_1: 11;

        then

         A14: x in ( dom <:f, X, Y:>) by A1, A9, A12, Th24;

        

        thus ( <:(g * f), X, Z:> . x) = ((g * f) . x) by A9, Th26

        .= (g . (f . x)) by A10, FUNCT_1: 12

        .= ( <:g, Y, Z:> . (f . x)) by A13, Th26

        .= ( <:g, Y, Z:> . ( <:f, X, Y:> . x)) by A14, Th26

        .= (( <:g, Y, Z:> * <:f, X, Y:>) . x) by A2, A9, FUNCT_1: 12;

      end;

      then

       A15: <:(g * f), X, Z:> c= ( <:g, Y, Z:> * <:f, X, Y:>) by A2, GRFUNC_1: 2;

      ( <:g, Y, Z:> * <:f, X, Y:>) c= <:(g * f), X, Z:> by Th35;

      hence thesis by A15;

    end;

    theorem :: PARTFUN1:37

    

     Th37: for f be Function st f is one-to-one holds <:f, X, Y:> is one-to-one

    proof

      let f be Function;

      assume f is one-to-one;

      then (Y |` f) is one-to-one by FUNCT_1: 58;

      hence thesis by FUNCT_1: 52;

    end;

    theorem :: PARTFUN1:38

    for f be Function st f is one-to-one holds ( <:f, X, Y:> " ) = <:(f " ), Y, X:>

    proof

      let f be Function;

      assume

       A1: f is one-to-one;

      then

       A2: <:f, X, Y:> is one-to-one by Th37;

      for y be object holds y in ( dom ( <:f, X, Y:> " )) iff y in ( dom <:(f " ), Y, X:>)

      proof

        let y be object;

        thus y in ( dom ( <:f, X, Y:> " )) implies y in ( dom <:(f " ), Y, X:>)

        proof

          assume y in ( dom ( <:f, X, Y:> " ));

          then

           A3: y in ( rng <:f, X, Y:>) by A2, FUNCT_1: 33;

          then

          consider x be object such that

           A4: x in ( dom <:f, X, Y:>) and

           A5: y = ( <:f, X, Y:> . x) by FUNCT_1:def 3;

          

           A6: (f . x) = y by A4, A5, Th26;

          then

           A7: y in Y by A4, Th24;

          ( rng <:f, X, Y:>) c= ( rng f) by Th23;

          then y in ( rng f) by A3;

          then

           A8: y in ( dom (f " )) by A1, FUNCT_1: 32;

          ( dom <:f, X, Y:>) c= ( dom f) by Th23;

          then ((f " ) . y) = x by A1, A4, A6, FUNCT_1: 32;

          hence thesis by A4, A8, A7, Th24;

        end;

        assume

         A9: y in ( dom <:(f " ), Y, X:>);

        ( dom <:(f " ), Y, X:>) c= ( dom (f " )) by Th23;

        then y in ( dom (f " )) by A9;

        then y in ( rng f) by A1, FUNCT_1: 33;

        then

        consider x be object such that

         A10: x in ( dom f) and

         A11: y = (f . x) by FUNCT_1:def 3;

        x = ((f " ) . (f . x)) by A1, A10, FUNCT_1: 34;

        then x in X by A9, A11, Th24;

        then x in ( dom <:f, X, Y:>) by A9, A10, A11, Th24;

        then ( <:f, X, Y:> . x) in ( rng <:f, X, Y:>) & ( <:f, X, Y:> . x) = (f . x) by Th26, FUNCT_1:def 3;

        hence thesis by A2, A11, FUNCT_1: 33;

      end;

      then

       A12: ( dom ( <:f, X, Y:> " )) = ( dom <:(f " ), Y, X:>) by TARSKI: 2;

      for y be object st y in ( dom <:(f " ), Y, X:>) holds ( <:(f " ), Y, X:> . y) = (( <:f, X, Y:> " ) . y)

      proof

        let y be object;

        

         A13: ( rng <:f, X, Y:>) c= ( rng f) by Th23;

        assume

         A14: y in ( dom <:(f " ), Y, X:>);

        then y in ( rng <:f, X, Y:>) by A2, A12, FUNCT_1: 33;

        then

        consider x be object such that

         A15: x in ( dom f) and

         A16: y = (f . x) by A13, FUNCT_1:def 3;

        

         A17: x = ((f " ) . (f . x)) by A1, A15, FUNCT_1: 34;

        then x in X by A14, A16, Th24;

        then x in ( dom <:f, X, Y:>) by A14, A15, A16, Th24;

        then (( <:f, X, Y:> " ) . ( <:f, X, Y:> . x)) = x & ( <:f, X, Y:> . x) = (f . x) by A2, Th26, FUNCT_1: 34;

        hence thesis by A14, A16, A17, Th26;

      end;

      hence thesis by A12;

    end;

    theorem :: PARTFUN1:39

    for f be Function holds (Z |` <:f, X, Y:>) = <:f, X, (Z /\ Y):>

    proof

      let f be Function;

      

      thus (Z |` <:f, X, Y:>) = (Z |` (Y |` (f | X))) by RELAT_1: 109

      .= ((Z /\ Y) |` (f | X)) by RELAT_1: 96

      .= <:f, X, (Z /\ Y):> by RELAT_1: 109;

    end;

    definition

      let X;

      let f be X -defined Relation;

      :: PARTFUN1:def2

      attr f is total means ( dom f) = X;

    end

    registration

      let X be empty set, Y be set;

      cluster -> total for Relation of X, Y;

      coherence ;

    end

    registration

      let X be non empty set, Y be empty set;

      cluster -> non total for Relation of X, Y;

      coherence ;

    end

    theorem :: PARTFUN1:40

    

     Th40: for f be Function st <:f, X, Y:> is total holds X c= ( dom f) by Th23;

    theorem :: PARTFUN1:41

     <: {} , X, Y:> is total implies X = {}

    proof

      ( dom {} ) = {} ;

      hence thesis by Th40, XBOOLE_1: 3;

    end;

    theorem :: PARTFUN1:42

    for f be Function st X c= ( dom f) & ( rng f) c= Y holds <:f, X, Y:> is total

    proof

      let f be Function such that

       A1: X c= ( dom f) and

       A2: ( rng f) c= Y;

      X c= ( dom <:f, X, Y:>)

      proof

        let x be object;

        assume

         A3: x in X;

        then (f . x) in ( rng f) by A1, FUNCT_1:def 3;

        hence thesis by A1, A2, A3, Th24;

      end;

      hence ( dom <:f, X, Y:>) = X;

    end;

    theorem :: PARTFUN1:43

    for f be Function st <:f, X, Y:> is total holds (f .: X) c= Y

    proof

      let f be Function such that

       A1: ( dom <:f, X, Y:>) = X;

      let y be object;

      

       A2: ( rng <:f, X, Y:>) c= Y by RELAT_1:def 19;

      assume y in (f .: X);

      then

      consider x be object such that x in ( dom f) and

       A3: x in X & y = (f . x) by FUNCT_1:def 6;

      ( <:f, X, Y:> . x) = y & ( <:f, X, Y:> . x) in ( rng <:f, X, Y:>) by A1, A3, Th26, FUNCT_1:def 3;

      hence thesis by A2;

    end;

    theorem :: PARTFUN1:44

    for f be Function st X c= ( dom f) & (f .: X) c= Y holds <:f, X, Y:> is total

    proof

      let f be Function such that

       A1: X c= ( dom f) and

       A2: (f .: X) c= Y;

      X c= ( dom <:f, X, Y:>)

      proof

        let x be object;

        assume

         A3: x in X;

        then (f . x) in (f .: X) by A1, FUNCT_1:def 6;

        hence thesis by A1, A2, A3, Th24;

      end;

      hence ( dom <:f, X, Y:>) = X;

    end;

    definition

      let X, Y;

      :: PARTFUN1:def3

      func PFuncs (X,Y) -> set means

      : Def3: x in it iff ex f be Function st x = f & ( dom f) c= X & ( rng f) c= Y;

      existence

      proof

        defpred P[ object] means ex f be Function st $1 = f & ( dom f) c= X & ( rng f) c= Y;

        consider F be set such that

         A1: for z be object holds z in F iff z in ( bool [:X, Y:]) & P[z] from XBOOLE_0:sch 1;

        take F;

        let z;

        thus z in F implies ex f be Function st z = f & ( dom f) c= X & ( rng f) c= Y by A1;

        given f be Function such that

         A2: z = f and

         A3: ( dom f) c= X & ( rng f) c= Y;

        f c= [:X, Y:]

        proof

          let x,y be object;

          assume

           A4: [x, y] in f;

          reconsider y as set by TARSKI: 1;

          

           A5: x in ( dom f) by XTUPLE_0:def 12, A4;

          then y = (f . x) by A4, FUNCT_1:def 2;

          then y in ( rng f) by A5, FUNCT_1:def 3;

          hence thesis by A3, A5, ZFMISC_1:def 2;

        end;

        hence thesis by A1, A2, A3;

      end;

      uniqueness

      proof

        let F1,F2 be set such that

         A6: x in F1 iff ex f be Function st x = f & ( dom f) c= X & ( rng f) c= Y and

         A7: x in F2 iff ex f be Function st x = f & ( dom f) c= X & ( rng f) c= Y;

        for x be object holds x in F1 iff x in F2

        proof

          let x be object;

          x in F1 iff ex f be Function st x = f & ( dom f) c= X & ( rng f) c= Y by A6;

          hence thesis by A7;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    registration

      let X, Y;

      cluster ( PFuncs (X,Y)) -> non empty;

      coherence

      proof

        ex f be Function st ( dom f) c= X & ( rng f) c= Y by Lm1;

        hence thesis by Def3;

      end;

    end

    theorem :: PARTFUN1:45

    

     Th45: for f be PartFunc of X, Y holds f in ( PFuncs (X,Y))

    proof

      let f be PartFunc of X, Y;

      ( dom f) c= X & ( rng f) c= Y by RELAT_1:def 19;

      hence thesis by Def3;

    end;

    theorem :: PARTFUN1:46

    

     Th46: for f be set st f in ( PFuncs (X,Y)) holds f is PartFunc of X, Y

    proof

      let f be set;

      assume f in ( PFuncs (X,Y));

      then ex F be Function st f = F & ( dom F) c= X & ( rng F) c= Y by Def3;

      hence thesis by RELSET_1: 4;

    end;

    theorem :: PARTFUN1:47

    for f be Element of ( PFuncs (X,Y)) holds f is PartFunc of X, Y by Th46;

    theorem :: PARTFUN1:48

    ( PFuncs ( {} ,Y)) = { {} }

    proof

      for x be object holds x in ( PFuncs ( {} ,Y)) iff x = {}

      proof

        let x be object;

        thus x in ( PFuncs ( {} ,Y)) implies x = {}

        proof

          assume x in ( PFuncs ( {} ,Y));

          then x is PartFunc of {} , Y by Th46;

          hence thesis;

        end;

         {} is PartFunc of {} , Y by RELSET_1: 12;

        hence thesis by Th45;

      end;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: PARTFUN1:49

    ( PFuncs (X, {} )) = { {} }

    proof

      for x be object holds x in ( PFuncs (X, {} )) iff x = {}

      proof

        let x be object;

        thus x in ( PFuncs (X, {} )) implies x = {}

        proof

          assume x in ( PFuncs (X, {} ));

          then x is PartFunc of X, {} by Th46;

          hence thesis;

        end;

         {} is PartFunc of X, {} by RELSET_1: 12;

        hence thesis by Th45;

      end;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: PARTFUN1:50

    X1 c= X2 & Y1 c= Y2 implies ( PFuncs (X1,Y1)) c= ( PFuncs (X2,Y2))

    proof

      assume

       A1: X1 c= X2 & Y1 c= Y2;

      let f be object;

      assume f in ( PFuncs (X1,Y1));

      then f is PartFunc of X1, Y1 by Th46;

      then f is PartFunc of X2, Y2 by A1, RELSET_1: 7;

      hence thesis by Th45;

    end;

    definition

      let f,g be Function;

      :: PARTFUN1:def4

      pred f tolerates g means for x be object st x in (( dom f) /\ ( dom g)) holds (f . x) = (g . x);

      reflexivity ;

      symmetry ;

    end

    theorem :: PARTFUN1:51

    

     Th51: for f,g be Function holds f tolerates g iff (f \/ g) is Function by Th1, Th2;

    theorem :: PARTFUN1:52

    

     Th52: for f,g be Function holds f tolerates g iff ex h be Function st f c= h & g c= h

    proof

      let f,g be Function;

      thus f tolerates g implies ex h be Function st f c= h & g c= h

      proof

        assume f tolerates g;

        then

        reconsider h = (f \/ g) as Function by Th1;

        take h;

        thus thesis by XBOOLE_1: 7;

      end;

      given h be Function such that

       A1: f c= h & g c= h;

      (f \/ g) is Function by A1, GRFUNC_1: 1, XBOOLE_1: 8;

      hence thesis by Th51;

    end;

    theorem :: PARTFUN1:53

    for f,g be Function st ( dom f) c= ( dom g) holds f tolerates g iff for x be object st x in ( dom f) holds (f . x) = (g . x)

    proof

      let f,g be Function;

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

      then (( dom f) /\ ( dom g)) = ( dom f) by XBOOLE_1: 28;

      hence thesis;

    end;

    theorem :: PARTFUN1:54

    for f,g be Function st f c= g holds f tolerates g by Th52;

    theorem :: PARTFUN1:55

    for f,g be Function st ( dom f) = ( dom g) & f tolerates g holds f = g;

    theorem :: PARTFUN1:56

    for f,g be Function st ( dom f) misses ( dom g) holds f tolerates g;

    theorem :: PARTFUN1:57

    for f,g,h be Function st f c= h & g c= h holds f tolerates g by Th52;

    theorem :: PARTFUN1:58

    for f,g be PartFunc of X, Y holds for h be Function st f tolerates h & g c= f holds g tolerates h

    proof

      let f,g be PartFunc of X, Y, h be Function such that

       A1: f tolerates h and

       A2: g c= f;

      

       A3: ( dom g) c= ( dom f) by A2, RELAT_1: 11;

      let x be object;

      assume

       A4: x in (( dom g) /\ ( dom h));

      then

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

      then

       A6: (f . x) = (g . x) by A2, GRFUNC_1: 2;

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

      then x in (( dom f) /\ ( dom h)) by A5, A3, XBOOLE_0:def 4;

      hence thesis by A1, A6;

    end;

    theorem :: PARTFUN1:59

    for f be Function holds {} tolerates f;

    theorem :: PARTFUN1:60

    for f be Function holds <: {} , X, Y:> tolerates f

    proof

      let f be Function;

       <: {} , X, Y:> = {} by Th34;

      hence thesis;

    end;

    theorem :: PARTFUN1:61

    for f,g be PartFunc of X, {y} holds f tolerates g

    proof

      let f,g be PartFunc of X, {y};

      let x be object;

      assume

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

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

      then

       A2: (f . x) = y by Th20;

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

      hence thesis by A2, Th20;

    end;

    theorem :: PARTFUN1:62

    for f be Function holds (f | X) tolerates f

    proof

      let f be Function;

      (f | X) c= f by RELAT_1: 59;

      hence thesis by Th52;

    end;

    theorem :: PARTFUN1:63

    for f be Function holds (Y |` f) tolerates f

    proof

      let f be Function;

      (Y |` f) c= f by RELAT_1: 86;

      hence thesis by Th52;

    end;

    theorem :: PARTFUN1:64

    

     Th64: for f be Function holds ((Y |` f) | X) tolerates f

    proof

      let f be Function;

      ((Y |` f) | X) c= (Y |` f) & (Y |` f) c= f by RELAT_1: 59, RELAT_1: 86;

      then ((Y |` f) | X) c= f;

      hence thesis by Th52;

    end;

    theorem :: PARTFUN1:65

    for f be Function holds <:f, X, Y:> tolerates f by Th64;

    theorem :: PARTFUN1:66

    

     Th66: for f,g be PartFunc of X, Y st f is total & g is total & f tolerates g holds f = g;

    theorem :: PARTFUN1:67

    

     Th67: for f,g,h be PartFunc of X, Y st f tolerates h & g tolerates h & h is total holds f tolerates g

    proof

      let f,g,h be PartFunc of X, Y such that

       A1: f tolerates h and

       A2: g tolerates h and

       A3: ( dom h) = X;

      let x be object;

      assume

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

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

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

      then

       A5: (f . x) = (h . x) by A1;

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

      then x in (( dom g) /\ ( dom h)) by A3, XBOOLE_0:def 4;

      hence thesis by A2, A5;

    end;

    theorem :: PARTFUN1:68

    

     Th68: for f,g be PartFunc of X, Y st (Y = {} implies X = {} ) & f tolerates g holds ex h be PartFunc of X, Y st h is total & f tolerates h & g tolerates h

    proof

      let f,g be PartFunc of X, Y such that

       A1: Y = {} implies X = {} and

       A2: f tolerates g;

      now

        per cases ;

          suppose

           A3: Y = {} ;

          then f tolerates <: {} , X, Y:> & g tolerates <: {} , X, Y:>;

          hence thesis by A1, A3;

        end;

          suppose

           A4: Y <> {} ;

          set y = the Element of Y;

          defpred P[ object, object] means ($1 in ( dom f) implies $2 = (f . $1)) & ($1 in ( dom g) implies $2 = (g . $1)) & ( not $1 in ( dom f) & not $1 in ( dom g) implies $2 = y);

          

           A5: for x be object st x in X holds ex y9 be object st P[x, y9]

          proof

            let x be object such that x in X;

            per cases ;

              suppose

               A6: x in ( dom f) & x in ( dom g);

              take y9 = (f . x);

              thus x in ( dom f) implies y9 = (f . x);

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

              hence x in ( dom g) implies y9 = (g . x) by A2;

              thus not x in ( dom f) & not x in ( dom g) implies y9 = y by A6;

            end;

              suppose

               A7: x in ( dom f) & not x in ( dom g);

              take y9 = (f . x);

              thus (x in ( dom f) implies y9 = (f . x)) & (x in ( dom g) implies y9 = (g . x)) & ( not x in ( dom f) & not x in ( dom g) implies y9 = y) by A7;

            end;

              suppose

               A8: not x in ( dom f) & x in ( dom g);

              take y9 = (g . x);

              thus (x in ( dom f) implies y9 = (f . x)) & (x in ( dom g) implies y9 = (g . x)) & ( not x in ( dom f) & not x in ( dom g) implies y9 = y) by A8;

            end;

              suppose not x in ( dom f) & not x in ( dom g);

              hence thesis;

            end;

          end;

          

           A9: for x,y1,y2 be object st x in X & P[x, y1] & P[x, y2] holds y1 = y2;

          consider h be Function such that

           A10: ( dom h) = X and

           A11: for x be object st x in X holds P[x, (h . x)] from FUNCT_1:sch 2( A9, A5);

          ( rng h) c= Y

          proof

            let z be object;

            assume z in ( rng h);

            then

            consider x be object such that

             A12: x in ( dom h) and

             A13: z = (h . x) by FUNCT_1:def 3;

            per cases ;

              suppose

               A14: x in ( dom f) & x in ( dom g);

              then z = (f . x) by A11, A13;

              hence thesis by A14, Th4;

            end;

              suppose

               A15: x in ( dom f) & not x in ( dom g);

              then z = (f . x) by A11, A13;

              hence thesis by A15, Th4;

            end;

              suppose

               A16: not x in ( dom f) & x in ( dom g);

              then z = (g . x) by A11, A13;

              hence thesis by A16, Th4;

            end;

              suppose not x in ( dom f) & not x in ( dom g);

              then z = y by A10, A11, A12, A13;

              hence thesis by A4;

            end;

          end;

          then

          reconsider h9 = h as PartFunc of X, Y by A10, RELSET_1: 4;

          

           A17: f tolerates h

          proof

            let x be object;

            assume x in (( dom f) /\ ( dom h));

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

            hence thesis by A11;

          end;

          

           A18: g tolerates h

          proof

            let x be object;

            assume x in (( dom g) /\ ( dom h));

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

            hence thesis by A11;

          end;

          h9 is total by A10;

          hence thesis by A17, A18;

        end;

      end;

      hence thesis;

    end;

    definition

      let X, Y;

      let f be PartFunc of X, Y;

      :: PARTFUN1:def5

      func TotFuncs f -> set means

      : Def5: for x be object holds x in it iff ex g be PartFunc of X, Y st g = x & g is total & f tolerates g;

      existence

      proof

        defpred P[ object] means ex g be PartFunc of X, Y st g = $1 & g is total & f tolerates g;

        now

          consider F be set such that

           A1: for x be object holds x in F iff x in ( PFuncs (X,Y)) & P[x] from XBOOLE_0:sch 1;

          take F;

          let x be object;

          thus x in F implies ex g be PartFunc of X, Y st g = x & g is total & f tolerates g by A1;

          given g be PartFunc of X, Y such that

           A2: g = x & g is total & f tolerates g;

          g in ( PFuncs (X,Y)) by Th45;

          hence x in F by A1, A2;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        defpred P[ object] means ex g be PartFunc of X, Y st g = $1 & g is total & f tolerates g;

        let F1,F2 be set such that

         A3: for x be object holds x in F1 iff P[x] and

         A4: for x be object holds x in F2 iff P[x];

        thus thesis from XBOOLE_0:sch 2( A3, A4);

      end;

    end

    theorem :: PARTFUN1:69

    

     Th69: for f be PartFunc of X, Y holds for g be set st g in ( TotFuncs f) holds g is PartFunc of X, Y

    proof

      let f be PartFunc of X, Y;

      let g be set;

      assume g in ( TotFuncs f);

      then ex g9 be PartFunc of X, Y st g9 = g & g9 is total & f tolerates g9 by Def5;

      hence thesis;

    end;

    theorem :: PARTFUN1:70

    

     Th70: for f,g be PartFunc of X, Y st g in ( TotFuncs f) holds g is total

    proof

      let f,g be PartFunc of X, Y;

      assume g in ( TotFuncs f);

      then ex g9 be PartFunc of X, Y st g9 = g & g9 is total & f tolerates g9 by Def5;

      hence thesis;

    end;

    theorem :: PARTFUN1:71

    

     Th71: for f be PartFunc of X, Y holds for g be Function st g in ( TotFuncs f) holds f tolerates g

    proof

      let f be PartFunc of X, Y;

      let g be Function;

      assume g in ( TotFuncs f);

      then ex g9 be PartFunc of X, Y st g9 = g & g9 is total & f tolerates g9 by Def5;

      hence thesis;

    end;

    registration

      let X be non empty set, Y be empty set;

      let f be PartFunc of X, Y;

      cluster ( TotFuncs f) -> empty;

      coherence

      proof

        set g = the Element of ( TotFuncs f);

        assume not ( TotFuncs f) is empty;

        then ex g9 be PartFunc of X, {} st g9 = g & g9 is total & f tolerates g9 by Def5;

        hence contradiction;

      end;

    end

    theorem :: PARTFUN1:72

    

     Th72: for f be PartFunc of X, Y holds f is total iff ( TotFuncs f) = {f}

    proof

      let f be PartFunc of X, Y;

      thus f is total implies ( TotFuncs f) = {f}

      proof

        assume

         A1: f is total;

        for g be object holds g in ( TotFuncs f) iff f = g

        proof

          let g be object;

          thus g in ( TotFuncs f) implies f = g

          proof

            assume g in ( TotFuncs f);

            then ex g9 be PartFunc of X, Y st g9 = g & g9 is total & f tolerates g9 by Def5;

            hence thesis by A1, Th66;

          end;

          thus thesis by A1, Def5;

        end;

        hence thesis by TARSKI:def 1;

      end;

      assume ( TotFuncs f) = {f};

      then f in ( TotFuncs f) by TARSKI:def 1;

      hence thesis by Th70;

    end;

    theorem :: PARTFUN1:73

    for f be PartFunc of {} , Y holds ( TotFuncs f) = {f} by Th72;

    theorem :: PARTFUN1:74

    for f be PartFunc of {} , Y holds ( TotFuncs f) = { {} } by Th72;

    theorem :: PARTFUN1:75

    for f,g be PartFunc of X, Y st ( TotFuncs f) meets ( TotFuncs g) holds f tolerates g

    proof

      let f,g be PartFunc of X, Y;

      set h = the Element of (( TotFuncs f) /\ ( TotFuncs g));

      assume

       A1: (( TotFuncs f) /\ ( TotFuncs g)) <> {} ;

      then

       A2: h in ( TotFuncs f) by XBOOLE_0:def 4;

      

       A3: h in ( TotFuncs g) by A1, XBOOLE_0:def 4;

      reconsider h as PartFunc of X, Y by A2, Th69;

      

       A4: g tolerates h by A3, Th71;

      f tolerates h by A2, Th71;

      hence thesis by A2, A4, Th67, Th70;

    end;

    theorem :: PARTFUN1:76

    for f,g be PartFunc of X, Y st (Y = {} implies X = {} ) & f tolerates g holds ( TotFuncs f) meets ( TotFuncs g)

    proof

      let f,g be PartFunc of X, Y;

      assume (Y = {} implies X = {} ) & f tolerates g;

      then

      consider h be PartFunc of X, Y such that

       A1: h is total & f tolerates h & g tolerates h by Th68;

      h in ( TotFuncs f) & h in ( TotFuncs g) by A1, Def5;

      hence (( TotFuncs f) /\ ( TotFuncs g)) <> {} by XBOOLE_0:def 4;

    end;

    begin

    

     Lm2: for R be Relation of X st R = ( id X) holds R is total;

    

     Lm3: for R be Relation st R = ( id X) holds R is reflexive symmetric antisymmetric transitive

    proof

      let R be Relation;

      assume

       A1: R = ( id X);

      thus R is_reflexive_in ( field R) by A1, RELAT_1:def 10;

      thus R is_symmetric_in ( field R) by A1, RELAT_1:def 10;

      thus R is_antisymmetric_in ( field R) by A1, RELAT_1:def 10;

      thus R is_transitive_in ( field R) by A1, RELAT_1:def 10;

    end;

    

     Lm4: ( id X) is Relation of X

    proof

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

      hence thesis by RELSET_1: 4;

    end;

    registration

      let X;

      cluster total reflexive symmetric antisymmetric transitive for Relation of X;

      existence

      proof

        reconsider R = ( id X) as Relation of X by Lm4;

        take R;

        thus thesis by Lm3;

      end;

    end

    registration

      cluster symmetric transitive -> reflexive for Relation;

      coherence

      proof

        let R be Relation;

        assume that

         A1: R is_symmetric_in ( field R) and

         A2: R is_transitive_in ( field R);

        let x be object;

        assume

         A3: x in ( field R);

        then x in ( dom R) or x in ( rng R) by XBOOLE_0:def 3;

        then

        consider y be object such that

         A4: [x, y] in R or [y, x] in R by XTUPLE_0:def 12, XTUPLE_0:def 13;

        y in ( rng R) or y in ( dom R) by A4, XTUPLE_0:def 12, XTUPLE_0:def 13;

        then

         A5: y in ( field R) by XBOOLE_0:def 3;

        then [x, y] in R & [y, x] in R by A1, A3, A4;

        hence thesis by A2, A3, A5;

      end;

    end

    registration

      let X;

      cluster ( id X) -> symmetric antisymmetric transitive;

      coherence by Lm3;

    end

    definition

      let X;

      :: original: id

      redefine

      func id X -> total Relation of X ;

      coherence by Lm2, Lm4;

    end

    scheme :: PARTFUN1:sch4

    LambdaC9 { A() -> non empty set , C[ object], F,G( object) -> object } :

ex f be Function st ( dom f) = A() & for x be Element of A() holds (C[x] implies (f . x) = F(x)) & ( not C[x] implies (f . x) = G(x));

      consider f be Function such that

       A1: ( dom f) = A() & for x be object st x in A() holds (C[x] implies (f . x) = F(x)) & ( not C[x] implies (f . x) = G(x)) from LambdaC;

      take f;

      thus thesis by A1;

    end;

    begin

    reserve A for set,

f,g,h for Function;

    theorem :: PARTFUN1:77

    

     Th77: for x,y,z be object holds f tolerates g & [x, y] in f & [x, z] in g implies y = z

    proof

      let x,y,z be object;

      set h = (f \/ g);

      assume f tolerates g;

      then

       A1: h is Function by Th51;

      assume [x, y] in f & [x, z] in g;

      then [x, y] in h & [x, z] in h by XBOOLE_0:def 3;

      hence thesis by A1, FUNCT_1:def 1;

    end;

    theorem :: PARTFUN1:78

    A is functional & (for f,g be Function st f in A & g in A holds f tolerates g) implies ( union A) is Function

    proof

      assume that

       A1: for x st x in A holds x is Function and

       A2: for f,g be Function st f in A & g in A holds f tolerates g;

       A3:

      now

        let x,y,z be object;

        assume that

         A4: [x, y] in ( union A) and

         A5: [x, z] in ( union A);

        consider p be set such that

         A6: [x, y] in p and

         A7: p in A by A4, TARSKI:def 4;

        consider q be set such that

         A8: [x, z] in q and

         A9: q in A by A5, TARSKI:def 4;

        reconsider p, q as Function by A1, A7, A9;

        p tolerates q by A2, A7, A9;

        hence y = z by A6, A8, Th77;

      end;

      now

        let z be object;

        assume z in ( union A);

        then

        consider p be set such that

         A10: z in p and

         A11: p in A by TARSKI:def 4;

        reconsider p as Function by A1, A11;

        p = p;

        hence ex x,y be object st [x, y] = z by A10, RELAT_1:def 1;

      end;

      hence thesis by A3, FUNCT_1:def 1, RELAT_1:def 1;

    end;

    definition

      let D be set, p be D -valued Function, i be object;

      assume

       A1: i in ( dom p);

      :: PARTFUN1:def6

      func p /. i -> Element of D equals

      : Def6: (p . i);

      coherence by A1, Th4;

    end

    registration

      let X,Y be non empty set;

      cluster non empty for PartFunc of X, Y;

      existence

      proof

        reconsider p = { [ the Element of X, the Element of Y]} as PartFunc of X, Y by RELSET_1: 3;

        take p;

        thus thesis;

      end;

    end

    registration

      let A,B be set;

      cluster ( PFuncs (A,B)) -> functional;

      coherence

      proof

        let x be object;

        assume x in ( PFuncs (A,B));

        then ex f be Function st x = f & ( dom f) c= A & ( rng f) c= B by Def3;

        hence thesis;

      end;

    end

    theorem :: PARTFUN1:79

    for f1,f2,g be Function st ( rng g) c= ( dom f1) & ( rng g) c= ( dom f2) & f1 tolerates f2 holds (f1 * g) = (f2 * g)

    proof

      let f1,f2,g be Function;

      assume that

       A1: ( rng g) c= ( dom f1) and

       A2: ( rng g) c= ( dom f2) and

       A3: f1 tolerates f2;

      

       A4: ( dom (f2 * g)) = ( dom g) by A2, RELAT_1: 27;

      

       A5: ( dom (f1 * g)) = ( dom g) by A1, RELAT_1: 27;

      now

        let x be object;

        assume

         A6: x in ( dom g);

        then

         A7: ((f2 * g) . x) = (f2 . (g . x)) by A4, FUNCT_1: 12;

        (g . x) in ( rng g) by A6, FUNCT_1:def 3;

        then

         A8: (g . x) in (( dom f1) /\ ( dom f2)) by A1, A2, XBOOLE_0:def 4;

        ((f1 * g) . x) = (f1 . (g . x)) by A5, A6, FUNCT_1: 12;

        hence ((f1 * g) . x) = ((f2 * g) . x) by A3, A7, A8;

      end;

      hence thesis by A5, A4;

    end;

    theorem :: PARTFUN1:80

    for f be Y -valued Function st x in ( dom (f | X)) holds ((f | X) /. x) = (f /. x)

    proof

      let f be Y -valued Function;

      assume

       A1: x in ( dom (f | X));

      then

       A2: x in ( dom f) by RELAT_1: 57;

      

      thus ((f | X) /. x) = ((f | X) . x) by A1, Def6

      .= (f . x) by A1, FUNCT_1: 47

      .= (f /. x) by A2, Def6;

    end;

    scheme :: PARTFUN1:sch5

    LambdaCS { A() -> set , C[ object], F,G( object) -> object } :

ex f be Function st ( dom f) = A() & for x be set st x in A() holds (C[x] implies (f . x) = F(x)) & ( not C[x] implies (f . x) = G(x));

      consider f be Function such that

       A1: ( dom f) = A() and

       A2: for x be object st x in A() holds (C[x] implies (f . x) = F(x)) & ( not C[x] implies (f . x) = G(x)) from LambdaC;

      take f;

      thus thesis by A1, A2;

    end;

    theorem :: PARTFUN1:81

    for f,g be Function st (f . x) = (g . x) holds (f | {x}) tolerates (g | {x})

    proof

      let f,g be Function such that

       A1: (f . x) = (g . x);

      let a be object;

      set F = (f | {x}), G = (g | {x});

      assume a in (( dom F) /\ ( dom G));

      then a in ( dom F) by XBOOLE_0:def 4;

      then

       A2: a in {x} by RELAT_1: 57;

      then a = x by TARSKI:def 1;

      

      hence (G . a) = (f . a) by A1, A2, FUNCT_1: 49

      .= (F . a) by A2, FUNCT_1: 49;

    end;

    theorem :: PARTFUN1:82

    for f,g be Function st (f . x) = (g . x) & (f . y) = (g . y) holds (f | {x, y}) tolerates (g | {x, y})

    proof

      let f,g be Function such that

       A1: (f . x) = (g . x) & (f . y) = (g . y);

      let a be object;

      set F = (f | {x, y}), G = (g | {x, y});

      assume a in (( dom F) /\ ( dom G));

      then a in ( dom F) by XBOOLE_0:def 4;

      then

       A2: a in {x, y} by RELAT_1: 57;

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

      

      hence (G . a) = (f . a) by A1, A2, FUNCT_1: 49

      .= (F . a) by A2, FUNCT_1: 49;

    end;

    definition

      let A,B be set;

      let F be ( PFuncs (A,B)) -valued Function;

      let i be object;

      :: original: .

      redefine

      func F . i -> PartFunc of A, B ;

      coherence

      proof

        per cases ;

          suppose i in ( dom F);

          then

           A1: (F . i) in ( rng F) by FUNCT_1:def 3;

          ( rng F) c= ( PFuncs (A,B)) by RELAT_1:def 19;

          hence thesis by A1, Th46;

        end;

          suppose not i in ( dom F);

          then (F . i) = {} by FUNCT_1:def 2;

          hence thesis by RELSET_1: 12;

        end;

      end;

    end