funct_4.miz



    begin

    reserve a,b,p,x,x9,x1,x19,x2,y,y9,y1,y19,y2,z,z9,z1,z2 for object,

X,X9,Y,Y9,Z,Z9 for set;

    reserve A,D,D9 for non empty set;

    reserve f,g,h for Function;

    

     Lm1: for x,y,x1,y1,x9,y9,x19,y19 be object holds [ [x, x9], [y, y9]] = [ [x1, x19], [y1, y19]] implies x = x1 & y = y1 & x9 = x19 & y9 = y19

    proof

      let x,y,x1,y1,x9,y9,x19,y19 be object;

      assume [ [x, x9], [y, y9]] = [ [x1, x19], [y1, y19]];

      then [x, x9] = [x1, x19] & [y, y9] = [y1, y19] by XTUPLE_0: 1;

      hence thesis by XTUPLE_0: 1;

    end;

    theorem :: FUNCT_4:1

    

     Th1: (for z be object st z in Z holds ex x,y be object st z = [x, y]) implies ex X, Y st Z c= [:X, Y:]

    proof

      assume

       A1: for z be object st z in Z holds ex x,y be object st z = [x, y];

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

      consider X such that

       A2: for x be object holds x in X iff x in ( union ( union Z)) & P[x] from XBOOLE_0:sch 1;

      defpred P[ object] means ex x be object st [x, $1] in Z;

      consider Y such that

       A3: for y be object holds y in Y iff y in ( union ( union Z)) & P[y] from XBOOLE_0:sch 1;

      take X, Y;

      let z be object;

      assume

       A4: z in Z;

      then

      consider x,y be object such that

       A5: z = [x, y] by A1;

      x in ( union ( union Z)) by A4, A5, ZFMISC_1: 134;

      then

       A6: x in X by A2, A4, A5;

      y in ( union ( union Z)) by A4, A5, ZFMISC_1: 134;

      then y in Y by A3, A4, A5;

      hence thesis by A5, A6, ZFMISC_1: 87;

    end;

    theorem :: FUNCT_4:2

    (g * f) = ((g | ( rng f)) * f)

    proof

      for x be object holds x in ( dom (g * f)) iff x in ( dom ((g | ( rng f)) * f))

      proof

        let x be object;

        

         A1: ( dom (g | ( rng f))) = (( dom g) /\ ( rng f)) by RELAT_1: 61;

        thus x in ( dom (g * f)) implies x in ( dom ((g | ( rng f)) * f))

        proof

          assume

           A2: x in ( dom (g * f));

          then

           A3: x in ( dom f) by FUNCT_1: 11;

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

          then

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

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

          then (f . x) in ( dom (g | ( rng f))) by A1, A4, XBOOLE_0:def 4;

          hence thesis by A3, FUNCT_1: 11;

        end;

        assume

         A5: x in ( dom ((g | ( rng f)) * f));

        then (f . x) in ( dom (g | ( rng f))) by FUNCT_1: 11;

        then

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

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

        hence thesis by A6, FUNCT_1: 11;

      end;

      then

       A7: ( dom (g * f)) = ( dom ((g | ( rng f)) * f)) by TARSKI: 2;

      for x be object holds x in ( dom (g * f)) implies ((g * f) . x) = (((g | ( rng f)) * f) . x)

      proof

        let x be object;

        assume

         A8: x in ( dom (g * f));

        then

         A9: x in ( dom f) by FUNCT_1: 11;

        then

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

        

        thus ((g * f) . x) = (g . (f . x)) by A8, FUNCT_1: 12

        .= ((g | ( rng f)) . (f . x)) by A10, FUNCT_1: 49

        .= (((g | ( rng f)) * f) . x) by A9, FUNCT_1: 13;

      end;

      hence thesis by A7;

    end;

    theorem :: FUNCT_4:3

    ( id X) c= ( id Y) iff X c= Y

    proof

      thus ( id X) c= ( id Y) implies X c= Y

      proof

        assume

         A1: ( id X) c= ( id Y);

        let x be object;

        assume x in X;

        then [x, x] in ( id X) by RELAT_1:def 10;

        hence thesis by A1, RELAT_1:def 10;

      end;

      assume

       A2: X c= Y;

      let z be object;

      assume

       A3: z in ( id X);

      then

      consider x,x9 be object such that

       A4: x in X and x9 in X and

       A5: z = [x, x9] by ZFMISC_1: 84;

      x = x9 by A3, A5, RELAT_1:def 10;

      hence thesis by A2, A4, A5, RELAT_1:def 10;

    end;

    theorem :: FUNCT_4:4

    X c= Y implies (X --> a) c= (Y --> a)

    proof

      assume

       A2: X c= Y;

       A3:

      now

        let x be object;

        assume

         A4: x in ( dom (X --> a));

        then ((X --> a) . x) = a by FUNCOP_1: 7;

        hence ((X --> a) . x) = ((Y --> a) . x) by A2, A4, FUNCOP_1: 7;

      end;

      ( dom (Y --> a)) = Y;

      hence thesis by A2, A3, GRFUNC_1: 2;

    end;

    theorem :: FUNCT_4:5

    

     Th5: for a,b be object holds (X --> a) c= (Y --> b) implies X c= Y

    proof

      let a,b be object;

      assume (X --> a) c= (Y --> b);

      then

       A1: ( dom (X --> a)) c= ( dom (Y --> b)) by RELAT_1: 11;

      thus thesis by A1;

    end;

    theorem :: FUNCT_4:6

    for a,b be object holds X <> {} & (X --> a) c= (Y --> b) implies a = b

    proof

      let a,b be object;

      assume

       A1: X <> {} ;

      set x = the Element of X;

      assume

       A2: (X --> a) c= (Y --> b);

      then X c= Y by Th5;

      then x in Y by A1;

      then

       A3: ((Y --> b) . x) = b by FUNCOP_1: 7;

      ( dom (X --> a)) = X & ((X --> a) . x) = a by A1, FUNCOP_1: 7;

      hence thesis by A1, A2, A3, GRFUNC_1: 2;

    end;

    theorem :: FUNCT_4:7

    x in ( dom f) implies (x .--> (f . x)) c= f

    proof

       A1:

      now

        let y be object;

        assume y in ( dom (x .--> (f . x)));

        then x = y by FUNCOP_1: 75;

        hence ((x .--> (f . x)) . y) = (f . y) by FUNCOP_1: 72;

      end;

      assume

       A2: x in ( dom f);

      ( dom (x .--> (f . x))) c= ( dom f) by A2, FUNCOP_1: 75;

      hence thesis by A1, GRFUNC_1: 2;

    end;

    theorem :: FUNCT_4:8

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

    proof

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

      hence thesis;

    end;

    theorem :: FUNCT_4:9

    f c= g implies ((Y |` f) | X) c= ((Y |` g) | X)

    proof

      assume f c= g;

      then (Y |` f) c= (Y |` g) by RELAT_1: 101;

      hence thesis by RELAT_1: 76;

    end;

    definition

      let f, g;

      :: FUNCT_4:def1

      func f +* g -> Function means

      : Def1: ( dom it ) = (( dom f) \/ ( dom g)) & for x be object st x in (( dom f) \/ ( dom g)) holds (x in ( dom g) implies (it . x) = (g . x)) & ( not x in ( dom g) implies (it . x) = (f . x));

      existence

      proof

        deffunc G( object) = (f . $1);

        deffunc F( object) = (g . $1);

        defpred P[ object] means $1 in ( dom g);

        thus ex F be Function st ( dom F) = (( dom f) \/ ( dom g)) & for x be object st x in (( dom f) \/ ( dom g)) holds ( P[x] implies (F . x) = F(x)) & ( not P[x] implies (F . x) = G(x)) from PARTFUN1:sch 1;

      end;

      uniqueness

      proof

        let h1,h2 be Function such that

         A1: ( dom h1) = (( dom f) \/ ( dom g)) and

         A2: for x be object st x in (( dom f) \/ ( dom g)) holds (x in ( dom g) implies (h1 . x) = (g . x)) & ( not x in ( dom g) implies (h1 . x) = (f . x)) and

         A3: ( dom h2) = (( dom f) \/ ( dom g)) and

         A4: for x be object st x in (( dom f) \/ ( dom g)) holds (x in ( dom g) implies (h2 . x) = (g . x)) & ( not x in ( dom g) implies (h2 . x) = (f . x));

        for x be object st x in (( dom f) \/ ( dom g)) holds (h1 . x) = (h2 . x)

        proof

          let x be object;

          assume

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

          then

           A6: not x in ( dom g) implies (h1 . x) = (f . x) & (h2 . x) = (f . x) by A2, A4;

          x in ( dom g) implies (h1 . x) = (g . x) & (h2 . x) = (g . x) by A2, A4, A5;

          hence thesis by A6;

        end;

        hence thesis by A1, A3;

      end;

      idempotence ;

    end

    theorem :: FUNCT_4:10

    

     Th10: ( dom f) c= ( dom (f +* g)) & ( dom g) c= ( dom (f +* g))

    proof

      ( dom (f +* g)) = (( dom f) \/ ( dom g)) by Def1;

      hence thesis by XBOOLE_1: 7;

    end;

    theorem :: FUNCT_4:11

    

     Th11: for x be object holds not x in ( dom g) implies ((f +* g) . x) = (f . x)

    proof

      let x be object;

      assume

       A1: not x in ( dom g);

      per cases ;

        suppose x in ( dom f);

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

        hence thesis by A1, Def1;

      end;

        suppose

         A2: not x in ( dom f);

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

        then not x in ( dom (f +* g)) by Def1;

        

        hence ((f +* g) . x) = {} by FUNCT_1:def 2

        .= (f . x) by A2, FUNCT_1:def 2;

      end;

    end;

    theorem :: FUNCT_4:12

    

     Th12: for x be object holds x in ( dom (f +* g)) iff x in ( dom f) or x in ( dom g)

    proof

      let x be object;

      x in ( dom (f +* g)) iff x in (( dom f) \/ ( dom g)) by Def1;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: FUNCT_4:13

    

     Th13: for x be object holds x in ( dom g) implies ((f +* g) . x) = (g . x)

    proof

      let x be object;

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

      hence thesis by Def1;

    end;

    theorem :: FUNCT_4:14

    

     Th14: ((f +* g) +* h) = (f +* (g +* h))

    proof

       A1:

      now

        let x be object such that x in (( dom f) \/ ( dom (g +* h)));

        hereby

          assume

           A2: x in ( dom (g +* h));

          per cases by A2, Th12;

            suppose

             A3: x in ( dom g) & not x in ( dom h);

            

            hence (((f +* g) +* h) . x) = ((f +* g) . x) by Th11

            .= (g . x) by A3, Th13

            .= ((g +* h) . x) by A3, Th11;

          end;

            suppose

             A4: x in ( dom h);

            

            hence (((f +* g) +* h) . x) = (h . x) by Th13

            .= ((g +* h) . x) by A4, Th13;

          end;

        end;

        assume

         A5: not x in ( dom (g +* h));

        then

         A6: not x in ( dom g) by Th12;

         not x in ( dom h) by A5, Th12;

        

        hence (((f +* g) +* h) . x) = ((f +* g) . x) by Th11

        .= (f . x) by A6, Th11;

      end;

      ( dom ((f +* g) +* h)) = (( dom (f +* g)) \/ ( dom h)) by Def1

      .= ((( dom f) \/ ( dom g)) \/ ( dom h)) by Def1

      .= (( dom f) \/ (( dom g) \/ ( dom h))) by XBOOLE_1: 4

      .= (( dom f) \/ ( dom (g +* h))) by Def1;

      hence thesis by A1, Def1;

    end;

    theorem :: FUNCT_4:15

    

     Th15: f tolerates g & x in ( dom f) implies ((f +* g) . x) = (f . x)

    proof

      assume that

       A1: f tolerates g and

       A2: x in ( dom f);

      now

        per cases ;

          suppose x in ( dom g);

          then x in (( dom f) /\ ( dom g)) & ((f +* g) . x) = (g . x) by A2, Th13, XBOOLE_0:def 4;

          hence thesis by A1;

        end;

          suppose not x in ( dom g);

          hence thesis by Th11;

        end;

      end;

      hence thesis;

    end;

    theorem :: FUNCT_4:16

    ( dom f) misses ( dom g) & x in ( dom f) implies ((f +* g) . x) = (f . x)

    proof

      assume (( dom f) /\ ( dom g)) = {} & x in ( dom f);

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

      hence thesis by Th11;

    end;

    theorem :: FUNCT_4:17

    

     Th17: ( rng (f +* g)) c= (( rng f) \/ ( rng g))

    proof

      let y be object;

      assume y in ( rng (f +* g));

      then

      consider x be object such that

       A1: x in ( dom (f +* g)) and

       A2: y = ((f +* g) . x) by FUNCT_1:def 3;

      x in ( dom f) & not x in ( dom g) or x in ( dom g) by A1, Th12;

      then x in ( dom f) & ((f +* g) . x) = (f . x) or x in ( dom g) & ((f +* g) . x) = (g . x) by Th11, Th13;

      then y in ( rng f) or y in ( rng g) by A2, FUNCT_1:def 3;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: FUNCT_4:18

    ( rng g) c= ( rng (f +* g))

    proof

      let y be object;

      assume y in ( rng g);

      then

      consider x be object such that

       A1: x in ( dom g) & y = (g . x) by FUNCT_1:def 3;

      x in ( dom (f +* g)) & ((f +* g) . x) = y by A1, Th12, Th13;

      hence thesis by FUNCT_1:def 3;

    end;

    theorem :: FUNCT_4:19

    

     Th19: ( dom f) c= ( dom g) implies (f +* g) = g

    proof

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

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

      then ( dom (f +* g)) = ( dom g) & for x be object st x in ( dom g) holds ((f +* g) . x) = (g . x) by Def1;

      hence thesis;

    end;

    registration

      let f;

      let g be empty Function;

      reduce (g +* f) to f;

      reducibility

      proof

        ( dom g) c= ( dom f);

        hence thesis by Th19;

      end;

      reduce (f +* g) to f;

      reducibility

      proof

        

         A1: for x be object st x in ( dom f) holds ((f +* g) . x) = (f . x)

        proof

          let x be object;

          assume x in ( dom f);

          then x in (( dom f) \ ( dom g));

          hence thesis by Th11;

        end;

        (( dom f) \/ ( dom g)) = ( dom f);

        then ( dom (f +* g)) = ( dom f) by Def1;

        hence thesis by A1;

      end;

    end

    theorem :: FUNCT_4:20

    ( {} +* f) = f;

    theorem :: FUNCT_4:21

    (f +* {} ) = f;

    theorem :: FUNCT_4:22

    (( id X) +* ( id Y)) = ( id (X \/ Y))

    proof

      

       A1: for x be object holds x in ( dom ( id (X \/ Y))) implies ((( id X) +* ( id Y)) . x) = (( id (X \/ Y)) . x)

      proof

        let x be object;

        assume

         A2: x in ( dom ( id (X \/ Y)));

        now

          per cases ;

            suppose

             A3: x in Y;

            ( dom ( id Y)) = Y;

            

            hence ((( id X) +* ( id Y)) . x) = (( id Y) . x) by A3, Th13

            .= x by A3, FUNCT_1: 18

            .= (( id (X \/ Y)) . x) by A2, FUNCT_1: 18;

          end;

            suppose

             A4: not x in Y;

            then

             A5: x in X by A2, XBOOLE_0:def 3;

             not x in ( dom ( id Y)) by A4;

            

            hence ((( id X) +* ( id Y)) . x) = (( id X) . x) by Th11

            .= x by A5, FUNCT_1: 18

            .= (( id (X \/ Y)) . x) by A2, FUNCT_1: 18;

          end;

        end;

        hence thesis;

      end;

      ( dom (( id X) +* ( id Y))) = (( dom ( id X)) \/ ( dom ( id Y))) by Def1

      .= (X \/ ( dom ( id Y)))

      .= (X \/ Y)

      .= ( dom ( id (X \/ Y)));

      hence thesis by A1;

    end;

    theorem :: FUNCT_4:23

    

     Th23: ((f +* g) | ( dom g)) = g

    proof

      (( dom f) \/ ( dom g)) = ( dom (f +* g)) by Def1;

      then

       A1: ( dom ((f +* g) | ( dom g))) = ( dom g) by RELAT_1: 62, XBOOLE_1: 7;

      for x be object st x in ( dom g) holds (((f +* g) | ( dom g)) . x) = (g . x)

      proof

        let x be object;

        x in ( dom g) implies ((f +* g) . x) = (g . x) by Th13;

        hence thesis by A1, FUNCT_1: 47;

      end;

      hence thesis by A1;

    end;

    registration

      let f,g be Function;

      reduce ((f +* g) | ( dom g)) to g;

      reducibility by Th23;

    end

    theorem :: FUNCT_4:24

    

     Th24: ((f +* g) | (( dom f) \ ( dom g))) c= f

    proof

      

       A1: for x be object st x in ( dom ((f +* g) | (( dom f) \ ( dom g)))) holds (((f +* g) | (( dom f) \ ( dom g))) . x) = (f . x)

      proof

        let x be object such that

         A2: x in ( dom ((f +* g) | (( dom f) \ ( dom g))));

        ( dom ((f +* g) | (( dom f) \ ( dom g)))) c= (( dom f) \ ( dom g)) by RELAT_1: 58;

        then not x in ( dom g) by A2, XBOOLE_0:def 5;

        then ((f +* g) . x) = (f . x) by Th11;

        hence thesis by A2, FUNCT_1: 47;

      end;

      ( dom ((f +* g) | (( dom f) \ ( dom g)))) c= (( dom f) \ ( dom g)) by RELAT_1: 58;

      then ( dom ((f +* g) | (( dom f) \ ( dom g)))) c= ( dom f) by XBOOLE_1: 1;

      hence thesis by A1, GRFUNC_1: 2;

    end;

    theorem :: FUNCT_4:25

    

     Th25: g c= (f +* g)

    proof

      ( dom (f +* g)) = (( dom f) \/ ( dom g)) by Def1;

      then

       A1: ( dom g) c= ( dom (f +* g)) by XBOOLE_1: 7;

      for x be object st x in ( dom g) holds ((f +* g) . x) = (g . x) by Th13;

      hence thesis by A1, GRFUNC_1: 2;

    end;

    theorem :: FUNCT_4:26

    f tolerates (g +* h) implies (f | (( dom f) \ ( dom h))) tolerates g

    proof

      assume

       A1: f tolerates (g +* h);

      let x be object;

      assume

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

      then

       A3: x in ( dom (f | (( dom f) \ ( dom h)))) by XBOOLE_0:def 4;

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

      then

       A4: x in ( dom (g +* h)) by Th12;

      

       A5: ( dom (f | (( dom f) \ ( dom h)))) c= (( dom f) \ ( dom h)) by RELAT_1: 58;

      then x in ( dom f) by A3, XBOOLE_0:def 5;

      then

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

       not x in ( dom h) by A3, A5, XBOOLE_0:def 5;

      then ((g +* h) . x) = (g . x) by Th11;

      then (f . x) = (g . x) by A1, A6;

      hence thesis by A3, A5, FUNCT_1: 49;

    end;

    theorem :: FUNCT_4:27

    

     Th27: f tolerates (g +* h) implies f tolerates h

    proof

      assume

       A1: f tolerates (g +* h);

      let x be object;

      assume

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

      then

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

      

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

      then x in ( dom (g +* h)) by Th12;

      then

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

      ((g +* h) . x) = (h . x) by A4, Th13;

      hence thesis by A1, A5;

    end;

    theorem :: FUNCT_4:28

    

     Th28: f tolerates g iff f c= (f +* g)

    proof

      thus f tolerates g implies f c= (f +* g)

      proof

        (( dom f) \/ ( dom g)) = ( dom (f +* g)) by Def1;

        then

         A1: ( dom f) c= ( dom (f +* g)) by XBOOLE_1: 7;

        assume f tolerates g;

        then for x be object st x in ( dom f) holds ((f +* g) . x) = (f . x) by Th15;

        hence thesis by A1, GRFUNC_1: 2;

      end;

      thus thesis by Th27, PARTFUN1: 54;

    end;

    theorem :: FUNCT_4:29

    

     Th29: (f +* g) c= (f \/ g)

    proof

      let p be object;

      assume

       A1: p in (f +* g);

      then

      consider x,y be object such that

       A2: p = [x, y] by RELAT_1:def 1;

      x in ( dom (f +* g)) by A1, A2, FUNCT_1: 1;

      then x in ( dom f) & not x in ( dom g) or x in ( dom g) by Th12;

      then

       A3: x in ( dom f) & ((f +* g) . x) = (f . x) or x in ( dom g) & ((f +* g) . x) = (g . x) by Th11, Th13;

      y = ((f +* g) . x) by A1, A2, FUNCT_1: 1;

      then p in f or p in g by A2, A3, FUNCT_1: 1;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: FUNCT_4:30

    

     Th30: f tolerates g iff (f \/ g) = (f +* g)

    proof

      thus f tolerates g implies (f \/ g) = (f +* g)

      proof

        assume f tolerates g;

        then

         A1: f c= (f +* g) by Th28;

        

         A2: (f +* g) c= (f \/ g) by Th29;

        g c= (f +* g) by Th25;

        then (f \/ g) c= (f +* g) by A1, XBOOLE_1: 8;

        hence thesis by A2;

      end;

      thus thesis by PARTFUN1: 51;

    end;

    theorem :: FUNCT_4:31

    

     Th31: ( dom f) misses ( dom g) implies (f \/ g) = (f +* g) by Th30, PARTFUN1: 56;

    theorem :: FUNCT_4:32

    

     Th32: ( dom f) misses ( dom g) implies f c= (f +* g)

    proof

      assume ( dom f) misses ( dom g);

      then (f \/ g) = (f +* g) by Th31;

      hence thesis by XBOOLE_1: 7;

    end;

    theorem :: FUNCT_4:33

    ( dom f) misses ( dom g) implies ((f +* g) | ( dom f)) = f

    proof

      assume ( dom f) misses ( dom g);

      then

       A1: (( dom f) \ ( dom g)) = ( dom f) by XBOOLE_1: 83;

      ( dom ((f +* g) | ( dom f))) = (( dom (f +* g)) /\ ( dom f)) by RELAT_1: 61

      .= ((( dom f) \/ ( dom g)) /\ ( dom f)) by Def1

      .= ( dom f) by XBOOLE_1: 21;

      hence thesis by A1, Th24, GRFUNC_1: 3;

    end;

    theorem :: FUNCT_4:34

    

     Th34: f tolerates g iff (f +* g) = (g +* f)

    proof

      thus f tolerates g implies (f +* g) = (g +* f)

      proof

        assume

         A1: f tolerates g;

        

         A2: for x be object st x in ( dom (f +* g)) holds ((f +* g) . x) = ((g +* f) . x)

        proof

          let x be object such that

           A3: x in ( dom (f +* g));

          now

            

             A4: ( dom (f +* g)) = (( dom f) \/ ( dom g)) by Def1;

            per cases by A3, A4, XBOOLE_0:def 3;

              suppose

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

              then

               A6: ((g +* f) . x) = (f . x) by Th13;

              x in (( dom f) /\ ( dom g)) & ((f +* g) . x) = (g . x) by A5, Th13, XBOOLE_0:def 4;

              hence thesis by A1, A6;

            end;

              suppose

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

              then ((f +* g) . x) = (f . x) by Th11;

              hence thesis by A7, Th13;

            end;

              suppose

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

              then ((f +* g) . x) = (g . x) by Th13;

              hence thesis by A8, Th11;

            end;

          end;

          hence thesis;

        end;

        ( dom (f +* g)) = (( dom g) \/ ( dom f)) by Def1

        .= ( dom (g +* f)) by Def1;

        hence thesis by A2;

      end;

      assume

       A9: (f +* g) = (g +* f);

      let x be object;

      assume

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

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

      then

       A11: ((f +* g) . x) = (g . x) by Th13;

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

      hence thesis by A9, A11, Th13;

    end;

    theorem :: FUNCT_4:35

    

     Th35: ( dom f) misses ( dom g) implies (f +* g) = (g +* f) by Th34, PARTFUN1: 56;

    theorem :: FUNCT_4:36

    for f,g be PartFunc of X, Y st g is total holds (f +* g) = g

    proof

      let f,g be PartFunc of X, Y;

      assume ( dom g) = X;

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

      hence thesis by Th19;

    end;

    theorem :: FUNCT_4:37

    

     Th37: for f,g be Function of X, Y holds (f +* g) = g

    proof

      let f,g be Function of X, Y;

      per cases ;

        suppose Y = {} implies X = {} ;

        then ( dom f) = X & ( dom g) = X by FUNCT_2:def 1;

        hence thesis by Th19;

      end;

        suppose Y = {} & X <> {} ;

        then f = {} & g = {} ;

        hence thesis;

      end;

    end;

    theorem :: FUNCT_4:38

    for f,g be Function of X, X holds (f +* g) = g by Th37;

    theorem :: FUNCT_4:39

    for f,g be Function of X, D holds (f +* g) = g by Th37;

    theorem :: FUNCT_4:40

    for f,g be PartFunc of X, Y holds (f +* g) is PartFunc of X, Y

    proof

      let f,g be PartFunc of X, Y;

      ( rng (f +* g)) c= (( rng f) \/ ( rng g)) by Th17;

      then

       A1: ( rng (f +* g)) c= Y by XBOOLE_1: 1;

      ( dom (f +* g)) = (( dom f) \/ ( dom g)) by Def1;

      hence thesis by A1, RELSET_1: 4;

    end;

    definition

      let f;

      :: FUNCT_4:def2

      func ~ f -> Function means

      : Def2: (for x be object holds x in ( dom it ) iff ex y,z be object st x = [z, y] & [y, z] in ( dom f)) & for y,z be object st [y, z] in ( dom f) holds (it . (z,y)) = (f . (y,z));

      existence

      proof

        defpred P[ object, object] means ex y,z be object st $1 = [z, y] & $2 = (f . [y, z]);

        defpred Q[ object] means ex y be object st [$1, y] in ( dom f);

        consider D1 be set such that

         A1: for x be object holds x in D1 iff x in ( union ( union ( dom f))) & Q[x] from XBOOLE_0:sch 1;

        defpred Q[ object] means ex y be object st [y, $1] in ( dom f);

        consider D2 be set such that

         A2: for y be object holds y in D2 iff y in ( union ( union ( dom f))) & Q[y] from XBOOLE_0:sch 1;

        defpred Q[ object] means ex y,z be object st $1 = [z, y] & [y, z] in ( dom f);

        consider D be set such that

         A3: for x be object holds x in D iff x in [:D2, D1:] & Q[x] from XBOOLE_0:sch 1;

        

         A4: for x,y1,y2 be object st x in D & P[x, y1] & P[x, y2] holds y1 = y2

        proof

          let x,y1,y2 be object such that x in D;

          given y,z be object such that

           A5: x = [z, y] and

           A6: y1 = (f . [y, z]);

          given y9,z9 be object such that

           A7: x = [z9, y9] and

           A8: y2 = (f . [y9, z9]);

          z = z9 by A5, A7, XTUPLE_0: 1;

          hence thesis by A5, A6, A7, A8, XTUPLE_0: 1;

        end;

        

         A9: for x be object st x in D holds ex y1 be object st P[x, y1]

        proof

          let x be object;

          assume x in D;

          then

          consider y1,z1 be object such that

           A10: x = [z1, y1] and [y1, z1] in ( dom f) by A3;

          take (f . [y1, z1]);

          thus thesis by A10;

        end;

        consider h be Function such that

         A11: ( dom h) = D and

         A12: for x be object st x in D holds P[x, (h . x)] from FUNCT_1:sch 2( A4, A9);

        take h;

        thus

         A13: for x be object holds x in ( dom h) iff ex y,z be object st x = [z, y] & [y, z] in ( dom f)

        proof

          let x be object;

          thus x in ( dom h) implies ex y,z be object st x = [z, y] & [y, z] in ( dom f) by A3, A11;

          given y,z be object such that

           A14: x = [z, y] and

           A15: [y, z] in ( dom f);

          y in ( union ( union ( dom f))) by A15, ZFMISC_1: 134;

          then

           A16: y in D1 by A1, A15;

          z in ( union ( union ( dom f))) by A15, ZFMISC_1: 134;

          then z in D2 by A2, A15;

          then [z, y] in [:D2, D1:] by A16, ZFMISC_1: 87;

          hence thesis by A3, A11, A14, A15;

        end;

        let y,z be object;

        assume [y, z] in ( dom f);

        then [z, y] in D by A11, A13;

        then

        consider y9,z9 be object such that

         A17: [z, y] = [z9, y9] and

         A18: (h . (z,y)) = (f . [y9, z9]) by A12;

        z = z9 by A17, XTUPLE_0: 1;

        hence thesis by A17, A18, XTUPLE_0: 1;

      end;

      uniqueness

      proof

        let h1,h2 be Function such that

         A19: for x be object holds x in ( dom h1) iff ex y,z be object st x = [z, y] & [y, z] in ( dom f) and

         A20: for y,z be object st [y, z] in ( dom f) holds (h1 . (z,y)) = (f . (y,z)) and

         A21: for x be object holds x in ( dom h2) iff ex y,z be object st x = [z, y] & [y, z] in ( dom f) and

         A22: for y,z be object st [y, z] in ( dom f) holds (h2 . (z,y)) = (f . (y,z));

        

         A23: for x be object holds x in ( dom h1) implies (h1 . x) = (h2 . x)

        proof

          let x be object;

          assume x in ( dom h1);

          then

          consider x1,x2 be object such that

           A24: x = [x2, x1] and

           A25: [x1, x2] in ( dom f) by A19;

          (h1 . (x2,x1)) = (f . (x1,x2)) by A20, A25

          .= (h2 . (x2,x1)) by A22, A25;

          hence thesis by A24;

        end;

        for x be object holds x in ( dom h1) iff x in ( dom h2)

        proof

          let x be object;

          x in ( dom h1) iff ex y,z be object st x = [z, y] & [y, z] in ( dom f) by A19;

          hence thesis by A21;

        end;

        then ( dom h1) = ( dom h2) by TARSKI: 2;

        hence thesis by A23;

      end;

    end

    theorem :: FUNCT_4:41

    

     Th41: ( rng ( ~ f)) c= ( rng f)

    proof

      let y be object;

      assume y in ( rng ( ~ f));

      then

      consider x be object such that

       A1: x in ( dom ( ~ f)) and

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

      consider x1,x2 be object such that

       A3: x = [x2, x1] and

       A4: [x1, x2] in ( dom f) by A1, Def2;

      y = (( ~ f) . (x2,x1)) by A2, A3

      .= (f . (x1,x2)) by A4, Def2;

      hence thesis by A4, FUNCT_1:def 3;

    end;

    theorem :: FUNCT_4:42

    

     Th42: for x,y be object holds [x, y] in ( dom f) iff [y, x] in ( dom ( ~ f))

    proof

      let x,y be object;

      thus [x, y] in ( dom f) implies [y, x] in ( dom ( ~ f)) by Def2;

      assume [y, x] in ( dom ( ~ f));

      then

      consider x1,y1 be object such that

       A1: [y, x] = [y1, x1] and

       A2: [x1, y1] in ( dom f) by Def2;

      x1 = x by A1, XTUPLE_0: 1;

      hence thesis by A1, A2, XTUPLE_0: 1;

    end;

    registration

      let f be empty Function;

      cluster ( ~ f) -> empty;

      coherence

      proof

        ( rng f) = {} ;

        then ( rng ( ~ f)) = {} by Th41, XBOOLE_1: 3;

        hence thesis;

      end;

    end

    theorem :: FUNCT_4:43

    

     Th43: for x,y be object holds [y, x] in ( dom ( ~ f)) implies (( ~ f) . (y,x)) = (f . (x,y))

    proof

      let x,y be object;

      assume [y, x] in ( dom ( ~ f));

      then [x, y] in ( dom f) by Th42;

      hence thesis by Def2;

    end;

    theorem :: FUNCT_4:44

    ex X, Y st ( dom ( ~ f)) c= [:X, Y:]

    proof

      now

        let z be object;

        assume z in ( dom ( ~ f));

        then ex x,y be object st z = [y, x] & [x, y] in ( dom f) by Def2;

        hence ex x,y be object st z = [x, y];

      end;

      hence thesis by Th1;

    end;

    theorem :: FUNCT_4:45

    

     Th45: ( dom f) c= [:X, Y:] implies ( dom ( ~ f)) c= [:Y, X:]

    proof

      assume

       A1: ( dom f) c= [:X, Y:];

      let z be object;

      assume z in ( dom ( ~ f));

      then ex x,y be object st z = [y, x] & [x, y] in ( dom f) by Def2;

      hence thesis by A1, ZFMISC_1: 88;

    end;

    theorem :: FUNCT_4:46

    

     Th46: ( dom f) = [:X, Y:] implies ( dom ( ~ f)) = [:Y, X:]

    proof

      assume

       A1: ( dom f) = [:X, Y:];

      hence ( dom ( ~ f)) c= [:Y, X:] by Th45;

      let z be object;

      assume z in [:Y, X:];

      then

      consider y,x be object such that

       A2: y in Y & x in X and

       A3: z = [y, x] by ZFMISC_1:def 2;

       [x, y] in ( dom f) by A1, A2, ZFMISC_1:def 2;

      hence thesis by A3, Def2;

    end;

    theorem :: FUNCT_4:47

    

     Th47: ( dom f) c= [:X, Y:] implies ( rng ( ~ f)) = ( rng f)

    proof

      assume

       A1: ( dom f) c= [:X, Y:];

      thus ( rng ( ~ f)) c= ( rng f) by Th41;

      let y be object;

      assume y in ( rng f);

      then

      consider x be object such that

       A2: x in ( dom f) and

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

      consider x1,y1 be object such that x1 in X and y1 in Y and

       A4: x = [x1, y1] by A1, A2, ZFMISC_1: 84;

      

       A5: [y1, x1] in ( dom ( ~ f)) by A2, A4, Th42;

      y = (f . (x1,y1)) by A3, A4

      .= (( ~ f) . (y1,x1)) by A2, A4, Def2;

      hence thesis by A5, FUNCT_1:def 3;

    end;

    theorem :: FUNCT_4:48

    

     Th48: for f be PartFunc of [:X, Y:], Z holds ( ~ f) is PartFunc of [:Y, X:], Z

    proof

      let f be PartFunc of [:X, Y:], Z;

      

       A1: ( dom f) c= [:X, Y:];

      then

       A2: ( dom ( ~ f)) c= [:Y, X:] by Th45;

      ( rng f) c= Z;

      then ( rng ( ~ f)) c= Z by A1, Th47;

      hence thesis by A2, RELSET_1: 4;

    end;

    definition

      let X, Y, Z;

      let f be PartFunc of [:X, Y:], Z;

      :: original: ~

      redefine

      func ~ f -> PartFunc of [:Y, X:], Z ;

      coherence by Th48;

    end

    theorem :: FUNCT_4:49

    

     Th49: for f be Function of [:X, Y:], Z holds ( ~ f) is Function of [:Y, X:], Z

    proof

      let f be Function of [:X, Y:], Z;

      per cases ;

        suppose

         A1: Z = {} ;

        then

        reconsider f as empty set;

        ( ~ f) = {} ;

        hence thesis by A1, FUNCT_2: 130;

      end;

        suppose

         A1: Z <> {} ;

        reconsider R = ( ~ f) as Relation of [:Y, X:], Z;

        R is quasi_total

        proof

          per cases ;

            case Z <> {} ;

            ( dom f) = [:X, Y:] by A1, FUNCT_2:def 1;

            hence thesis by Th46;

          end;

            case Z = {} ;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

    end;

    definition

      let X, Y, Z;

      let f be Function of [:X, Y:], Z;

      :: original: ~

      redefine

      func ~ f -> Function of [:Y, X:], Z ;

      coherence by Th49;

    end

    theorem :: FUNCT_4:50

    for f be Function of [:X, Y:], Z holds ( ~ f) is Function of [:Y, X:], Z;

    theorem :: FUNCT_4:51

    

     Th51: ( ~ ( ~ f)) c= f

    proof

       A1:

      now

        let x be object;

        assume x in ( dom ( ~ ( ~ f)));

        then

        consider y2,z2 be object such that

         A2: x = [z2, y2] & [y2, z2] in ( dom ( ~ f)) by Def2;

        take y2, z2;

        thus x = [z2, y2] & [y2, z2] in ( dom ( ~ f)) & [z2, y2] in ( dom f) by A2, Th42;

      end;

      

       A3: for x be object holds x in ( dom ( ~ ( ~ f))) implies (( ~ ( ~ f)) . x) = (f . x)

      proof

        let x be object;

        assume x in ( dom ( ~ ( ~ f)));

        then

        consider y2,z2 be object such that

         A4: x = [z2, y2] and

         A5: [y2, z2] in ( dom ( ~ f)) and

         A6: [z2, y2] in ( dom f) by A1;

        (( ~ ( ~ f)) . (z2,y2)) = (( ~ f) . (y2,z2)) by A5, Def2

        .= (f . (z2,y2)) by A6, Def2;

        hence thesis by A4;

      end;

      ( dom ( ~ ( ~ f))) c= ( dom f)

      proof

        let x be object;

        assume x in ( dom ( ~ ( ~ f)));

        then ex y2,z2 be object st x = [z2, y2] & [y2, z2] in ( dom ( ~ f)) & [z2, y2] in ( dom f) by A1;

        hence thesis;

      end;

      hence thesis by A3, GRFUNC_1: 2;

    end;

    theorem :: FUNCT_4:52

    

     Th52: ( dom f) c= [:X, Y:] implies ( ~ ( ~ f)) = f

    proof

      assume

       A1: ( dom f) c= [:X, Y:];

      

       A2: ( ~ ( ~ f)) c= f by Th51;

      ( dom ( ~ ( ~ f))) = ( dom f)

      proof

        thus ( dom ( ~ ( ~ f))) c= ( dom f) by A2, RELAT_1: 11;

        let z be object;

        assume

         A3: z in ( dom f);

        then

        consider x,y be object such that x in X and y in Y and

         A4: z = [x, y] by A1, ZFMISC_1: 84;

         [y, x] in ( dom ( ~ f)) by A3, A4, Th42;

        hence thesis by A4, Th42;

      end;

      hence thesis by Th51, GRFUNC_1: 3;

    end;

    theorem :: FUNCT_4:53

    for f be PartFunc of [:X, Y:], Z holds ( ~ ( ~ f)) = f

    proof

      let f be PartFunc of [:X, Y:], Z;

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

      hence thesis by Th52;

    end;

    definition

      let f, g;

      :: FUNCT_4:def3

      func |:f,g:| -> Function means

      : Def3: (for z be object holds z in ( dom it ) iff ex x,y,x9,y9 be object st z = [ [x, x9], [y, y9]] & [x, y] in ( dom f) & [x9, y9] in ( dom g)) & for x,y,x9,y9 be object st [x, y] in ( dom f) & [x9, y9] in ( dom g) holds (it . ( [x, x9], [y, y9])) = [(f . (x,y)), (g . (x9,y9))];

      existence

      proof

        defpred P[ object, object] means ex x,y,x9,y9 be object st $1 = [ [x, x9], [y, y9]] & $2 = [(f . [x, y]), (g . [x9, y9])];

        defpred Q[ object] means ex y be object st [$1, y] in ( dom f);

        consider D1 be set such that

         A1: for x be object holds x in D1 iff x in ( union ( union ( dom f))) & Q[x] from XBOOLE_0:sch 1;

        defpred Q[ object] means ex x be object st [x, $1] in ( dom f);

        consider D2 be set such that

         A2: for y be object holds y in D2 iff y in ( union ( union ( dom f))) & Q[y] from XBOOLE_0:sch 1;

        defpred Q[ object] means ex y be object st [$1, y] in ( dom g);

        consider D19 be set such that

         A3: for x be object holds x in D19 iff x in ( union ( union ( dom g))) & Q[x] from XBOOLE_0:sch 1;

        defpred Q[ object] means ex x be object st [x, $1] in ( dom g);

        consider D29 be set such that

         A4: for y be object holds y in D29 iff y in ( union ( union ( dom g))) & Q[y] from XBOOLE_0:sch 1;

        defpred Q[ object] means ex x,y,x9,y9 be object st $1 = [ [x, x9], [y, y9]] & [x, y] in ( dom f) & [x9, y9] in ( dom g);

        consider D be set such that

         A5: for z be object holds z in D iff z in [: [:D1, D19:], [:D2, D29:]:] & Q[z] from XBOOLE_0:sch 1;

        

         A6: for z,z1,z2 be object st z in D & P[z, z1] & P[z, z2] holds z1 = z2

        proof

          let z,z1,z2 be object such that z in D;

          given x,y,x9,y9 be object such that

           A7: z = [ [x, x9], [y, y9]] and

           A8: z1 = [(f . [x, y]), (g . [x9, y9])];

          given x1,y1,x19,y19 be object such that

           A9: z = [ [x1, x19], [y1, y19]] and

           A10: z2 = [(f . [x1, y1]), (g . [x19, y19])];

          

           A11: x9 = x19 by A7, A9, Lm1;

          x = x1 & y = y1 by A7, A9, Lm1;

          hence thesis by A7, A8, A9, A10, A11, Lm1;

        end;

        

         A12: for z be object st z in D holds ex z1 be object st P[z, z1]

        proof

          let z be object;

          assume z in D;

          then

          consider x1,y1,x8,y8 be object such that

           A13: z = [ [x1, x8], [y1, y8]] and [x1, y1] in ( dom f) and [x8, y8] in ( dom g) by A5;

          take [(f . [x1, y1]), (g . [x8, y8])];

          thus thesis by A13;

        end;

        consider h be Function such that

         A14: ( dom h) = D and

         A15: for z be object st z in D holds P[z, (h . z)] from FUNCT_1:sch 2( A6, A12);

        take h;

        thus

         A16: for z be object holds z in ( dom h) iff ex x,y,x9,y9 be object st z = [ [x, x9], [y, y9]] & [x, y] in ( dom f) & [x9, y9] in ( dom g)

        proof

          let z be object;

          thus z in ( dom h) implies ex x,y,x9,y9 be object st z = [ [x, x9], [y, y9]] & [x, y] in ( dom f) & [x9, y9] in ( dom g) by A5, A14;

          given x,y,x9,y9 be object such that

           A17: z = [ [x, x9], [y, y9]] and

           A18: [x, y] in ( dom f) and

           A19: [x9, y9] in ( dom g);

          y9 in ( union ( union ( dom g))) by A19, ZFMISC_1: 134;

          then

           A20: y9 in D29 by A4, A19;

          y in ( union ( union ( dom f))) by A18, ZFMISC_1: 134;

          then y in D2 by A2, A18;

          then

           A21: [y, y9] in [:D2, D29:] by A20, ZFMISC_1: 87;

          x9 in ( union ( union ( dom g))) by A19, ZFMISC_1: 134;

          then

           A22: x9 in D19 by A3, A19;

          x in ( union ( union ( dom f))) by A18, ZFMISC_1: 134;

          then x in D1 by A1, A18;

          then [x, x9] in [:D1, D19:] by A22, ZFMISC_1: 87;

          then z in [: [:D1, D19:], [:D2, D29:]:] by A17, A21, ZFMISC_1: 87;

          hence thesis by A5, A14, A17, A18, A19;

        end;

        let x,y,x9,y9 be object;

        assume [x, y] in ( dom f) & [x9, y9] in ( dom g);

        then [ [x, x9], [y, y9]] in D by A14, A16;

        then

        consider x1,y1,x19,y19 be object such that

         A23: [ [x, x9], [y, y9]] = [ [x1, x19], [y1, y19]] and

         A24: (h . [ [x, x9], [y, y9]]) = [(f . [x1, y1]), (g . [x19, y19])] by A15;

        

         A25: x9 = x19 by A23, Lm1;

        x = x1 & y = y1 by A23, Lm1;

        hence thesis by A23, A24, A25, Lm1;

      end;

      uniqueness

      proof

        let h1,h2 be Function such that

         A26: for z be object holds z in ( dom h1) iff ex x,y,x9,y9 be object st z = [ [x, x9], [y, y9]] & [x, y] in ( dom f) & [x9, y9] in ( dom g) and

         A27: for x,y,x9,y9 be object st [x, y] in ( dom f) & [x9, y9] in ( dom g) holds (h1 . ( [x, x9], [y, y9])) = [(f . (x,y)), (g . (x9,y9))] and

         A28: for z be object holds z in ( dom h2) iff ex x,y,x9,y9 be object st z = [ [x, x9], [y, y9]] & [x, y] in ( dom f) & [x9, y9] in ( dom g) and

         A29: for x,y,x9,y9 be object st [x, y] in ( dom f) & [x9, y9] in ( dom g) holds (h2 . ( [x, x9], [y, y9])) = [(f . (x,y)), (g . (x9,y9))];

        

         A30: for z be object holds z in ( dom h1) implies (h1 . z) = (h2 . z)

        proof

          let z be object;

          assume z in ( dom h1);

          then

          consider x,y,x9,y9 be object such that

           A31: z = [ [x, x9], [y, y9]] and

           A32: [x, y] in ( dom f) & [x9, y9] in ( dom g) by A26;

          (h1 . ( [x, x9], [y, y9])) = [(f . (x,y)), (g . (x9,y9))] by A27, A32

          .= (h2 . ( [x, x9], [y, y9])) by A29, A32;

          hence thesis by A31;

        end;

        for z be object holds z in ( dom h1) iff z in ( dom h2)

        proof

          let z be object;

          z in ( dom h1) iff ex x,y,x9,y9 be object st z = [ [x, x9], [y, y9]] & [x, y] in ( dom f) & [x9, y9] in ( dom g) by A26;

          hence thesis by A28;

        end;

        then ( dom h1) = ( dom h2) by TARSKI: 2;

        hence thesis by A30;

      end;

    end

    theorem :: FUNCT_4:54

    

     Th54: [ [x, x9], [y, y9]] in ( dom |:f, g:|) iff [x, y] in ( dom f) & [x9, y9] in ( dom g)

    proof

      thus [ [x, x9], [y, y9]] in ( dom |:f, g:|) implies [x, y] in ( dom f) & [x9, y9] in ( dom g)

      proof

        assume [ [x, x9], [y, y9]] in ( dom |:f, g:|);

        then

        consider x1,y1,x19,y19 be object such that

         A1: [ [x, x9], [y, y9]] = [ [x1, x19], [y1, y19]] and

         A2: [x1, y1] in ( dom f) & [x19, y19] in ( dom g) by Def3;

        x = x1 & x9 = x19 by A1, Lm1;

        hence thesis by A1, A2, Lm1;

      end;

      thus thesis by Def3;

    end;

    theorem :: FUNCT_4:55

     [ [x, x9], [y, y9]] in ( dom |:f, g:|) implies ( |:f, g:| . ( [x, x9], [y, y9])) = [(f . (x,y)), (g . (x9,y9))]

    proof

      assume [ [x, x9], [y, y9]] in ( dom |:f, g:|);

      then [x, y] in ( dom f) & [x9, y9] in ( dom g) by Th54;

      hence thesis by Def3;

    end;

    theorem :: FUNCT_4:56

    

     Th56: ( rng |:f, g:|) c= [:( rng f), ( rng g):]

    proof

      let z be object;

      assume z in ( rng |:f, g:|);

      then

      consider p be object such that

       A1: p in ( dom |:f, g:|) and

       A2: z = ( |:f, g:| . p) by FUNCT_1:def 3;

      consider x,y,x9,y9 be object such that

       A3: p = [ [x, x9], [y, y9]] and

       A4: [x, y] in ( dom f) & [x9, y9] in ( dom g) by A1, Def3;

      

       A5: (f . [x, y]) in ( rng f) & (g . [x9, y9]) in ( rng g) by A4, FUNCT_1:def 3;

      z = ( |:f, g:| . ( [x, x9], [y, y9])) by A2, A3

      .= [(f . (x,y)), (g . (x9,y9))] by A4, Def3;

      hence thesis by A5, ZFMISC_1: 87;

    end;

    theorem :: FUNCT_4:57

    

     Th57: ( dom f) c= [:X, Y:] & ( dom g) c= [:X9, Y9:] implies ( dom |:f, g:|) c= [: [:X, X9:], [:Y, Y9:]:]

    proof

      assume

       A1: ( dom f) c= [:X, Y:] & ( dom g) c= [:X9, Y9:];

      let xy be object;

      assume xy in ( dom |:f, g:|);

      then

      consider x,y,x9,y9 be object such that

       A2: xy = [ [x, x9], [y, y9]] and

       A3: [x, y] in ( dom f) & [x9, y9] in ( dom g) by Def3;

      y in Y & y9 in Y9 by A1, A3, ZFMISC_1: 87;

      then

       A4: [y, y9] in [:Y, Y9:] by ZFMISC_1: 87;

      x in X & x9 in X9 by A1, A3, ZFMISC_1: 87;

      then [x, x9] in [:X, X9:] by ZFMISC_1: 87;

      hence thesis by A2, A4, ZFMISC_1: 87;

    end;

    theorem :: FUNCT_4:58

    

     Th58: ( dom f) = [:X, Y:] & ( dom g) = [:X9, Y9:] implies ( dom |:f, g:|) = [: [:X, X9:], [:Y, Y9:]:]

    proof

      assume

       A1: ( dom f) = [:X, Y:] & ( dom g) = [:X9, Y9:];

      hence ( dom |:f, g:|) c= [: [:X, X9:], [:Y, Y9:]:] by Th57;

      let z be object;

      assume z in [: [:X, X9:], [:Y, Y9:]:];

      then

      consider xx,yy be object such that

       A2: xx in [:X, X9:] and

       A3: yy in [:Y, Y9:] and

       A4: z = [xx, yy] by ZFMISC_1:def 2;

      consider y,y9 be object such that

       A5: y in Y & y9 in Y9 and

       A6: yy = [y, y9] by A3, ZFMISC_1:def 2;

      consider x,x9 be object such that

       A7: x in X & x9 in X9 and

       A8: xx = [x, x9] by A2, ZFMISC_1:def 2;

       [x, y] in ( dom f) & [x9, y9] in ( dom g) by A1, A7, A5, ZFMISC_1: 87;

      hence thesis by A4, A8, A6, Def3;

    end;

    theorem :: FUNCT_4:59

    

     Th59: for f be PartFunc of [:X, Y:], Z holds for g be PartFunc of [:X9, Y9:], Z9 holds |:f, g:| is PartFunc of [: [:X, X9:], [:Y, Y9:]:], [:Z, Z9:]

    proof

      let f be PartFunc of [:X, Y:], Z;

      let g be PartFunc of [:X9, Y9:], Z9;

      ( rng |:f, g:|) c= [:( rng f), ( rng g):] & [:( rng f), ( rng g):] c= [:Z, Z9:] by Th56, ZFMISC_1: 96;

      then

       A1: ( rng |:f, g:|) c= [:Z, Z9:];

      ( dom f) c= [:X, Y:] & ( dom g) c= [:X9, Y9:];

      then ( dom |:f, g:|) c= [: [:X, X9:], [:Y, Y9:]:] by Th57;

      hence thesis by A1, RELSET_1: 4;

    end;

    theorem :: FUNCT_4:60

    

     Th60: for f be Function of [:X, Y:], Z holds for g be Function of [:X9, Y9:], Z9 st Z <> {} & Z9 <> {} holds |:f, g:| is Function of [: [:X, X9:], [:Y, Y9:]:], [:Z, Z9:]

    proof

      let f be Function of [:X, Y:], Z;

      let g be Function of [:X9, Y9:], Z9;

      ( rng |:f, g:|) c= [:( rng f), ( rng g):] & [:( rng f), ( rng g):] c= [:Z, Z9:] by Th56, ZFMISC_1: 96;

      then

       A1: ( rng |:f, g:|) c= [:Z, Z9:];

      assume

       A2: Z <> {} & Z9 <> {} ;

      then ( dom f) = [:X, Y:] & ( dom g) = [:X9, Y9:] by FUNCT_2:def 1;

      then [: [:X, X9:], [:Y, Y9:]:] = ( dom |:f, g:|) by Th58;

      then

      reconsider R = |:f, g:| as Relation of [: [:X, X9:], [:Y, Y9:]:], [:Z, Z9:] by A1, RELSET_1: 4;

      R is quasi_total

      proof

        per cases ;

          case [:Z, Z9:] <> {} ;

          ( dom f) = [:X, Y:] & ( dom g) = [:X9, Y9:] by A2, FUNCT_2:def 1;

          hence thesis by Th58;

        end;

          case [:Z, Z9:] = {} ;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: FUNCT_4:61

    for f be Function of [:X, Y:], D holds for g be Function of [:X9, Y9:], D9 holds |:f, g:| is Function of [: [:X, X9:], [:Y, Y9:]:], [:D, D9:] by Th60;

    definition

      let x,y,a,b be object;

      :: FUNCT_4:def4

      func (x,y) --> (a,b) -> set equals ((x .--> a) +* (y .--> b));

      correctness ;

    end

    registration

      let x,y,a,b be object;

      cluster ((x,y) --> (a,b)) -> Function-like Relation-like;

      coherence ;

    end

    theorem :: FUNCT_4:62

    

     Th62: for x1,x2,y1,y2 be object holds ( dom ((x1,x2) --> (y1,y2))) = {x1, x2} & ( rng ((x1,x2) --> (y1,y2))) c= {y1, y2}

    proof

      let x1,x2,y1,y2 be object;

      set f = ( {x1} --> y1), g = ( {x2} --> y2), h = ((x1,x2) --> (y1,y2));

      (( rng f) \/ ( rng g)) c= ( {y1} \/ {y2}) by XBOOLE_1: 13;

      then

       A1: (( rng f) \/ ( rng g)) c= {y1, y2} by ENUMSET1: 1;

      (( dom f) \/ ( dom g)) = {x1, x2} by ENUMSET1: 1;

      hence ( dom h) = {x1, x2} by Def1;

      ( rng h) c= (( rng f) \/ ( rng g)) by Th17;

      hence thesis by A1;

    end;

    theorem :: FUNCT_4:63

    

     Th63: for x1,x2,y1,y2 be object holds (x1 <> x2 implies (((x1,x2) --> (y1,y2)) . x1) = y1) & (((x1,x2) --> (y1,y2)) . x2) = y2

    proof

      let x1,x2,y1,y2 be object;

      set f = ( {x1} --> y1), g = ( {x2} --> y2), h = ((x1,x2) --> (y1,y2));

      

       A1: x2 in {x2} by TARSKI:def 1;

      

       A2: x1 in {x1} by TARSKI:def 1;

      hereby

        assume x1 <> x2;

        then not x1 in ( dom g) by TARSKI:def 1;

        then (h . x1) = (f . x1) by Th11;

        hence (h . x1) = y1 by A2, FUNCOP_1: 7;

      end;

       {x2} = ( dom g);

      then (h . x2) = (g . x2) by A1, Th13;

      hence thesis by A1, FUNCOP_1: 7;

    end;

    theorem :: FUNCT_4:64

    for x1,x2,y1,y2 be object holds x1 <> x2 implies ( rng ((x1,x2) --> (y1,y2))) = {y1, y2}

    proof

      let x1,x2,y1,y2 be object;

      set h = ((x1,x2) --> (y1,y2));

      assume

       A1: x1 <> x2;

      thus ( rng h) c= {y1, y2} by Th62;

      let y be object;

      assume y in {y1, y2};

      then y = y1 or y = y2 by TARSKI:def 2;

      then

       A2: (h . x1) = y or (h . x2) = y by A1, Th63;

      ( dom h) = {x1, x2} by Th62;

      then x1 in ( dom h) & x2 in ( dom h) by TARSKI:def 2;

      hence thesis by A2, FUNCT_1:def 3;

    end;

    theorem :: FUNCT_4:65

    for x1,x2,y be object holds ((x1,x2) --> (y,y)) = ( {x1, x2} --> y)

    proof

      let x1,x2,y be object;

      set F = ((x1,x2) --> (y,y)), f = ( {x1} --> y), g = ( {x2} --> y), F9 = ( {x1, x2} --> y);

      now

        thus

         A1: ( dom F) = {x1, x2} & ( dom F9) = {x1, x2} by Th62;

        let x be object such that

         A2: x in {x1, x2};

        now

          per cases by A1, A2, Th12;

            suppose

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

            then (F . x) = (f . x) by Th11;

            hence (F . x) = y & (F9 . x) = y by A2, A3, FUNCOP_1: 7;

          end;

            suppose

             A4: x in ( dom g);

            then (F . x) = (g . x) by Th13;

            hence (F . x) = y & (F9 . x) = y by A2, A4, FUNCOP_1: 7;

          end;

        end;

        hence (F . x) = (F9 . x);

      end;

      hence thesis;

    end;

    definition

      let A, x1, x2;

      let y1,y2 be Element of A;

      :: original: -->

      redefine

      func (x1,x2) --> (y1,y2) -> Function of {x1, x2}, A ;

      coherence

      proof

        set f = ( {x1} --> y1), g = ( {x2} --> y2), h = ((x1,x2) --> (y1,y2));

        ( rng h) c= (( rng f) \/ ( rng g)) by Th17;

        then

         A1: ( rng h) c= A by XBOOLE_1: 1;

        ( dom h) = {x1, x2} by Th62;

        hence thesis by A1, FUNCT_2:def 1, RELSET_1: 4;

      end;

    end

    theorem :: FUNCT_4:66

    for a,b,c,d be object, g be Function st ( dom g) = {a, b} & (g . a) = c & (g . b) = d holds g = ((a,b) --> (c,d))

    proof

      let a,b,c,d be object;

      let h be Function such that

       A1: ( dom h) = {a, b} and

       A2: (h . a) = c and

       A3: (h . b) = d;

      set f = ( {a} --> c), g = ( {b} --> d);

      

       A4: b in {b} by TARSKI:def 1;

      

       A5: a in {a} by TARSKI:def 1;

       A6:

      now

        let x be object such that

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

        thus x in ( dom g) implies (h . x) = (g . x)

        proof

          assume x in ( dom g);

          then x = b by TARSKI:def 1;

          hence thesis by A3, A4, FUNCOP_1: 7;

        end;

        assume not x in ( dom g);

        then x in ( dom f) by A7, XBOOLE_0:def 3;

        then x = a by TARSKI:def 1;

        hence (h . x) = (f . x) by A2, A5, FUNCOP_1: 7;

      end;

      ( dom h) = (( dom f) \/ ( dom g)) by A1, ENUMSET1: 1;

      hence thesis by A6, Def1;

    end;

    theorem :: FUNCT_4:67

    

     Th67: for a,b,c,d be object st a <> c holds ((a,c) --> (b,d)) = { [a, b], [c, d]}

    proof

      let a,b,c,d be object such that

       A1: a <> c;

      set f = ( {a} --> b), g = ( {c} --> d);

      ( {a} --> b) = { [a, b]} & ( {c} --> d) = { [c, d]} by ZFMISC_1: 29;

      

      hence ((a,c) --> (b,d)) = ( { [a, b]} \/ { [c, d]}) by A1, Th31, ZFMISC_1: 11

      .= { [a, b], [c, d]} by ENUMSET1: 1;

    end;

    theorem :: FUNCT_4:68

    for a,b,x,y,x9,y9 be object st a <> b & ((a,b) --> (x,y)) = ((a,b) --> (x9,y9)) holds x = x9 & y = y9

    proof

      let a,b,x,y,x9,y9 be object such that

       A1: a <> b and

       A2: ((a,b) --> (x,y)) = ((a,b) --> (x9,y9));

      

      thus x = (((a,b) --> (x,y)) . a) by A1, Th63

      .= x9 by A1, A2, Th63;

      

      thus y = (((a,b) --> (x,y)) . b) by Th63

      .= y9 by A2, Th63;

    end;

    begin

    theorem :: FUNCT_4:69

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

    proof

      let f1,f2,g1,g2 be Function;

      assume that

       A1: ( rng g1) c= ( dom f1) & ( rng g2) c= ( dom f2) and

       A2: f1 tolerates f2;

      

       A3: ( rng (g1 +* g2)) c= (( rng g1) \/ ( rng g2)) & ( dom (f1 +* f2)) = (( dom f1) \/ ( dom f2)) by Def1, Th17;

      (( rng g1) \/ ( rng g2)) c= (( dom f1) \/ ( dom f2)) by A1, XBOOLE_1: 13;

      

      then

       A4: ( dom ((f1 +* f2) * (g1 +* g2))) = ( dom (g1 +* g2)) by A3, RELAT_1: 27, XBOOLE_1: 1

      .= (( dom g1) \/ ( dom g2)) by Def1;

      

       A5: ( dom (f1 * g1)) = ( dom g1) & ( dom (f2 * g2)) = ( dom g2) by A1, RELAT_1: 27;

       A6:

      now

        let x be object;

        

         A7: not x in ( dom g2) or x in ( dom g2);

        assume

         A8: x in (( dom g1) \/ ( dom g2));

        then

         A9: (((f1 +* f2) * (g1 +* g2)) . x) = ((f1 +* f2) . ((g1 +* g2) . x)) by A4, FUNCT_1: 12;

        x in ( dom g1) or x in ( dom g2) by A8, XBOOLE_0:def 3;

        then ((g1 +* g2) . x) = (g1 . x) & (((f1 * g1) +* (f2 * g2)) . x) = ((f1 * g1) . x) & ((f1 * g1) . x) = (f1 . (g1 . x)) & (g1 . x) in ( rng g1) & ((g1 . x) in ( rng g1) implies (g1 . x) in ( dom f1)) or ((g1 +* g2) . x) = (g2 . x) & (((f1 * g1) +* (f2 * g2)) . x) = ((f2 * g2) . x) & ((f2 * g2) . x) = (f2 . (g2 . x)) & (g2 . x) in ( rng g2) & ((g2 . x) in ( rng g2) implies (g2 . x) in ( dom f2)) by A1, A5, A8, A7, Def1, FUNCT_1: 12, FUNCT_1:def 3;

        hence (((f1 +* f2) * (g1 +* g2)) . x) = (((f1 * g1) +* (f2 * g2)) . x) by A2, A9, Th13, Th15;

      end;

      ( dom ((f1 * g1) +* (f2 * g2))) = (( dom g1) \/ ( dom g2)) by A5, Def1;

      hence thesis by A4, A6;

    end;

    reserve A,B for set;

    theorem :: FUNCT_4:70

    

     Th70: ( dom f) c= (A \/ B) implies ((f | A) +* (f | B)) = f

    proof

      

       A1: ( dom (f | A)) = (( dom f) /\ A) & ( dom (f | B)) = (( dom f) /\ B) by RELAT_1: 61;

      

       A2: for x be object holds x in (( dom (f | A)) \/ ( dom (f | B))) implies (x in ( dom (f | B)) implies (f . x) = ((f | B) . x)) & ( not x in ( dom (f | B)) implies (f . x) = ((f | A) . x))

      proof

        let x be object;

        assume

         A3: x in (( dom (f | A)) \/ ( dom (f | B)));

        thus x in ( dom (f | B)) implies (f . x) = ((f | B) . x) by FUNCT_1: 47;

        assume not x in ( dom (f | B));

        then x in ( dom (f | A)) by A3, XBOOLE_0:def 3;

        hence thesis by FUNCT_1: 47;

      end;

      assume ( dom f) c= (A \/ B);

      

      then ( dom f) = (( dom f) /\ (A \/ B)) by XBOOLE_1: 28

      .= (( dom (f | A)) \/ ( dom (f | B))) by A1, XBOOLE_1: 23;

      hence thesis by A2, Def1;

    end;

    theorem :: FUNCT_4:71

    

     Th71: for p,q be Function, A be set holds ((p +* q) | A) = ((p | A) +* (q | A))

    proof

      let p,q be Function, A be set;

      

       A1: ( dom ((p +* q) | A)) = (( dom (p +* q)) /\ A) by RELAT_1: 61

      .= ((( dom p) \/ ( dom q)) /\ A) by Def1

      .= ((( dom p) /\ A) \/ (( dom q) /\ A)) by XBOOLE_1: 23

      .= (( dom (p | A)) \/ (( dom q) /\ A)) by RELAT_1: 61

      .= (( dom (p | A)) \/ ( dom (q | A))) by RELAT_1: 61;

      for x be object st x in (( dom (p | A)) \/ ( dom (q | A))) holds (x in ( dom (q | A)) implies (((p +* q) | A) . x) = ((q | A) . x)) & ( not x in ( dom (q | A)) implies (((p +* q) | A) . x) = ((p | A) . x))

      proof

        let x be object;

        assume

         A2: x in (( dom (p | A)) \/ ( dom (q | A)));

        then x in ( dom (p | A)) or x in ( dom (q | A)) by XBOOLE_0:def 3;

        then x in (( dom p) /\ A) or x in (( dom q) /\ A) by RELAT_1: 61;

        then

         A3: x in A by XBOOLE_0:def 4;

        hereby

          assume

           A4: x in ( dom (q | A));

          then x in (( dom q) /\ A) by RELAT_1: 61;

          then

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

          

          thus (((p +* q) | A) . x) = ((p +* q) . x) by A1, A2, FUNCT_1: 47

          .= (q . x) by A5, Th13

          .= ((q | A) . x) by A4, FUNCT_1: 47;

        end;

        assume

         A6: not x in ( dom (q | A));

        then not x in (( dom q) /\ A) by RELAT_1: 61;

        then

         A7: not x in ( dom q) by A3, XBOOLE_0:def 4;

        

         A8: x in ( dom (p | A)) by A2, A6, XBOOLE_0:def 3;

        then x in (( dom p) /\ A) by RELAT_1: 61;

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

        then x in ( dom (p +* q)) by Th12;

        then x in (( dom (p +* q)) /\ A) by A3, XBOOLE_0:def 4;

        then x in ( dom ((p +* q) | A)) by RELAT_1: 61;

        

        hence (((p +* q) | A) . x) = ((p +* q) . x) by FUNCT_1: 47

        .= (p . x) by A7, Th11

        .= ((p | A) . x) by A8, FUNCT_1: 47;

      end;

      hence thesis by A1, Def1;

    end;

    theorem :: FUNCT_4:72

    

     Th72: for f,g be Function, A be set st A misses ( dom g) holds ((f +* g) | A) = (f | A)

    proof

      let f,g be Function, A be set;

      assume A misses ( dom g);

      then (( dom g) /\ A) = {} ;

      then ( dom (g | A)) = {} by RELAT_1: 61;

      then (g | A) = {} ;

      

      hence ((f +* g) | A) = ((f | A) +* {} ) by Th71

      .= (f | A);

    end;

    theorem :: FUNCT_4:73

    for f,g be Function, A be set holds ( dom f) misses A implies ((f +* g) | A) = (g | A)

    proof

      let f,g be Function, A be set;

      assume ( dom f) misses A;

      then (( dom f) /\ A) = {} ;

      then ( dom (f | A)) = {} by RELAT_1: 61;

      then (f | A) = {} ;

      

      hence ((f +* g) | A) = ( {} +* (g | A)) by Th71

      .= (g | A);

    end;

    theorem :: FUNCT_4:74

    for f,g,h be Function st ( dom g) = ( dom h) holds ((f +* g) +* h) = (f +* h)

    proof

      let f,g,h be Function;

      assume

       A1: ( dom g) = ( dom h);

      

      thus ((f +* g) +* h) = (f +* (g +* h)) by Th14

      .= (f +* h) by A1, Th19;

    end;

    

     Lm2: for f,g be Function holds f c= g implies (g +* f) = g

    proof

      let f,g be Function;

      assume

       A1: f c= g;

      then f tolerates g by PARTFUN1: 54;

      

      hence (g +* f) = (f \/ g) by Th30

      .= g by A1, XBOOLE_1: 12;

    end;

    theorem :: FUNCT_4:75

    for f be Function, A be set holds (f +* (f | A)) = f by Lm2, RELAT_1: 59;

    theorem :: FUNCT_4:76

    for f,g be Function, B,C be set st ( dom f) c= B & ( dom g) c= C & B misses C holds ((f +* g) | B) = f & ((f +* g) | C) = g

    proof

      let f,g be Function, B,C be set;

      assume that

       A1: ( dom f) c= B and

       A2: ( dom g) c= C and

       A3: B misses C;

      ( dom f) misses C by A1, A3, XBOOLE_1: 63;

      then (( dom f) /\ C) = {} ;

      then ( dom (f | C)) = {} by RELAT_1: 61;

      then

       A4: (f | C) = {} ;

      ( dom g) misses B by A2, A3, XBOOLE_1: 63;

      then (( dom g) /\ B) = {} ;

      then ( dom (g | B)) = {} by RELAT_1: 61;

      then

       A5: (g | B) = {} ;

      

      thus ((f +* g) | B) = ((f | B) +* (g | B)) by Th71

      .= (f | B) by A5

      .= f by A1, RELAT_1: 68;

      

      thus ((f +* g) | C) = ((f | C) +* (g | C)) by Th71

      .= (g | C) by A4

      .= g by A2, RELAT_1: 68;

    end;

    theorem :: FUNCT_4:77

    for p,q be Function, A be set holds ( dom p) c= A & ( dom q) misses A implies ((p +* q) | A) = p

    proof

      let p,q be Function, A be set;

      assume that

       A1: ( dom p) c= A and

       A2: ( dom q) misses A;

      

      thus ((p +* q) | A) = (p | A) by A2, Th72

      .= p by A1, RELAT_1: 68;

    end;

    theorem :: FUNCT_4:78

    for f be Function, A,B be set holds (f | (A \/ B)) = ((f | A) +* (f | B))

    proof

      let f be Function, A,B be set;

      

       A1: ((f | (A \/ B)) | B) = (f | ((A \/ B) /\ B)) by RELAT_1: 71

      .= (f | B) by XBOOLE_1: 21;

      

       A2: ( dom (f | (A \/ B))) c= (A \/ B) by RELAT_1: 58;

      ((f | (A \/ B)) | A) = (f | ((A \/ B) /\ A)) by RELAT_1: 71

      .= (f | A) by XBOOLE_1: 21;

      hence thesis by A1, A2, Th70;

    end;

    reserve x,y,i,j,k for object;

    theorem :: FUNCT_4:79

    ((i,j) :-> k) = ( [i, j] .--> k);

    theorem :: FUNCT_4:80

    (((i,j) :-> k) . (i,j)) = k by FUNCOP_1: 71;

    theorem :: FUNCT_4:81

    

     Th81: for a,b,c be object holds ((a,a) --> (b,c)) = (a .--> c)

    proof

      let a,b,c be object;

      ( dom (a .--> c)) = {a}

      .= ( dom ( {a} --> b));

      hence thesis by Th19;

    end;

    theorem :: FUNCT_4:82

    for x, y holds (x .--> y) = { [x, y]} by ZFMISC_1: 29;

    theorem :: FUNCT_4:83

    for f be Function, a,b,c be object st a <> c holds ((f +* (a .--> b)) . c) = (f . c)

    proof

      let f be Function, a,b,c be object such that

       A1: a <> c;

      set g = (a .--> b);

       not c in ( dom g) by A1, TARSKI:def 1;

      hence thesis by Th11;

    end;

    theorem :: FUNCT_4:84

    

     Th84: for f be Function, a,b,c,d be object st a <> b holds ((f +* ((a,b) --> (c,d))) . a) = c & ((f +* ((a,b) --> (c,d))) . b) = d

    proof

      let f be Function, a,b,c,d be object such that

       A1: a <> b;

      set g = ((a,b) --> (c,d));

      

       A2: ( dom g) = {a, b} by Th62;

      then a in ( dom g) by TARSKI:def 2;

      

      hence ((f +* g) . a) = (g . a) by Th13

      .= c by A1, Th63;

      b in ( dom g) by A2, TARSKI:def 2;

      

      hence ((f +* g) . b) = (g . b) by Th13

      .= d by Th63;

    end;

    theorem :: FUNCT_4:85

    

     Th85: for a,b be set, f be Function st a in ( dom f) & (f . a) = b holds (a .--> b) c= f

    proof

      let a,b be set, f be Function;

      assume a in ( dom f) & (f . a) = b;

      then [a, b] in f by FUNCT_1: 1;

      then { [a, b]} c= f by ZFMISC_1: 31;

      hence thesis by ZFMISC_1: 29;

    end;

    theorem :: FUNCT_4:86

    for a,b,c,d be set, f be Function st a in ( dom f) & c in ( dom f) & (f . a) = b & (f . c) = d holds ((a,c) --> (b,d)) c= f

    proof

      let a,b,c,d be set, f be Function;

      assume that

       A1: a in ( dom f) and

       A2: c in ( dom f) and

       A3: (f . a) = b & (f . c) = d;

      per cases ;

        suppose

         A4: a <> c;

         [a, b] in f & [c, d] in f by A1, A2, A3, FUNCT_1: 1;

        then { [a, b], [c, d]} c= f by ZFMISC_1: 32;

        hence thesis by A4, Th67;

      end;

        suppose a = c;

        hence thesis by A1, A3, Th85;

      end;

    end;

    theorem :: FUNCT_4:87

    

     Th87: for f,g,h be Function st f c= h & g c= h holds (f +* g) c= h

    proof

      let f,g,h be Function;

      assume f c= h & g c= h;

      then

       A1: (f \/ g) c= h by XBOOLE_1: 8;

      (f +* g) c= (f \/ g) by Th29;

      hence thesis by A1;

    end;

    theorem :: FUNCT_4:88

    for f,g be Function, A be set st (A /\ ( dom f)) c= (A /\ ( dom g)) holds ((f +* (g | A)) | A) = (g | A)

    proof

      let f,g be Function, A be set;

      assume

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

      

       A2: ( dom (f | A)) = (A /\ ( dom f)) & ( dom (g | A)) = (A /\ ( dom g)) by RELAT_1: 61;

      

      thus ((f +* (g | A)) | A) = ((f | A) +* ((g | A) | A)) by Th71

      .= ((f | A) +* (g | A))

      .= (g | A) by A1, A2, Th19;

    end;

    theorem :: FUNCT_4:89

    

     Th89: for f be Function, a,b,n,m be object holds (((f +* (a .--> b)) +* (m .--> n)) . m) = n

    proof

      let f be Function, a,b,n,m be object;

      set mn = (m .--> n);

      m in ( dom mn) by TARSKI:def 1;

      

      hence (((f +* (a .--> b)) +* mn) . m) = (mn . m) by Th13

      .= n by FUNCOP_1: 72;

    end;

    theorem :: FUNCT_4:90

    for f be Function, n,m be object holds (((f +* (n .--> m)) +* (m .--> n)) . n) = m

    proof

      let f be Function, n,m be object;

      set mn = (m .--> n), nm = (n .--> m);

      

       A1: m in ( dom mn) by TARSKI:def 1;

      per cases ;

        suppose

         A2: n = m;

        

        hence (((f +* nm) +* mn) . n) = (mn . m) by A1, Th13

        .= m by A2, FUNCOP_1: 72;

      end;

        suppose

         A3: n <> m;

        

         A4: n in ( dom nm) by TARSKI:def 1;

         not n in ( dom mn) by A3, TARSKI:def 1;

        

        hence (((f +* nm) +* mn) . n) = ((f +* nm) . n) by Th11

        .= (nm . n) by A4, Th13

        .= m by FUNCOP_1: 72;

      end;

    end;

    theorem :: FUNCT_4:91

    for f be Function, a,b,n,m,x be object st x <> m & x <> a holds (((f +* (a .--> b)) +* (m .--> n)) . x) = (f . x)

    proof

      let f be Function, a,b,n,m,x be object;

      assume that

       A1: x <> m and

       A2: x <> a;

      set mn = (m .--> n), nm = (a .--> b);

      

       A3: not x in ( dom nm) by A2, TARSKI:def 1;

       not x in ( dom mn) by A1, TARSKI:def 1;

      

      hence (((f +* nm) +* mn) . x) = ((f +* nm) . x) by Th11

      .= (f . x) by A3, Th11;

    end;

    theorem :: FUNCT_4:92

    f is one-to-one & g is one-to-one & ( rng f) misses ( rng g) implies (f +* g) is one-to-one

    proof

      set fg = (f +* g);

      assume that

       A1: f is one-to-one and

       A2: g is one-to-one and

       A3: ( rng f) misses ( rng g);

      let x1,x2 be object;

      assume that

       A4: x1 in ( dom fg) and

       A5: x2 in ( dom fg) and

       A6: (fg . x1) = (fg . x2);

      

       A7: x1 in ( dom f) or x1 in ( dom g) by A4, Th12;

      

       A8: x2 in ( dom f) or x2 in ( dom g) by A5, Th12;

      per cases ;

        suppose

         A9: x1 in ( dom g) & x2 in ( dom g);

        then (fg . x1) = (g . x1) & (fg . x2) = (g . x2) by Th13;

        hence thesis by A2, A6, A9;

      end;

        suppose

         A10: x1 in ( dom g) & not x2 in ( dom g);

        then x2 in ( dom f) by A5, Th12;

        then

         A11: (f . x2) in ( rng f) by FUNCT_1:def 3;

        

         A12: (g . x1) in ( rng g) by A10, FUNCT_1:def 3;

        (fg . x1) = (g . x1) & (fg . x2) = (f . x2) by A10, Th11, Th13;

        hence thesis by A3, A6, A12, A11, XBOOLE_0: 3;

      end;

        suppose

         A13: not x1 in ( dom g) & x2 in ( dom g);

        then x1 in ( dom f) by A4, Th12;

        then

         A14: (f . x1) in ( rng f) by FUNCT_1:def 3;

        

         A15: (g . x2) in ( rng g) by A13, FUNCT_1:def 3;

        (fg . x1) = (f . x1) & (fg . x2) = (g . x2) by A13, Th11, Th13;

        hence thesis by A3, A6, A15, A14, XBOOLE_0: 3;

      end;

        suppose

         A16: not x1 in ( dom g) & not x2 in ( dom g);

        then (fg . x1) = (f . x1) & (fg . x2) = (f . x2) by Th11;

        hence thesis by A1, A6, A7, A8, A16;

      end;

    end;

    registration

      let f,g be Function;

      reduce ((f +* g) +* g) to (f +* g);

      reducibility

      proof

        

        thus ((f +* g) +* g) = (f +* (g +* g)) by Th14

        .= (f +* g);

      end;

    end

    theorem :: FUNCT_4:93

    for f,g be Function holds ((f +* g) +* g) = (f +* g);

    theorem :: FUNCT_4:94

    for f,g,h be Function, D be set holds ((f +* g) | D) = (h | D) implies ((h +* g) | D) = ((f +* g) | D)

    proof

      let f,g,h be Function, D be set;

      assume

       A1: ((f +* g) | D) = (h | D);

      

       A2: ( dom ((f +* g) | D)) = (( dom (f +* g)) /\ D) by RELAT_1: 61

      .= ((( dom f) \/ ( dom g)) /\ D) by Def1;

      

       A3: ( dom ((h +* g) | D)) = (( dom (h +* g)) /\ D) by RELAT_1: 61

      .= ((( dom h) \/ ( dom g)) /\ D) by Def1;

      

      then

       A4: ( dom ((h +* g) | D)) = ((( dom h) /\ D) \/ (( dom g) /\ D)) by XBOOLE_1: 23

      .= (((( dom f) \/ ( dom g)) /\ D) \/ (( dom g) /\ D)) by A1, A2, RELAT_1: 61

      .= (((( dom f) \/ ( dom g)) \/ ( dom g)) /\ D) by XBOOLE_1: 23

      .= ((( dom f) \/ (( dom g) \/ ( dom g))) /\ D) by XBOOLE_1: 4

      .= ((( dom f) \/ ( dom g)) /\ D);

      now

        let x be object;

        assume

         A5: x in ( dom ((f +* g) | D));

        then

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

        

         A7: x in D by A2, A5, XBOOLE_0:def 4;

        

         A8: x in (( dom h) \/ ( dom g)) & (((h +* g) | D) . x) = ((h +* g) . x) by A2, A3, A4, A5, FUNCT_1: 47, XBOOLE_0:def 4;

        per cases ;

          suppose

           A9: x in ( dom g);

          (((f +* g) | D) . x) = ((f +* g) . x) by A5, FUNCT_1: 47

          .= (g . x) by A6, A9, Def1;

          hence (((h +* g) | D) . x) = (((f +* g) | D) . x) by A8, A9, Def1;

        end;

          suppose not x in ( dom g);

          

          hence (((h +* g) | D) . x) = (h . x) by A8, Def1

          .= (((f +* g) | D) . x) by A1, A7, FUNCT_1: 49;

        end;

      end;

      hence thesis by A2, A4;

    end;

    theorem :: FUNCT_4:95

    for f,g,h be Function, D be set holds (f | D) = (h | D) implies ((h +* g) | D) = ((f +* g) | D)

    proof

      let f,g,h be Function, D be set;

      assume

       A1: (f | D) = (h | D);

      

       A2: ( dom ((f +* g) | D)) = (( dom (f +* g)) /\ D) by RELAT_1: 61

      .= ((( dom f) \/ ( dom g)) /\ D) by Def1;

      

       A3: ( dom ((h +* g) | D)) = (( dom (h +* g)) /\ D) by RELAT_1: 61

      .= ((( dom h) \/ ( dom g)) /\ D) by Def1;

      

      then

       A4: ( dom ((h +* g) | D)) = ((( dom h) /\ D) \/ (( dom g) /\ D)) by XBOOLE_1: 23

      .= (( dom (f | D)) \/ (( dom g) /\ D)) by A1, RELAT_1: 61

      .= ((( dom f) /\ D) \/ (( dom g) /\ D)) by RELAT_1: 61

      .= ((( dom f) \/ ( dom g)) /\ D) by XBOOLE_1: 23;

      now

        let x be object;

        assume

         A5: x in ( dom ((f +* g) | D));

        then

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

        

         A7: x in D by A2, A5, XBOOLE_0:def 4;

        

         A8: x in (( dom h) \/ ( dom g)) & (((h +* g) | D) . x) = ((h +* g) . x) by A2, A3, A4, A5, FUNCT_1: 47, XBOOLE_0:def 4;

        per cases ;

          suppose

           A9: x in ( dom g);

          (((f +* g) | D) . x) = ((f +* g) . x) by A5, FUNCT_1: 47

          .= (g . x) by A6, A9, Def1;

          hence (((h +* g) | D) . x) = (((f +* g) | D) . x) by A8, A9, Def1;

        end;

          suppose

           A10: not x in ( dom g);

          

          then

           A11: (((h +* g) | D) . x) = (h . x) by A8, Def1

          .= ((h | D) . x) by A7, FUNCT_1: 49;

          

          thus (((f +* g) | D) . x) = ((f +* g) . x) by A5, FUNCT_1: 47

          .= (f . x) by A6, A10, Def1

          .= (((h +* g) | D) . x) by A1, A7, A11, FUNCT_1: 49;

        end;

      end;

      hence thesis by A2, A4;

    end;

    theorem :: FUNCT_4:96

    

     Th96: (x .--> x) = ( id {x})

    proof

      for y,z be object holds [y, z] in (x .--> x) iff y in {x} & y = z

      proof

        let y,z be object;

        

         A1: (x .--> x) = { [x, x]} by ZFMISC_1: 29;

        thus [y, z] in (x .--> x) implies y in {x} & y = z

        proof

          assume [y, z] in (x .--> x);

          then

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

          then y = x by XTUPLE_0: 1;

          hence thesis by A2, TARSKI:def 1, XTUPLE_0: 1;

        end;

        assume y in {x};

        then y = x by TARSKI:def 1;

        hence thesis by A1, TARSKI:def 1;

      end;

      hence thesis by RELAT_1:def 10;

    end;

    theorem :: FUNCT_4:97

    

     Th97: f c= g implies (f +* g) = g

    proof

      assume

       A1: f c= g;

      then f tolerates g by PARTFUN1: 54;

      

      hence (f +* g) = (f \/ g) by Th30

      .= g by A1, XBOOLE_1: 12;

    end;

    theorem :: FUNCT_4:98

    

     Th98: f c= g implies (g +* f) = g

    proof

      assume

       A1: f c= g;

      then f tolerates g by PARTFUN1: 54;

      

      hence (g +* f) = (f \/ g) by Th30

      .= g by A1, XBOOLE_1: 12;

    end;

    begin

    definition

      let f, x, y;

      :: FUNCT_4:def5

      func f +~ (x,y) -> set equals (f +* ((x .--> y) * f));

      coherence ;

    end

    registration

      let f, x, y;

      cluster (f +~ (x,y)) -> Relation-like Function-like;

      coherence ;

    end

    theorem :: FUNCT_4:99

    

     Th99: for x,y be object holds ( dom (f +~ (x,y))) = ( dom f)

    proof

      let x,y be object;

      

      thus ( dom (f +~ (x,y))) = (( dom f) \/ ( dom ((x .--> y) * f))) by Def1

      .= ( dom f) by RELAT_1: 25, XBOOLE_1: 12;

    end;

    theorem :: FUNCT_4:100

    

     Th100: for x,y be object holds x <> y implies not x in ( rng (f +~ (x,y)))

    proof

      let x,y be object;

      assume

       A1: x <> y;

      assume x in ( rng (f +~ (x,y)));

      then

      consider z be object such that

       A2: z in ( dom (f +~ (x,y))) and

       A3: ((f +~ (x,y)) . z) = x by FUNCT_1:def 3;

      

       A4: z in ( dom f) by A2, Th99;

       A5:

      now

        assume

         A6: not z in ( dom ((x .--> y) * f));

        then (f . z) = x by A3, Th11;

        then (f . z) in ( dom (x .--> y)) by FUNCOP_1: 74;

        hence contradiction by A4, A6, FUNCT_1: 11;

      end;

      ((x .--> y) . (f . z)) = (((x .--> y) * f) . z) by A4, FUNCT_1: 13

      .= x by A3, A5, Th13;

      then (f . z) <> x by A1, FUNCOP_1: 72;

      then not (f . z) in ( dom (x .--> y)) by FUNCOP_1: 75;

      hence thesis by A5, FUNCT_1: 11;

    end;

    theorem :: FUNCT_4:101

    for x,y be object holds x in ( rng f) implies y in ( rng (f +~ (x,y)))

    proof

      let x,y be object;

      assume x in ( rng f);

      then

      consider z be object such that

       A1: z in ( dom f) and

       A2: (f . z) = x by FUNCT_1:def 3;

      

       A3: ( dom ((x .--> y) * f)) c= ( dom (f +~ (x,y))) by Th10;

      x in ( dom (x .--> y)) by FUNCOP_1: 74;

      then

       A4: z in ( dom ((x .--> y) * f)) by A1, A2, FUNCT_1: 11;

      

      then ((f +~ (x,y)) . z) = (((x .--> y) * f) . z) by Th13

      .= ((x .--> y) . (f . z)) by A1, FUNCT_1: 13

      .= y by A2, FUNCOP_1: 72;

      hence thesis by A4, A3, FUNCT_1: 3;

    end;

    theorem :: FUNCT_4:102

    

     Th102: for x be object holds (f +~ (x,x)) = f

    proof

      let x be object;

      

      thus (f +~ (x,x)) = (f +* (( id {x}) * f)) by Th96

      .= f by Th98, RELAT_1: 50;

    end;

    theorem :: FUNCT_4:103

    

     Th103: for x,y be object holds not x in ( rng f) implies (f +~ (x,y)) = f

    proof

      let x,y be object;

      assume not x in ( rng f);

      then ( dom (x .--> y)) misses ( rng f) by ZFMISC_1: 50;

      then ((x .--> y) * f) = {} by RELAT_1: 44;

      hence thesis;

    end;

    theorem :: FUNCT_4:104

    for x,y be object holds ( rng (f +~ (x,y))) c= ((( rng f) \ {x}) \/ {y})

    proof

      let x,y be object;

      per cases ;

        suppose

         A1: not x in ( rng f);

        then (f +~ (x,y)) = f by Th103;

        then ( rng (f +~ (x,y))) = (( rng f) \ {x}) by A1, ZFMISC_1: 57;

        hence thesis by XBOOLE_1: 7;

      end;

        suppose that

         A2: x in ( rng f) and

         A3: x = y;

        (f +~ (x,y)) = f by A3, Th102;

        hence thesis by A2, A3, ZFMISC_1: 116;

      end;

        suppose that

         A4: x <> y;

         not x in ( rng (f +~ (x,y))) by A4, Th100;

        then

         A5: (( rng (f +~ (x,y))) \ {x}) = ( rng (f +~ (x,y))) by ZFMISC_1: 57;

        ( rng (x .--> y)) = {y} by FUNCOP_1: 8;

        then

         A6: (( rng f) \/ ( rng ((x .--> y) * f))) c= (( rng f) \/ {y}) by RELAT_1: 26, XBOOLE_1: 9;

        ( rng (f +~ (x,y))) c= (( rng f) \/ ( rng ((x .--> y) * f))) by Th17;

        then ( rng (f +~ (x,y))) c= (( rng f) \/ {y}) by A6;

        then ( rng (f +~ (x,y))) c= ((( rng f) \/ {y}) \ {x}) by A5, XBOOLE_1: 33;

        hence thesis by A4, ZFMISC_1: 123;

      end;

    end;

    theorem :: FUNCT_4:105

    for x,y,z be object holds (f . z) <> x implies ((f +~ (x,y)) . z) = (f . z)

    proof

      let x,y,z be object;

      assume (f . z) <> x;

      then not (f . z) in ( dom (x .--> y)) by FUNCOP_1: 75;

      then not z in ( dom ((x .--> y) * f)) by FUNCT_1: 11;

      hence thesis by Th11;

    end;

    theorem :: FUNCT_4:106

    z in ( dom f) & (f . z) = x implies ((f +~ (x,y)) . z) = y

    proof

      assume that

       A1: z in ( dom f) and

       A2: (f . z) = x;

      (f . z) in ( dom (x .--> y)) by A2, FUNCOP_1: 74;

      then

       A3: z in ( dom ((x .--> y) * f)) by A1, FUNCT_1: 11;

      

      hence ((f +~ (x,y)) . z) = (((x .--> y) * f) . z) by Th13

      .= ((x .--> y) . x) by A2, A3, FUNCT_1: 12

      .= y by FUNCOP_1: 72;

    end;

    theorem :: FUNCT_4:107

     not x in ( dom f) implies f c= (f +* (x .--> y))

    proof

      assume not x in ( dom f);

      then ( dom f) misses {x} by ZFMISC_1: 50;

      then ( dom f) misses ( dom (x .--> y));

      hence thesis by Th32;

    end;

    theorem :: FUNCT_4:108

    for f be PartFunc of X, Y, x, y st x in X & y in Y holds (f +* (x .--> y)) is PartFunc of X, Y

    proof

      let f be PartFunc of X, Y, x, y;

      assume that

       A1: x in X and

       A2: y in Y;

      

       A3: {x} c= X by A1, ZFMISC_1: 31;

       {y} c= Y by A2, ZFMISC_1: 31;

      then ( rng (x .--> y)) c= Y by FUNCOP_1: 8;

      then

       A4: (( rng f) \/ ( rng (x .--> y))) c= Y by XBOOLE_1: 8;

      ( rng (f +* (x .--> y))) c= (( rng f) \/ ( rng (x .--> y))) by Th17;

      then

       A5: ( rng (f +* (x .--> y))) c= Y by A4;

      ( dom (f +* (x .--> y))) = (( dom f) \/ ( dom (x .--> y))) by Def1

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

      hence thesis by A3, A5, RELSET_1: 4, XBOOLE_1: 8;

    end;

    registration

      let f be Function, g be non empty Function;

      cluster (f +* g) -> non empty;

      coherence

      proof

        ( dom (f +* g)) = (( dom f) \/ ( dom g)) by Def1;

        hence thesis;

      end;

      cluster (g +* f) -> non empty;

      coherence

      proof

        ( dom (g +* f)) = (( dom g) \/ ( dom f)) by Def1;

        hence thesis;

      end;

    end

    registration

      let f,g be non-empty Function;

      cluster (f +* g) -> non-empty;

      coherence

      proof

        set h = (f +* g);

        

         A1: ( dom (f +* g)) = (( dom f) \/ ( dom g)) by Def1;

         not {} in ( rng h)

        proof

          assume {} in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom (f +* g)) & {} = (h . x) by FUNCT_1:def 3;

           not x in ( dom g) or x in ( dom g);

          then {} = (f . x) & x in ( dom f) or {} = (g . x) & x in ( dom g) by A1, A2, Def1, XBOOLE_0:def 3;

          then {} in ( rng f) or {} in ( rng g) by FUNCT_1:def 3;

          hence thesis by RELAT_1:def 9;

        end;

        hence thesis by RELAT_1:def 9;

      end;

    end

    definition

      let X,Y be set;

      let f,g be PartFunc of X, Y;

      :: original: +*

      redefine

      func f +* g -> PartFunc of X, Y ;

      coherence

      proof

        

         A1: ( dom (f +* g)) c= (( dom f) \/ ( dom g)) by Def1;

        

         A2: ( dom (f +* g)) c= X by A1, XBOOLE_1: 1;

        

         A3: ( rng (f +* g)) c= (( rng f) \/ ( rng g)) by Th17;

        ( rng (f +* g)) c= Y by A3, XBOOLE_1: 1;

        then (f +* g) is Relation of X, Y by A2, RELSET_1: 4;

        hence thesis;

      end;

    end

    reserve x for set;

    theorem :: FUNCT_4:109

    ( dom ((x --> y) +* (x .--> z))) = ( succ x)

    proof

      

      thus ( dom ((x --> y) +* (x .--> z))) = (( dom (x --> y)) \/ ( dom (x .--> z))) by Def1

      .= (x \/ ( dom (x .--> z)))

      .= (x \/ {x})

      .= ( succ x) by ORDINAL1:def 1;

    end;

    theorem :: FUNCT_4:110

    ( dom (((x --> y) +* (x .--> z)) +* (( succ x) .--> z))) = ( succ ( succ x))

    proof

      

      thus ( dom (((x --> y) +* (x .--> z)) +* (( succ x) .--> z))) = (( dom ((x --> y) +* (x .--> z))) \/ ( dom (( succ x) .--> z))) by Def1

      .= ((( dom (x --> y)) \/ ( dom (x .--> z))) \/ ( dom (( succ x) .--> z))) by Def1

      .= ((x \/ ( dom (x .--> z))) \/ ( dom (( succ x) .--> z)))

      .= ((x \/ {x}) \/ ( dom (( succ x) .--> z)))

      .= ((x \/ {x}) \/ {( succ x)})

      .= (( succ x) \/ {( succ x)}) by ORDINAL1:def 1

      .= ( succ ( succ x)) by ORDINAL1:def 1;

    end;

    reserve x for object;

    registration

      let f,g be Function-yielding Function;

      cluster (f +* g) -> Function-yielding;

      coherence

      proof

        let x be object;

        assume x in ( dom (f +* g));

        then

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

        per cases by A1, XBOOLE_0:def 3;

          suppose x in ( dom g);

          then ((f +* g) . x) = (g . x) by Th13;

          hence ((f +* g) . x) is Function;

        end;

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

          then ((f +* g) . x) = (f . x) by Th11;

          hence ((f +* g) . x) is Function;

        end;

      end;

    end

    registration

      let I be set;

      let f,g be I -defined Function;

      cluster (f +* g) -> I -defined;

      coherence

      proof

        ( dom (f +* g)) = (( dom f) \/ ( dom g)) by Def1;

        then ( dom (f +* g)) c= I;

        hence thesis by RELAT_1:def 18;

      end;

    end

    registration

      let I be set;

      let f be totalI -defined Function;

      let g be I -defined Function;

      cluster (f +* g) -> total;

      coherence

      proof

        ( dom f) = I by PARTFUN1:def 2;

        

        then ( dom (f +* g)) = (I \/ ( dom g)) by Def1

        .= I by XBOOLE_1: 12;

        hence thesis;

      end;

      cluster (g +* f) -> total;

      coherence

      proof

        ( dom f) = I by PARTFUN1:def 2;

        

        then ( dom (g +* f)) = (I \/ ( dom g)) by Def1

        .= I by XBOOLE_1: 12;

        hence thesis;

      end;

    end

    registration

      let I be set;

      let g,h be I -valued Function;

      cluster (g +* h) -> I -valued;

      coherence

      proof

        

         A1: ( rng (g +* h)) c= (( rng g) \/ ( rng h)) by Th17;

        ( rng (g +* h)) c= I by A1, XBOOLE_1: 1;

        hence thesis by RELAT_1:def 19;

      end;

    end

    registration

      let f be Function;

      let g,h be f -compatible Function;

      cluster (g +* h) -> f -compatible;

      coherence

      proof

        let x be object;

        assume

         A1: x in ( dom (g +* h));

        

         A2: ( dom (g +* h)) = (( dom g) \/ ( dom h)) by Def1;

        per cases by A1, A2, XBOOLE_0:def 3;

          suppose

           A3: x in ( dom g) & not x in ( dom h);

          then (g . x) in (f . x) by FUNCT_1:def 14;

          hence ((g +* h) . x) in (f . x) by A3, Th11;

        end;

          suppose

           A4: x in ( dom h);

          then (h . x) in (f . x) by FUNCT_1:def 14;

          hence ((g +* h) . x) in (f . x) by A4, Th13;

        end;

      end;

    end

    theorem :: FUNCT_4:111

    ((f | A) +* f) = f by Th97, RELAT_1: 59;

    theorem :: FUNCT_4:112

    for R be Relation st ( dom R) = {x} & ( rng R) = {y} holds R = (x .--> y)

    proof

      let R be Relation;

      assume that

       A1: ( dom R) = {x} and

       A2: ( rng R) = {y};

      set g = (x .--> y);

      

       A3: g = { [x, y]} by ZFMISC_1: 29;

      for a,b be object holds [a, b] in R iff [a, b] in g

      proof

        let a,b be object;

        hereby

          assume

           A4: [a, b] in R;

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

          then

           A5: b = y by A2, TARSKI:def 1;

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

          then a = x by A1, TARSKI:def 1;

          hence [a, b] in g by A3, A5, TARSKI:def 1;

        end;

        assume [a, b] in g;

        then

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

        then

         A7: b = y by XTUPLE_0: 1;

        a = x by A6, XTUPLE_0: 1;

        then a in ( dom R) by A1, TARSKI:def 1;

        then

        consider z be object such that

         A8: [a, z] in R by XTUPLE_0:def 12;

        z in ( rng R) by A8, XTUPLE_0:def 13;

        hence thesis by A2, A7, A8, TARSKI:def 1;

      end;

      hence thesis by RELAT_1:def 2;

    end;

    theorem :: FUNCT_4:113

    ((f +* (x .--> y)) . x) = y

    proof

      

       A1: x in {x} by TARSKI:def 1;

      then ( dom (x .--> y)) = {x} & x in (( dom f) \/ {x}) by XBOOLE_0:def 3;

      

      hence ((f +* (x .--> y)) . x) = ((x .--> y) . x) by A1, Def1

      .= y by FUNCOP_1: 72;

    end;

    theorem :: FUNCT_4:114

    ((f +* (x .--> z1)) +* (x .--> z2)) = (f +* (x .--> z2))

    proof

      

       A1: ( dom (x .--> z1)) = {x}

      .= ( dom (x .--> z2));

      

      thus ((f +* (x .--> z1)) +* (x .--> z2)) = (f +* ((x .--> z1) +* (x .--> z2))) by Th14

      .= (f +* (x .--> z2)) by A1, Th19;

    end;

    registration

      let A be non empty set, a,b be Element of A, x,y be set;

      cluster ((a,b) --> (x,y)) -> A -defined;

      coherence ;

    end

    theorem :: FUNCT_4:115

    ( dom g) misses ( dom h) implies (((f +* g) +* h) +* g) = ((f +* g) +* h)

    proof

      assume

       A1: ( dom g) misses ( dom h);

      

      thus (((f +* g) +* h) +* g) = ((f +* (g +* h)) +* g) by Th14

      .= (f +* ((g +* h) +* g)) by Th14

      .= (f +* ((h +* g) +* g)) by A1, Th35

      .= (f +* (h +* g))

      .= (f +* (g +* h)) by A1, Th35

      .= ((f +* g) +* h) by Th14;

    end;

    theorem :: FUNCT_4:116

    ( dom f) misses ( dom h) & f c= (g +* h) implies f c= g

    proof

      assume that

       A1: ( dom f) misses ( dom h) and

       A2: f c= (g +* h);

      

       A3: ((g +* h) | ( dom f)) = ((g | ( dom f)) +* (h | ( dom f))) by Th71

      .= ((g | ( dom f)) +* {} ) by A1, RELAT_1: 66

      .= (g | ( dom f));

      (f | ( dom f)) = f;

      then f c= (g | ( dom f)) by A2, A3, RELAT_1: 76;

      hence f c= g by RELAT_1: 184;

    end;

    theorem :: FUNCT_4:117

    

     Th117: ( dom f) misses ( dom h) & f c= g implies f c= (g +* h)

    proof

      assume that

       A1: ( dom f) misses ( dom h) and

       A2: f c= g;

      

       A3: ((g +* h) | ( dom f)) = ((g | ( dom f)) +* (h | ( dom f))) by Th71

      .= ((g | ( dom f)) +* {} ) by A1, RELAT_1: 66

      .= (g | ( dom f));

      (f | ( dom f)) = f;

      then f c= ((g +* h) | ( dom f)) by A2, A3, RELAT_1: 76;

      hence f c= (g +* h) by RELAT_1: 184;

    end;

    theorem :: FUNCT_4:118

    ( dom g) misses ( dom h) implies ((f +* g) +* h) = ((f +* h) +* g)

    proof

      assume

       A1: ( dom g) misses ( dom h);

      

      thus ((f +* g) +* h) = (f +* (g +* h)) by Th14

      .= (f +* (h +* g)) by A1, Th35

      .= ((f +* h) +* g) by Th14;

    end;

    theorem :: FUNCT_4:119

    ( dom f) misses ( dom g) implies ((f +* g) \ g) = f

    proof

      assume

       A1: ( dom f) misses ( dom g);

      then

       A2: f misses g by RELAT_1: 179;

      

      thus ((f +* g) \ g) = ((f \/ g) \ g) by A1, Th31

      .= f by A2, XBOOLE_1: 88;

    end;

    theorem :: FUNCT_4:120

    ( dom f) misses ( dom g) implies (f \ g) = f by RELAT_1: 179, XBOOLE_1: 83;

    theorem :: FUNCT_4:121

    ( dom g) misses ( dom h) implies ((f \ g) +* h) = ((f +* h) \ g)

    proof

      assume

       A1: ( dom g) misses ( dom h);

      

       A2: ( dom (f +* h)) = (( dom f) \/ ( dom h)) by Def1;

      

       A3: ( dom ((f \ g) +* h)) = (( dom (f \ g)) \/ ( dom h)) by Def1;

      

       A4: ( dom ((f \ g) +* h)) = ( dom ((f +* h) \ g))

      proof

        thus ( dom ((f \ g) +* h)) c= ( dom ((f +* h) \ g))

        proof

          let x be object;

          assume

           A5: x in ( dom ((f \ g) +* h));

          per cases by A3, A5, XBOOLE_0:def 3;

            suppose that

             A6: x in ( dom (f \ g)) and

             A7: not x in ( dom h);

            consider y be object such that

             A8: [x, y] in (f \ g) by A6, XTUPLE_0:def 12;

            

             A9: x in ( dom f) by A8, XTUPLE_0:def 12;

            then

             A10: x in ( dom (f +* h)) by A2, XBOOLE_0:def 3;

            

             A11: not [x, y] in g by A8, XBOOLE_0:def 5;

            

             A12: ((f +* h) . x) = (f . x) by A7, Th11;

            reconsider y as set by TARSKI: 1;

            (f . x) = y by A8, A9, FUNCT_1:def 2;

            then [x, y] in (f +* h) by A12, A10, FUNCT_1:def 2;

            then [x, y] in ((f +* h) \ g) by A11, XBOOLE_0:def 5;

            hence thesis by XTUPLE_0:def 12;

          end;

            suppose

             A13: x in ( dom h);

            then

             A14: not x in ( dom g) by A1, XBOOLE_0: 3;

            x in ( dom (f +* h)) by A2, A13, XBOOLE_0:def 3;

            then

             A15: x in (( dom (f +* h)) \ ( dom g)) by A14, XBOOLE_0:def 5;

            (( dom (f +* h)) \ ( dom g)) c= ( dom ((f +* h) \ g)) by XTUPLE_0: 25;

            hence thesis by A15;

          end;

        end;

        let x be object;

        assume x in ( dom ((f +* h) \ g));

        then

        consider y be object such that

         A16: [x, y] in ((f +* h) \ g) by XTUPLE_0:def 12;

        reconsider y as set by TARSKI: 1;

        

         A17: x in ( dom (f +* h)) by A16, XTUPLE_0:def 12;

        then

         A18: y = ((f +* h) . x) by A16, FUNCT_1:def 2;

        per cases by A2, A17, XBOOLE_0:def 3;

          suppose that

           A19: x in ( dom f) and

           A20: not x in ( dom h);

          

           A21: not [x, y] in g by A16, XBOOLE_0:def 5;

          ((f +* h) . x) = (f . x) by A20, Th11;

          then [x, y] in f by A19, A18, FUNCT_1:def 2;

          then [x, y] in (f \ g) by A21, XBOOLE_0:def 5;

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

          hence thesis by A3, XBOOLE_0:def 3;

        end;

          suppose x in ( dom h);

          hence thesis by A3, XBOOLE_0:def 3;

        end;

      end;

      now

        let x be object;

        assume

         A22: x in ( dom ((f \ g) +* h));

        per cases by A3, A22, XBOOLE_0:def 3;

          suppose that

           A23: x in ( dom (f \ g)) and

           A24: not x in ( dom h);

          

          thus (((f \ g) +* h) . x) = ((f \ g) . x) by A24, Th11

          .= (f . x) by A23, GRFUNC_1: 2

          .= ((f +* h) . x) by A24, Th11

          .= (((f +* h) \ g) . x) by A4, A22, GRFUNC_1: 2;

        end;

          suppose

           A25: x in ( dom h);

          then

           A26: not x in ( dom g) by A1, XBOOLE_0: 3;

          x in ( dom (f +* h)) by A25, A2, XBOOLE_0:def 3;

          then x in (( dom (f +* h)) \ ( dom g)) by A26, XBOOLE_0:def 5;

          

          hence (((f +* h) \ g) . x) = ((f +* h) . x) by GRFUNC_1: 32

          .= (h . x) by A25, Th13

          .= (((f \ g) +* h) . x) by A25, Th13;

        end;

      end;

      hence thesis by A4;

    end;

    theorem :: FUNCT_4:122

    for f1,f2,g1,g2 be Function st f1 c= g1 & f2 c= g2 & ( dom f1) misses ( dom g2) holds (f1 +* f2) c= (g1 +* g2)

    proof

      let f1,f2,g1,g2 be Function such that

       A1: f1 c= g1 and

       A2: f2 c= g2 and

       A3: ( dom f1) misses ( dom g2);

      

       A4: f1 c= (g1 +* g2) by A1, A3, Th117;

      g2 c= (g1 +* g2) by Th25;

      then f2 c= (g1 +* g2) by A2;

      hence (f1 +* f2) c= (g1 +* g2) by A4, Th87;

    end;

    theorem :: FUNCT_4:123

    

     Th123: for f,g,h be Function st f c= g holds (f +* h) c= (g +* h)

    proof

      let f,g,h be Function;

      assume

       A1: f c= g;

      now

        ( dom (f +* h)) = (( dom f) \/ ( dom h)) & ( dom (g +* h)) = (( dom g) \/ ( dom h)) by Def1;

        hence ( dom (f +* h)) c= ( dom (g +* h)) by A1, RELAT_1: 11, XBOOLE_1: 9;

        let x be object;

        assume x in ( dom (f +* h));

        then

         A2: x in ( dom f) or x in ( dom h) by Th12;

        per cases ;

          suppose

           A3: x in ( dom h);

          

          hence ((f +* h) . x) = (h . x) by Th13

          .= ((g +* h) . x) by A3, Th13;

        end;

          suppose

           A4: not x in ( dom h);

          then ((f +* h) . x) = (f . x) & ((g +* h) . x) = (g . x) by Th11;

          hence ((f +* h) . x) = ((g +* h) . x) by A1, A2, A4, GRFUNC_1: 2;

        end;

      end;

      hence thesis by GRFUNC_1: 2;

    end;

    theorem :: FUNCT_4:124

    for f,g,h be Function st f c= g & ( dom f) misses ( dom h) holds f c= (g +* h)

    proof

      let f,g,h be Function;

      assume f c= g;

      then

       A1: (f +* h) c= (g +* h) by Th123;

      assume ( dom f) misses ( dom h);

      then f c= (f +* h) by Th32;

      hence thesis by A1;

    end;

    registration

      let x,y be set;

      cluster (x .--> y) -> trivial;

      coherence ;

    end

    theorem :: FUNCT_4:125

    for f,g,h be Function st f tolerates g & g tolerates h & h tolerates f holds (f +* g) tolerates h

    proof

      let f,g,h be Function such that

       A1: f tolerates g and

       A2: g tolerates h and

       A3: h tolerates f;

      let x be object;

      assume

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

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

      then

       A5: x in ( dom f) or x in ( dom g) by Th12;

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

      then x in (( dom h) /\ ( dom f)) & ((f +* g) . x) = (f . x) or x in (( dom g) /\ ( dom h)) & ((f +* g) . x) = (g . x) by A1, A5, Th13, Th15, XBOOLE_0:def 4;

      hence thesis by A2, A3;

    end;

    reserve A1,A2,B1,B2 for non empty set,

f for Function of A1, B1,

g for Function of A2, B2,

Y1 for non empty Subset of A1,

Y2 for non empty Subset of A2;

    definition

      let A,B be non empty set;

      let f be PartFunc of [:A, A:], A;

      let g be PartFunc of [:B, B:], B;

      :: original: |:

      redefine

      func |:f,g:| -> PartFunc of [: [:A, B:], [:A, B:]:], [:A, B:] ;

      coherence by Th59;

    end

    theorem :: FUNCT_4:126

    for f be PartFunc of [:A1, A1:], A1, g be PartFunc of [:A2, A2:], A2 holds for F be PartFunc of [:Y1, Y1:], Y1 st F = (f || Y1) holds for G be PartFunc of [:Y2, Y2:], Y2 st G = (g || Y2) holds |:F, G:| = ( |:f, g:| || [:Y1, Y2:])

    proof

      let f be PartFunc of [:A1, A1:], A1, g be PartFunc of [:A2, A2:], A2;

      let F be PartFunc of [:Y1, Y1:], Y1 such that

       A1: F = (f || Y1);

      

       A2: ( dom F) c= ( dom f) by A1, RELAT_1: 60;

      let G be PartFunc of [:Y2, Y2:], Y2 such that

       A3: G = (g || Y2);

      set X = ( dom |:F, G:|);

      

       A4: ( dom G) c= ( dom g) by A3, RELAT_1: 60;

      

       A5: X = ( dom ( |:f, g:| || [:Y1, Y2:]))

      proof

        thus X c= ( dom ( |:f, g:| || [:Y1, Y2:]))

        proof

          let x be object;

          assume x in X;

          then

          consider x11,x21,x12,x22 be object such that

           A6: x = [ [x11, x12], [x21, x22]] and

           A7: [x11, x21] in ( dom F) and

           A8: [x12, x22] in ( dom G) by Def3;

          

           A9: x12 in Y2 by A8, ZFMISC_1: 87;

          

           A10: x22 in Y2 by A8, ZFMISC_1: 87;

          x21 in Y1 by A7, ZFMISC_1: 87;

          then

           A11: [x21, x22] in [:Y1, Y2:] by A10, ZFMISC_1: 87;

          x11 in Y1 by A7, ZFMISC_1: 87;

          then [x11, x12] in [:Y1, Y2:] by A9, ZFMISC_1: 87;

          then

           A12: x in [: [:Y1, Y2:], [:Y1, Y2:]:] by A6, A11, ZFMISC_1: 87;

          x in ( dom |:f, g:|) by A2, A4, A6, A7, A8, Def3;

          then x in (( dom |:f, g:|) /\ [: [:Y1, Y2:], [:Y1, Y2:]:]) by A12, XBOOLE_0:def 4;

          hence thesis by RELAT_1: 61;

        end;

        let x be object;

        

         A13: ( dom F) = (( dom f) /\ [:Y1, Y1:]) by A1, RELAT_1: 61;

        assume x in ( dom ( |:f, g:| || [:Y1, Y2:]));

        then

         A14: x in (( dom |:f, g:|) /\ [: [:Y1, Y2:], [:Y1, Y2:]:]) by RELAT_1: 61;

        then

         A15: x in [: [:Y1, Y2:], [:Y1, Y2:]:] by XBOOLE_0:def 4;

        

         A16: ( dom G) = (( dom g) /\ [:Y2, Y2:]) by A3, RELAT_1: 61;

        x in ( dom |:f, g:|) by A14, XBOOLE_0:def 4;

        then

        consider x11,x21,x12,x22 be object such that

         A17: x = [ [x11, x12], [x21, x22]] and

         A18: [x11, x21] in ( dom f) and

         A19: [x12, x22] in ( dom g) by Def3;

        

         A20: [x21, x22] in [:Y1, Y2:] by A17, A15, ZFMISC_1: 87;

        then

         A21: x22 in Y2 by ZFMISC_1: 87;

        

         A22: [x11, x12] in [:Y1, Y2:] by A17, A15, ZFMISC_1: 87;

        then x12 in Y2 by ZFMISC_1: 87;

        then [x12, x22] in [:Y2, Y2:] by A21, ZFMISC_1: 87;

        then

         A23: [x12, x22] in ( dom G) by A19, A16, XBOOLE_0:def 4;

        

         A24: x21 in Y1 by A20, ZFMISC_1: 87;

        x11 in Y1 by A22, ZFMISC_1: 87;

        then [x11, x21] in [:Y1, Y1:] by A24, ZFMISC_1: 87;

        then [x11, x21] in ( dom F) by A18, A13, XBOOLE_0:def 4;

        hence thesis by A17, A23, Def3;

      end;

      now

        let x be set;

        assume

         A25: x in X;

        then

        consider x11,x21,x12,x22 be object such that

         A26: x = [ [x11, x12], [x21, x22]] and

         A27: [x11, x21] in ( dom F) and

         A28: [x12, x22] in ( dom G) by Def3;

        

        thus ( |:F, G:| . x) = ( |:F, G:| . ( [x11, x12], [x21, x22])) by A26

        .= [(F . (x11,x21)), (G . (x12,x22))] by A27, A28, Def3

        .= [(f . [x11, x21]), (G . [x12, x22])] by A1, A27, FUNCT_1: 47

        .= [(f . (x11,x21)), (g . (x12,x22))] by A3, A28, FUNCT_1: 47

        .= ( |:f, g:| . ( [x11, x12], [x21, x22])) by A2, A4, A27, A28, Def3

        .= (( |:f, g:| || [:Y1, Y2:]) . x) by A5, A25, A26, FUNCT_1: 47;

      end;

      then

       A29: for x be Element of [: [:Y1, Y2:], [:Y1, Y2:]:] st x in X holds ( |:F, G:| . x) = (( |:f, g:| || [:Y1, Y2:]) . x);

      thus thesis by A5, A29;

    end;

    theorem :: FUNCT_4:127

    for f be Function, x,y be object st x <> y holds ((f +~ (x,y)) +~ (x,z)) = (f +~ (x,y))

    proof

      let f be Function, x,y be object;

      assume x <> y;

      then not x in ( rng (f +~ (x,y))) by Th100;

      hence ((f +~ (x,y)) +~ (x,z)) = (f +~ (x,y)) by Th103;

    end;

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

    definition

      let a,b,c,x,y,z be object;

      :: FUNCT_4:def6

      func (a,b,c) --> (x,y,z) -> set equals (((a,b) --> (x,y)) +* (c .--> z));

      coherence ;

    end

    registration

      let a,b,c,x,y,z be object;

      cluster ((a,b,c) --> (x,y,z)) -> Function-like Relation-like;

      coherence ;

    end

    theorem :: FUNCT_4:128

    

     Th128: ( dom ((a,b,c) --> (x,y,z))) = {a, b, c}

    proof

      

       A1: ( dom ((a,b) --> (x,y))) = {a, b} & ( dom (c .--> z)) = {c} by Th62;

      

      thus ( dom ((a,b,c) --> (x,y,z))) = (( dom ((a,b) --> (x,y))) \/ ( dom (c .--> z))) by Def1

      .= {a, b, c} by A1, ENUMSET1: 3;

    end;

    theorem :: FUNCT_4:129

    ( rng ((a,b,c) --> (x,y,z))) c= {x, y, z}

    proof

      

       A1: ( {x, y} \/ {z}) = {x, y, z} by ENUMSET1: 3;

      

       A2: ( rng ((a,b,c) --> (x,y,z))) c= (( rng ((a,b) --> (x,y))) \/ ( rng (c .--> z))) by Th17;

      

       A3: ( rng (c .--> z)) = {z} by FUNCOP_1: 8;

      ( rng ((a,b) --> (x,y))) c= {x, y} by Th62;

      then (( rng ((a,b) --> (x,y))) \/ ( rng (c .--> z))) c= ( {x, y} \/ {z}) by A3, XBOOLE_1: 13;

      hence thesis by A2, A1;

    end;

    theorem :: FUNCT_4:130

    ((a,a,a) --> (x,y,z)) = (a .--> z)

    proof

      

      thus ((a,a,a) --> (x,y,z)) = ((a,a) --> (y,z)) by Th81

      .= (a .--> z) by Th81;

    end;

    theorem :: FUNCT_4:131

    ((a,a,b) --> (x,y,z)) = ((a,b) --> (y,z)) by Th81;

    theorem :: FUNCT_4:132

    

     Th132: a <> b implies ((a,b,a) --> (x,y,z)) = ((a,b) --> (z,y))

    proof

      assume

       A1: a <> b;

      

       A2: ( dom ((a,b,a) --> (x,y,z))) = {a, b, a} by Th128

      .= {a, a, b} by ENUMSET1: 57

      .= {a, b} by ENUMSET1: 30;

      hence ( dom ((a,b,a) --> (x,y,z))) = ( dom ((a,b) --> (z,y))) by Th62;

      let k be object;

      assume

       A3: k in ( dom ((a,b,a) --> (x,y,z)));

      per cases by A2, A3, TARSKI:def 2;

        suppose

         A4: k = a;

        

        hence (((a,b,a) --> (x,y,z)) . k) = z by Th89

        .= (((a,b) --> (z,y)) . k) by A1, A4, Th63;

      end;

        suppose

         A5: k = b;

        

        thus (((a,b,a) --> (x,y,z)) . k) = (((a .--> x) +* ((b,a) --> (y,z))) . k) by Th14

        .= y by A1, A5, Th84

        .= (((a,b) --> (z,y)) . k) by A5, Th63;

      end;

    end;

    theorem :: FUNCT_4:133

    ((a,b,b) --> (x,y,z)) = ((a,b) --> (x,z))

    proof

      

      thus ((a,b,b) --> (x,y,z)) = ((a .--> x) +* ((b,b) --> (y,z))) by Th14

      .= ((a,b) --> (x,z)) by Th81;

    end;

    theorem :: FUNCT_4:134

    

     Th134: a <> b & a <> c implies (((a,b,c) --> (x,y,z)) . a) = x

    proof

      assume that

       A1: a <> b and

       A2: a <> c;

       not a in ( dom (c .--> z)) by A2, TARSKI:def 1;

      

      hence (((a,b,c) --> (x,y,z)) . a) = (((a,b) --> (x,y)) . a) by Th11

      .= x by A1, Th63;

    end;

    theorem :: FUNCT_4:135

    

     Th135: (b <> c implies (((a,b,c) --> (x,y,z)) . b) = y) & (((a,b,c) --> (x,y,z)) . c) = z

    proof

      set f = ((a,b) --> (x,y));

      set g = (c .--> z);

      set h = ((a,b,c) --> (x,y,z));

      

       A1: c in {c} by TARSKI:def 1;

      

       A2: ( dom g) = {c};

      hereby

        assume b <> c;

        then

         A3: not b in {c} by TARSKI:def 1;

        

        thus (h . b) = (f . b) by A3, A2, Th11

        .= y by Th63;

      end;

      

      thus (h . c) = (g . c) by A1, A2, Th13

      .= z by FUNCOP_1: 72;

    end;

    theorem :: FUNCT_4:136

    for f be Function st ( dom f) = {a, b, c} & (f . a) = x & (f . b) = y & (f . c) = z holds f = ((a,b,c) --> (x,y,z))

    proof

      let f be Function such that

       A1: ( dom f) = {a, b, c} and

       A2: (f . a) = x & (f . b) = y & (f . c) = z;

      set g = ((a,b,c) --> (x,y,z));

      thus ( dom f) = ( dom g) by A1, Th128;

      let k be object;

      assume k in ( dom f);

      then

       A3: k = a or k = b or k = c by A1, ENUMSET1:def 1;

      per cases ;

        suppose (a,b,c) are_mutually_distinct ;

        hence thesis by A2, A3, Th134, Th135;

      end;

        suppose

         A4: a = b & a <> c;

        then g = ((a,c) --> (y,z)) by Th81;

        hence thesis by A4, A2, A3, Th63;

      end;

        suppose

         A5: a = c;

        per cases ;

          suppose

           A6: a <> b;

          then g = ((a,b) --> (z,y)) by A5, Th132;

          hence thesis by A5, A2, A3, A6, Th63;

        end;

          suppose a = b;

          hence thesis by A5, A2, A3, FUNCOP_1: 72;

        end;

      end;

        suppose

         A7: b = c & a <> c;

        thus thesis by A7, A2, A3, Th63;

      end;

    end;

    definition

      let x,y,w,z,a,b,c,d be object;

      :: FUNCT_4:def7

      func (x,y,w,z) --> (a,b,c,d) -> set equals (((x,y) --> (a,b)) +* ((w,z) --> (c,d)));

      coherence ;

    end

    registration

      let x,y,w,z,a,b,c,d be object;

      cluster ((x,y,w,z) --> (a,b,c,d)) -> Function-like Relation-like;

      coherence ;

    end

    theorem :: FUNCT_4:137

    

     Th137: ( dom ((x,y,w,z) --> (a,b,c,d))) = {x, y, w, z}

    proof

      set f = ((x,y) --> (a,b)), g = ((w,z) --> (c,d));

      

       A1: ( dom f) = {x, y} by Th62;

      ( dom g) = {w, z} by Th62;

      then (( dom f) \/ ( dom g)) = {x, y, w, z} by A1, ENUMSET1: 5;

      hence thesis by Def1;

    end;

    theorem :: FUNCT_4:138

    

     Th138: ( rng ((x,y,w,z) --> (a,b,c,d))) c= {a, b, c, d}

    proof

      set f = ((x,y) --> (a,b)), g = ((w,z) --> (c,d)), h = (((x,y) --> (a,b)) +* ((w,z) --> (c,d)));

      

       A1: ( rng f) c= {a, b} by Th62;

      ( rng g) c= {c, d} by Th62;

      then (( rng f) \/ ( rng g)) c= ( {a, b} \/ {c, d}) by A1, XBOOLE_1: 13;

      then

       A2: (( rng f) \/ ( rng g)) c= {a, b, c, d} by ENUMSET1: 5;

      ( rng h) c= (( rng f) \/ ( rng g)) by Th17;

      hence thesis by A2;

    end;

    theorem :: FUNCT_4:139

    

     Th139: (((x,y,w,z) --> (a,b,c,d)) . z) = d

    proof

      set f = ((x,y) --> (a,b)), g = ((w,z) --> (c,d));

      

       A1: (g . z) = d by Th63;

      

       A2: ( dom g) = {w, z} by Th62;

      z in ( dom g) by A2, TARSKI:def 2;

      hence thesis by A1, Th13;

    end;

    theorem :: FUNCT_4:140

    

     Th140: w <> z implies (((x,y,w,z) --> (a,b,c,d)) . w) = c

    proof

      assume

       A1: w <> z;

      

       A2: w <> z by A1;

      set f = ((x,y) --> (a,b)), g = ((w,z) --> (c,d));

      

       A3: (g . w) = c by A2, Th63;

      

       A4: ( dom g) = {w, z} by Th62;

      

       A5: w in ( dom g) by A4, TARSKI:def 2;

      thus thesis by A3, A5, Th13;

    end;

    theorem :: FUNCT_4:141

    

     Th141: y <> w & y <> z implies (((x,y,w,z) --> (a,b,c,d)) . y) = b

    proof

      assume that

       A1: y <> w and

       A2: y <> z;

      set f = ((x,y) --> (a,b)), g = ((w,z) --> (c,d));

      

       A3: (f . y) = b by Th63;

      

       A4: ( dom g) = {w, z} by Th62;

      

       A5: not y in ( dom g) by A1, A2, A4, TARSKI:def 2;

      thus thesis by A3, A5, Th11;

    end;

    theorem :: FUNCT_4:142

    

     Th142: x <> y & x <> w & x <> z implies (((x,y,w,z) --> (a,b,c,d)) . x) = a

    proof

      assume that

       A1: x <> y and

       A2: x <> w and

       A3: x <> z;

      set f = ((x,y) --> (a,b)), g = ((w,z) --> (c,d));

      

       A4: (f . x) = a by A1, Th63;

      ( dom g) = {w, z} by Th62;

      then

       A5: not x in ( dom g) by A2, A3, TARSKI:def 2;

      thus thesis by A4, A5, Th11;

    end;

    theorem :: FUNCT_4:143

    (x,y,w,z) are_mutually_distinct implies ( rng ((x,y,w,z) --> (a,b,c,d))) = {a, b, c, d}

    proof

      set h = ((x,y,w,z) --> (a,b,c,d));

      assume

       A1: (x,y,w,z) are_mutually_distinct ;

      

       A2: ( rng h) c= {a, b, c, d} by Th138;

       {a, b, c, d} c= ( rng h)

      proof

        set h = ((x,y,w,z) --> (a,b,c,d));

        let y1 be object;

        assume y1 in {a, b, c, d};

        then

         A3: y1 = a or y1 = b or y1 = c or y1 = d by ENUMSET1:def 2;

        

         A4: ( dom h) = {x, y, w, z} by Th137;

        

         A5: (h . x) = y1 or (h . y) = y1 or (h . w) = y1 or (h . z) = y1 by A1, A3, Th139, Th140, Th141, Th142;

        

         A6: x in ( dom h) by A4, ENUMSET1:def 2;

        

         A7: y in ( dom h) by A4, ENUMSET1:def 2;

        

         A8: w in ( dom h) by A4, ENUMSET1:def 2;

        z in ( dom h) by A4, ENUMSET1:def 2;

        hence thesis by A5, A6, A7, A8, FUNCT_1:def 3;

      end;

      hence thesis by A2;

    end;

    theorem :: FUNCT_4:144

    for a,b,c,d,e,i,j,k be object, g be Function st ( dom g) = {a, b, c, d} & (g . a) = e & (g . b) = i & (g . c) = j & (g . d) = k holds g = ((a,b,c,d) --> (e,i,j,k))

    proof

      let a,b,c,d,e,i,j,k be object;

      let h be Function such that

       A1: ( dom h) = {a, b, c, d} and

       A2: (h . a) = e and

       A3: (h . b) = i and

       A4: (h . c) = j and

       A5: (h . d) = k;

      set f = ((a,b) --> (e,i));

      set g = ((c,d) --> (j,k));

      

       A6: ( dom f) = {a, b} by Th62;

      

       A7: ( dom g) = {c, d} by Th62;

      then

       A8: ( dom h) = (( dom f) \/ ( dom g)) by A1, A6, ENUMSET1: 5;

      now

        let x be object such that

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

        thus x in ( dom g) implies (h . x) = (g . x)

        proof

          assume

           A10: x in ( dom g);

          per cases by A7, A10, TARSKI:def 2;

            suppose x = c & c <> d;

            hence thesis by A4, Th63;

          end;

            suppose x = d;

            hence thesis by A5, Th63;

          end;

        end;

        thus not x in ( dom g) implies (h . x) = (f . x)

        proof

          assume not x in ( dom g);

          then

           A11: x in ( dom f) by A9, XBOOLE_0:def 3;

          per cases by A6, A11, TARSKI:def 2;

            suppose x = a & a <> b;

            hence thesis by A2, Th63;

          end;

            suppose x = b;

            hence thesis by A3, Th63;

          end;

        end;

      end;

      hence thesis by A8, Def1;

    end;

    theorem :: FUNCT_4:145

    for a,c,b,d,x,y,z,w be object holds (a,c,x,w) are_mutually_distinct implies ((a,c,x,w) --> (b,d,y,z)) = { [a, b], [c, d], [x, y], [w, z]}

    proof

      let a,c,b,d,x,y,z,w be object;

      assume

       A1: (a,c,x,w) are_mutually_distinct ;

      then

       A2: a <> c;

      

       A3: a <> x by A1;

      

       A4: a <> w by A1;

      

       A5: c <> x by A1;

      

       A6: c <> w by A1;

      

       A7: x <> w by A1;

      set m = ((a,c) --> (b,d)), n = ((x,w) --> (y,z));

      

       A8: ( dom m) = {a, c} by Th62;

      

       A9: ( dom n) = {x, w} by Th62;

      

       A10: not a in {x, w} by A3, A4, TARSKI:def 2;

       not c in {x, w} by A5, A6, TARSKI:def 2;

      

      then ((a,c,x,w) --> (b,d,y,z)) = (m \/ n) by A8, A9, A10, Th31, ZFMISC_1: 51

      .= ( { [a, b], [c, d]} \/ n) by A2, Th67

      .= ( { [a, b], [c, d]} \/ { [x, y], [w, z]}) by A7, Th67

      .= { [a, b], [c, d], [x, y], [w, z]} by ENUMSET1: 5;

      hence thesis;

    end;

    theorem :: FUNCT_4:146

    for a,b,c,d,x,y,z,w,x9,y9,z9,w9 be object st (a,b,c,d) are_mutually_distinct & ((a,b,c,d) --> (x,y,z,w)) = ((a,b,c,d) --> (x9,y9,z9,w9)) holds x = x9 & y = y9 & z = z9 & w = w9

    proof

      let a,b,c,d,x,y,z,w,x9,y9,z9,w9 be object such that

       A1: (a,b,c,d) are_mutually_distinct and

       A2: ((a,b,c,d) --> (x,y,z,w)) = ((a,b,c,d) --> (x9,y9,z9,w9));

      

       A3: x = (((a,b,c,d) --> (x,y,z,w)) . a) by A1, Th142

      .= x9 by A1, A2, Th142;

      

       A4: y = (((a,b,c,d) --> (x,y,z,w)) . b) by A1, Th141

      .= y9 by A1, A2, Th141;

      

       A5: z = (((a,b,c,d) --> (x,y,z,w)) . c) by A1, Th140

      .= z9 by A1, A2, Th140;

      w = (((a,b,c,d) --> (x,y,z,w)) . d) by Th139

      .= w9 by A2, Th139;

      hence thesis by A3, A4, A5;

    end;

    theorem :: FUNCT_4:147

    for a1,a2,a3,b1,b2,b3 be object st (a1,a2,a3) are_mutually_distinct holds ( rng ((a1,a2,a3) --> (b1,b2,b3))) = {b1, b2, b3}

    proof

      let a1,a2,a3,b1,b2,b3 be object;

      assume

       A1: (a1,a2,a3) are_mutually_distinct ;

      set f = ((a1,a2,a3) --> (b1,b2,b3));

      thus ( rng f) c= {b1, b2, b3}

      proof

        let x be object;

        assume x in ( rng f);

        then

        consider y be object such that

         A2: y in ( dom f) & x = (f . y) by FUNCT_1:def 3;

        ( dom f) = {a1, a2, a3} by Th128;

        then y = a1 or y = a2 or y = a3 by A2, ENUMSET1:def 1;

        then x = b1 or x = b2 or x = b3 by A2, A1, Th134, Th135;

        hence thesis by ENUMSET1:def 1;

      end;

      let x be object;

      assume x in {b1, b2, b3};

      then

       A3: x = b1 or x = b2 or x = b3 by ENUMSET1:def 1;

      

       A4: a1 in {a1, a2, a3} & a2 in {a1, a2, a3} & a3 in {a1, a2, a3} by ENUMSET1:def 1;

      

       A5: ( dom f) = {a1, a2, a3} by Th128;

      (f . a1) = b1 & (f . a2) = b2 & (f . a3) = b3 by A1, Th134, Th135;

      hence thesis by A3, A4, A5, FUNCT_1:def 3;

    end;

    definition

      let C,D,E be non empty set;

      let f be Function of [:C, D:], E;

      :: original: ~

      redefine

      :: FUNCT_4:def8

      func ~ f -> Function of [:D, C:], E means for d be Element of D, c be Element of C holds (it . (d,c)) = (f . (c,d));

      coherence

      proof

        thus ( ~ f) is Function of [:D, C:], E;

      end;

      compatibility

      proof

        let g be Function of [:D, C:], E;

        

         A1: ( dom g) = [:D, C:] by FUNCT_2:def 1;

        hence g = ( ~ f) implies for d be Element of D, c be Element of C holds (g . (d,c)) = (f . (c,d)) by ZFMISC_1: 87, Th43;

        assume

         A3: for d be Element of D, c be Element of C holds (g . (d,c)) = (f . (c,d));

        thus

         A6: ( dom g) = ( dom ( ~ f)) by A1, FUNCT_2:def 1;

        let x be object;

        assume x in ( dom g);

        then

        consider d be Element of D, c be Element of C such that

         A4: x = [d, c] by SUBSET_1: 43;

        

        thus (g . x) = (g . (d,c)) by A4

        .= (f . (c,d)) by A3

        .= (( ~ f) . (d,c)) by A1, A6, ZFMISC_1: 87, Th43

        .= (( ~ f) . x) by A4;

      end;

    end