funct_5.miz



    begin

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

x,y,z,t,x1,x2 for object,

f,g,h,f1,f2,g1,g2 for Function;

    scheme :: FUNCT_5:sch1

    LambdaFS { FS() -> set , f( object) -> object } :

ex f st ( dom f) = FS() & for g st g in FS() holds (f . g) = f(g);

      consider f such that

       A1: ( dom f) = FS() & for x be object st x in FS() holds (f . x) = f(x) from FUNCT_1:sch 3;

      take f;

      thus thesis by A1;

    end;

    theorem :: FUNCT_5:1

    

     Th1: ( ~ {} ) = {}

    proof

       [: {} qua set, {} :] = {} & ( dom {} ) = {} by ZFMISC_1: 90;

      then ( dom ( ~ {} )) = {} by FUNCT_4: 46;

      hence thesis;

    end;

    ::$Canceled

    theorem :: FUNCT_5:8

    

     Th2: ( proj1 {} ) = {} & ( proj2 {} ) = {} ;

    theorem :: FUNCT_5:9

    

     Th3: Y <> {} or [:X, Y:] <> {} or [:Y, X:] <> {} implies ( proj1 [:X, Y:]) = X & ( proj2 [:Y, X:]) = X

    proof

      set y = the Element of Y;

      assume Y <> {} or [:X, Y:] <> {} or [:Y, X:] <> {} ;

      then

       A1: Y <> {} by ZFMISC_1: 90;

      now

        let x be object;

        x in X implies [x, y] in [:X, Y:] by A1, ZFMISC_1: 87;

        hence x in X iff ex y be object st [x, y] in [:X, Y:] by ZFMISC_1: 87;

      end;

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

      now

        let x be object;

        x in X implies [y, x] in [:Y, X:] by A1, ZFMISC_1: 87;

        hence x in X iff ex y be object st [y, x] in [:Y, X:] by ZFMISC_1: 87;

      end;

      hence thesis by XTUPLE_0:def 13;

    end;

    theorem :: FUNCT_5:10

    

     Th4: ( proj1 [:X, Y:]) c= X & ( proj2 [:X, Y:]) c= Y

    proof

      thus ( proj1 [:X, Y:]) c= X

      proof

        let x be object;

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

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

        hence thesis by ZFMISC_1: 87;

      end;

      let y be object;

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

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

      hence thesis by ZFMISC_1: 87;

    end;

    theorem :: FUNCT_5:11

    

     Th5: Z c= [:X, Y:] implies ( proj1 Z) c= X & ( proj2 Z) c= Y

    proof

      assume Z c= [:X, Y:];

      then

       A1: ( proj1 Z) c= ( proj1 [:X, Y:]) & ( proj2 Z) c= ( proj2 [:X, Y:]) by XTUPLE_0: 8, XTUPLE_0: 9;

      ( proj1 [:X, Y:]) c= X & ( proj2 [:X, Y:]) c= Y by Th4;

      hence thesis by A1;

    end;

    theorem :: FUNCT_5:12

    

     Th6: ( proj1 { [x, y]}) = {x} & ( proj2 { [x, y]}) = {y}

    proof

      thus ( proj1 { [x, y]}) c= {x}

      proof

        let z be object;

        assume z in ( proj1 { [x, y]});

        then

        consider t be object such that

         A1: [z, t] in { [x, y]} by XTUPLE_0:def 12;

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

        then z = x by XTUPLE_0: 1;

        hence thesis by TARSKI:def 1;

      end;

      thus {x} c= ( proj1 { [x, y]})

      proof

        let z be object;

        assume z in {x};

        then z = x by TARSKI:def 1;

        then [z, y] in { [x, y]} by TARSKI:def 1;

        hence thesis by XTUPLE_0:def 12;

      end;

      thus ( proj2 { [x, y]}) c= {y}

      proof

        let z be object;

        assume z in ( proj2 { [x, y]});

        then

        consider t be object such that

         A2: [t, z] in { [x, y]} by XTUPLE_0:def 13;

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

        then z = y by XTUPLE_0: 1;

        hence thesis by TARSKI:def 1;

      end;

      thus {y} c= ( proj2 { [x, y]})

      proof

        let z be object;

        assume z in {y};

        then z = y by TARSKI:def 1;

        then [x, z] in { [x, y]} by TARSKI:def 1;

        hence thesis by XTUPLE_0:def 13;

      end;

    end;

    theorem :: FUNCT_5:13

    ( proj1 { [x, y], [z, t]}) = {x, z} & ( proj2 { [x, y], [z, t]}) = {y, t}

    proof

      

       A1: ( proj2 { [x, y]}) = {y} & ( proj2 { [z, t]}) = {t} by Th6;

       { [x, y], [z, t]} = ( { [x, y]} \/ { [z, t]}) by ENUMSET1: 1;

      then

       A2: ( proj1 { [x, y], [z, t]}) = (( proj1 { [x, y]}) \/ ( proj1 { [z, t]})) & ( proj2 { [x, y], [z, t]}) = (( proj2 { [x, y]}) \/ ( proj2 { [z, t]})) by XTUPLE_0: 23, XTUPLE_0: 27;

      ( proj1 { [x, y]}) = {x} & ( proj1 { [z, t]}) = {z} by Th6;

      hence thesis by A2, A1, ENUMSET1: 1;

    end;

    theorem :: FUNCT_5:14

    

     Th8: not (ex x,y be object st [x, y] in X) implies ( proj1 X) = {} & ( proj2 X) = {}

    proof

      set x = the Element of ( proj2 X);

      assume

       A1: not (ex x,y be object st [x, y] in X);

      hereby

        set x = the Element of ( proj1 X);

        assume ( proj1 X) <> {} ;

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

        hence contradiction by A1;

      end;

      assume ( proj2 X) <> {} ;

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

      hence thesis by A1;

    end;

    theorem :: FUNCT_5:15

    ( proj1 X) = {} or ( proj2 X) = {} implies not ex x,y be object st [x, y] in X by XTUPLE_0:def 12, XTUPLE_0:def 13;

    theorem :: FUNCT_5:16

    ( proj1 X) = {} iff ( proj2 X) = {}

    proof

      ( proj1 X) = {} or ( proj2 X) = {} implies not ex x,y be object st [x, y] in X by XTUPLE_0:def 12, XTUPLE_0:def 13;

      hence thesis by Th8;

    end;

    theorem :: FUNCT_5:17

    

     Th11: ( proj1 ( dom f)) = ( proj2 ( dom ( ~ f))) & ( proj2 ( dom f)) = ( proj1 ( dom ( ~ f)))

    proof

      thus ( proj1 ( dom f)) c= ( proj2 ( dom ( ~ f)))

      proof

        let x be object;

        assume x in ( proj1 ( dom f));

        then

        consider y be object such that

         A1: [x, y] in ( dom f) by XTUPLE_0:def 12;

         [y, x] in ( dom ( ~ f)) by A1, FUNCT_4: 42;

        hence thesis by XTUPLE_0:def 13;

      end;

      thus ( proj2 ( dom ( ~ f))) c= ( proj1 ( dom f))

      proof

        let y be object;

        assume y in ( proj2 ( dom ( ~ f)));

        then

        consider x be object such that

         A2: [x, y] in ( dom ( ~ f)) by XTUPLE_0:def 13;

         [y, x] in ( dom f) by A2, FUNCT_4: 42;

        hence thesis by XTUPLE_0:def 12;

      end;

      thus ( proj2 ( dom f)) c= ( proj1 ( dom ( ~ f)))

      proof

        let y be object;

        assume y in ( proj2 ( dom f));

        then

        consider x be object such that

         A3: [x, y] in ( dom f) by XTUPLE_0:def 13;

         [y, x] in ( dom ( ~ f)) by A3, FUNCT_4: 42;

        hence thesis by XTUPLE_0:def 12;

      end;

      thus ( proj1 ( dom ( ~ f))) c= ( proj2 ( dom f))

      proof

        let x be object;

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

        then

        consider y be object such that

         A4: [x, y] in ( dom ( ~ f)) by XTUPLE_0:def 12;

         [y, x] in ( dom f) by A4, FUNCT_4: 42;

        hence thesis by XTUPLE_0:def 13;

      end;

    end;

    definition

      let f;

      :: FUNCT_5:def1

      func curry f -> Function means

      : Def1: ( dom it ) = ( proj1 ( dom f)) & for x be object st x in ( proj1 ( dom f)) holds ex g st (it . x) = g & ( dom g) = ( proj2 (( dom f) /\ [: {x}, ( proj2 ( dom f)):])) & for y st y in ( dom g) holds (g . y) = (f . (x,y));

      existence

      proof

        defpred F[ object, Function] means ( dom $2) = ( proj2 (( dom f) /\ [: {$1}, ( proj2 ( dom f)):])) & for y st y in ( dom $2) holds ($2 . y) = (f . ($1,y));

        defpred P[ object, object] means ex g st $2 = g & F[$1, g];

        

         A1: for x,y,z be object st x in ( proj1 ( dom f)) & P[x, y] & P[x, z] holds y = z

        proof

          let x,y,z be object such that x in ( proj1 ( dom f));

          given g1 be Function such that

           A2: y = g1 and

           A3: F[x, g1];

          given g2 be Function such that

           A4: z = g2 and

           A5: F[x, g2];

          now

            let t be object;

            assume

             A6: t in ( proj2 (( dom f) /\ [: {x}, ( proj2 ( dom f)):]));

            then (g1 . t) = (f . (x,t)) by A3;

            hence (g1 . t) = (g2 . t) by A5, A6;

          end;

          hence thesis by A2, A3, A4, A5, FUNCT_1: 2;

        end;

        

         A7: for x be object st x in ( proj1 ( dom f)) holds ex y be object st P[x, y]

        proof

          let x be object such that x in ( proj1 ( dom f));

          deffunc F( object) = (f . [x, $1]);

          consider g such that

           A8: ( dom g) = ( proj2 (( dom f) /\ [: {x}, ( proj2 ( dom f)):])) & for y be object st y in ( proj2 (( dom f) /\ [: {x}, ( proj2 ( dom f)):])) holds (g . y) = F(y) from FUNCT_1:sch 3;

          reconsider y = g as set;

          take A = y, B = g;

          thus thesis by A8;

        end;

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

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be Function such that

         A9: ( dom f1) = ( proj1 ( dom f)) and

         A10: for x be object st x in ( proj1 ( dom f)) holds ex g st (f1 . x) = g & ( dom g) = ( proj2 (( dom f) /\ [: {x}, ( proj2 ( dom f)):])) & for y st y in ( dom g) holds (g . y) = (f . (x,y)) and

         A11: ( dom f2) = ( proj1 ( dom f)) and

         A12: for x be object st x in ( proj1 ( dom f)) holds ex g st (f2 . x) = g & ( dom g) = ( proj2 (( dom f) /\ [: {x}, ( proj2 ( dom f)):])) & for y st y in ( dom g) holds (g . y) = (f . (x,y));

        now

          let x be object;

          assume

           A13: x in ( proj1 ( dom f));

          then

          consider g1 be Function such that

           A14: (f1 . x) = g1 and

           A15: ( dom g1) = ( proj2 (( dom f) /\ [: {x}, ( proj2 ( dom f)):])) and

           A16: for y st y in ( dom g1) holds (g1 . y) = (f . (x,y)) by A10;

          consider g2 be Function such that

           A17: (f2 . x) = g2 and

           A18: ( dom g2) = ( proj2 (( dom f) /\ [: {x}, ( proj2 ( dom f)):])) and

           A19: for y st y in ( dom g2) holds (g2 . y) = (f . (x,y)) by A12, A13;

          now

            let y be object;

            assume

             A20: y in ( proj2 (( dom f) /\ [: {x}, ( proj2 ( dom f)):]));

            then (g1 . y) = (f . (x,y)) by A15, A16;

            hence (g1 . y) = (g2 . y) by A18, A19, A20;

          end;

          hence (f1 . x) = (f2 . x) by A14, A15, A17, A18, FUNCT_1: 2;

        end;

        hence thesis by A9, A11;

      end;

      :: FUNCT_5:def2

      func uncurry f -> Function means

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

      existence

      proof

        defpred Q[ object, object] means ex g st g = (f . ($1 `1 )) & $2 = (g . ($1 `2 ));

        deffunc F( Function) = ( dom $1);

        defpred P[ object] means (f . $1) is Function;

        consider X such that

         A21: for x be object holds x in X iff x in ( dom f) & P[x] from XBOOLE_0:sch 1;

        defpred P[ object] means for g1 st g1 = (f . ($1 `1 )) holds ($1 `2 ) in ( dom g1);

        consider g such that

         A22: ( dom g) = (f .: X) & for g1 st g1 in (f .: X) holds (g . g1) = F(g1) from LambdaFS;

        consider Y such that

         A23: for x be object holds x in Y iff x in [:X, ( union ( rng g)):] & P[x] from XBOOLE_0:sch 1;

        

         A24: for x be object st x in Y holds ex y be object st Q[x, y]

        proof

          let x be object;

          assume x in Y;

          then x in [:X, ( union ( rng g)):] by A23;

          then (x `1 ) in X by MCART_1: 10;

          then

          reconsider h = (f . (x `1 )) as Function by A21;

          take (h . (x `2 )), h;

          thus thesis;

        end;

        

         A25: for x,x1,x2 be object st x in Y & Q[x, x1] & Q[x, x2] holds x1 = x2;

        consider F be Function such that

         A26: ( dom F) = Y & for x be object st x in Y holds Q[x, (F . x)] from FUNCT_1:sch 2( A25, A24);

        take F;

        thus for t be object holds t in ( dom F) iff ex x, g, y st t = [x, y] & x in ( dom f) & g = (f . x) & y in ( dom g)

        proof

          let t be object;

          thus t in ( dom F) implies ex x, g, y st t = [x, y] & x in ( dom f) & g = (f . x) & y in ( dom g)

          proof

            assume

             A27: t in ( dom F);

            take x = (t `1 );

            t in [:X, ( union ( rng g)):] by A23, A26, A27;

            then

             A28: x in X by MCART_1: 10;

            then

            reconsider h = (f . x) as Function by A21;

            take h, (t `2 );

            thus thesis by A21, A23, A26, A27, A28, MCART_1: 21;

          end;

          given x be object, h be Function, y be object such that

           A29: t = [x, y] and

           A30: x in ( dom f) and

           A31: h = (f . x) and

           A32: y in ( dom h);

          

           A33: x in X by A21, A30, A31;

          then h in (f .: X) by A30, A31, FUNCT_1:def 6;

          then (g . h) = ( dom h) & (g . h) in ( rng g) by A22, FUNCT_1:def 3;

          then ( dom h) c= ( union ( rng g)) by ZFMISC_1: 74;

          then

           A34: t in [:X, ( union ( rng g)):] by A29, A32, A33, ZFMISC_1: 87;

          for g1 st g1 = (f . (t `1 )) holds (t `2 ) in ( dom g1) by A29, A31, A32;

          hence thesis by A23, A26, A34;

        end;

        let x;

        let h be Function;

        assume that

         A35: x in ( dom F) and

         A36: h = (f . (x `1 ));

        ex g st g = (f . (x `1 )) & (F . x) = (g . (x `2 )) by A26, A35;

        hence thesis by A36;

      end;

      uniqueness

      proof

        defpred P[ object] means ex x, g, y st $1 = [x, y] & x in ( dom f) & g = (f . x) & y in ( dom g);

        let f1, f2;

        assume that

         A37: for t be object holds t in ( dom f1) iff P[t] and

         A38: for x, g st x in ( dom f1) & g = (f . (x `1 )) holds (f1 . x) = (g . (x `2 )) and

         A39: for t be object holds t in ( dom f2) iff P[t] and

         A40: for x, g st x in ( dom f2) & g = (f . (x `1 )) holds (f2 . x) = (g . (x `2 ));

        

         A41: ( dom f1) = ( dom f2) from XBOOLE_0:sch 2( A37, A39);

        now

          let x be object;

          assume

           A42: x in ( dom f1);

          then

          consider z, g, y such that

           A43: x = [z, y] and z in ( dom f) and

           A44: g = (f . z) and y in ( dom g) by A37;

          

           A45: z = (x `1 ) & y = (x `2 ) by A43;

          then (f1 . x) = (g . y) by A38, A42, A44;

          hence (f1 . x) = (f2 . x) by A40, A41, A42, A44, A45;

        end;

        hence thesis by A41;

      end;

    end

    definition

      let f;

      :: FUNCT_5:def3

      func curry' f -> Function equals ( curry ( ~ f));

      correctness ;

      :: FUNCT_5:def4

      func uncurry' f -> Function equals ( ~ ( uncurry f));

      correctness ;

    end

    ::$Canceled

    registration

      let f;

      cluster ( curry f) -> Function-yielding;

      coherence

      proof

        let x be object;

        assume x in ( dom ( curry f));

        then

         A1: x in ( proj1 ( dom f)) by Def1;

        ex g st (( curry f) . x) = g & ( dom g) = ( proj2 (( dom f) /\ [: {x}, ( proj2 ( dom f)):])) & for y st y in ( dom g) holds (g . y) = (f . (x,y)) by A1, Def1;

        hence thesis;

      end;

    end

    theorem :: FUNCT_5:19

    

     Th12: for x,y be object holds [x, y] in ( dom f) implies x in ( dom ( curry f))

    proof

      let x,y be object;

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

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

      hence x in ( dom ( curry f)) by Def1;

    end;

    theorem :: FUNCT_5:20

    

     Th13: for x,y be object holds [x, y] in ( dom f) & g = (( curry f) . x) implies y in ( dom g) & (g . y) = (f . (x,y))

    proof

      let x,y be object;

      assume that

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

       A2: g = (( curry f) . x);

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

      then

       A3: ex h st (( curry f) . x) = h & ( dom h) = ( proj2 (( dom f) /\ [: {x}, ( proj2 ( dom f)):])) & for y st y in ( dom h) holds (h . y) = (f . (x,y)) by Def1;

      y in ( proj2 ( dom f)) by A1, XTUPLE_0:def 13;

      then [x, y] in [: {x}, ( proj2 ( dom f)):] by ZFMISC_1: 105;

      then [x, y] in (( dom f) /\ [: {x}, ( proj2 ( dom f)):]) by A1, XBOOLE_0:def 4;

      hence y in ( dom g) by A2, A3, XTUPLE_0:def 13;

      hence thesis by A2, A3;

    end;

    registration

      let f;

      cluster ( curry' f) -> Function-yielding;

      coherence ;

    end

    theorem :: FUNCT_5:21

    for x,y be object holds [x, y] in ( dom f) implies y in ( dom ( curry' f))

    proof

      let x,y be object;

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

      then [y, x] in ( dom ( ~ f)) by FUNCT_4: 42;

      then y in ( dom ( curry' f)) by Th12;

      hence thesis;

    end;

    theorem :: FUNCT_5:22

    

     Th15: for x,y be object holds [x, y] in ( dom f) & g = (( curry' f) . y) implies x in ( dom g) & (g . x) = (f . (x,y))

    proof

      let x,y be object;

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

      then

       A1: [y, x] in ( dom ( ~ f)) by FUNCT_4: 42;

      assume

       A2: g = (( curry' f) . y);

      then (g . x) = (( ~ f) . (y,x)) by A1, Th13;

      hence thesis by A1, A2, Th13, FUNCT_4: 43;

    end;

    theorem :: FUNCT_5:23

    ( dom ( curry' f)) = ( proj2 ( dom f))

    proof

      ( dom ( curry ( ~ f))) = ( proj1 ( dom ( ~ f))) by Def1;

      hence thesis by Th11;

    end;

    theorem :: FUNCT_5:24

    

     Th17: [:X, Y:] <> {} & ( dom f) = [:X, Y:] implies ( dom ( curry f)) = X & ( dom ( curry' f)) = Y

    proof

      assume that

       A1: [:X, Y:] <> {} and

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

      ( dom ( curry f)) = ( proj1 ( dom f)) by Def1;

      hence ( dom ( curry f)) = X by A1, A2, Th3;

      

      thus ( dom ( curry' f)) = ( proj1 ( dom ( ~ f))) by Def1

      .= ( proj1 [:Y, X:]) by A2, FUNCT_4: 46

      .= Y by A1, Th3;

    end;

    theorem :: FUNCT_5:25

    

     Th18: ( dom f) c= [:X, Y:] implies ( dom ( curry f)) c= X & ( dom ( curry' f)) c= Y

    proof

      assume

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

      ( dom ( curry f)) = ( proj1 ( dom f)) by Def1;

      hence ( dom ( curry f)) c= X by A1, Th5;

      

       A2: ( dom ( curry' f)) = ( proj1 ( dom ( ~ f))) by Def1;

      ( dom ( ~ f)) c= [:Y, X:] by A1, FUNCT_4: 45;

      hence thesis by A2, Th5;

    end;

    theorem :: FUNCT_5:26

    

     Th19: ( rng f) c= ( Funcs (X,Y)) implies ( dom ( uncurry f)) = [:( dom f), X:] & ( dom ( uncurry' f)) = [:X, ( dom f):]

    proof

      defpred P[ object] means ex x, g, y st $1 = [x, y] & x in ( dom f) & g = (f . x) & y in ( dom g);

      assume

       A1: ( rng f) c= ( Funcs (X,Y));

      

       A2: for t be object holds t in [:( dom f), X:] iff P[t]

      proof

        let t be object;

        thus t in [:( dom f), X:] implies ex x, g, y st t = [x, y] & x in ( dom f) & g = (f . x) & y in ( dom g)

        proof

          assume

           A3: t in [:( dom f), X:];

          then (t `1 ) in ( dom f) by MCART_1: 10;

          then (f . (t `1 )) in ( rng f) by FUNCT_1:def 3;

          then

          consider g such that

           A4: (f . (t `1 )) = g & ( dom g) = X and ( rng g) c= Y by A1, FUNCT_2:def 2;

          take (t `1 ), g, (t `2 );

          thus thesis by A3, A4, MCART_1: 10, MCART_1: 21;

        end;

        given x, g, y such that

         A5: t = [x, y] and

         A6: x in ( dom f) and

         A7: g = (f . x) and

         A8: y in ( dom g);

        g in ( rng f) by A6, A7, FUNCT_1:def 3;

        then ex g1 st g = g1 & ( dom g1) = X & ( rng g1) c= Y by A1, FUNCT_2:def 2;

        hence thesis by A5, A6, A8, ZFMISC_1: 87;

      end;

      

       A9: for t be object holds t in ( dom ( uncurry f)) iff P[t] by Def2;

      thus ( dom ( uncurry f)) = [:( dom f), X:] from XBOOLE_0:sch 2( A9, A2);

      hence thesis by FUNCT_4: 46;

    end;

    theorem :: FUNCT_5:27

     not (ex x,y be object st [x, y] in ( dom f)) implies ( curry f) = {} & ( curry' f) = {}

    proof

      assume

       A1: not ex x,y be object st [x, y] in ( dom f);

      then ( proj1 ( dom f)) = {} by Th8;

      then ( dom ( curry f)) = {} by Def1;

      hence ( curry f) = {} ;

      now

        let x,y be object;

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

        then [y, x] in ( dom f) by FUNCT_4: 42;

        hence contradiction by A1;

      end;

      then ( proj1 ( dom ( ~ f))) = {} by Th8;

      then ( dom ( curry ( ~ f))) = {} by Def1;

      hence thesis;

    end;

    theorem :: FUNCT_5:28

     not (ex x st x in ( dom f) & (f . x) is Function) implies ( uncurry f) = {} & ( uncurry' f) = {}

    proof

      assume

       A1: not (ex x st x in ( dom f) & (f . x) is Function);

       A2:

      now

        set t = the Element of ( dom ( uncurry f));

        assume ( dom ( uncurry f)) <> {} ;

        then ex x, g, y st t = [x, y] & x in ( dom f) & g = (f . x) & y in ( dom g) by Def2;

        hence contradiction by A1;

      end;

      hence ( uncurry f) = {} ;

      thus thesis by A2, Th1, RELAT_1: 41;

    end;

    theorem :: FUNCT_5:29

    

     Th22: [:X, Y:] <> {} & ( dom f) = [:X, Y:] & x in X implies ex g st (( curry f) . x) = g & ( dom g) = Y & ( rng g) c= ( rng f) & for y st y in Y holds (g . y) = (f . (x,y))

    proof

      assume that

       A1: [:X, Y:] <> {} and

       A2: ( dom f) = [:X, Y:] and

       A3: x in X;

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

      then

       A4: ( [: {x}, Y:] /\ ( dom f)) = [: {x}, Y:] by A2, ZFMISC_1: 101;

      x in ( proj1 ( dom f)) by A1, A2, A3, Th3;

      then

      consider g such that

       A5: (( curry f) . x) = g and

       A6: ( dom g) = ( proj2 (( dom f) /\ [: {x}, ( proj2 ( dom f)):])) & for y st y in ( dom g) holds (g . y) = (f . (x,y)) by Def1;

      take g;

      

       A7: ( proj2 [: {x}, Y:]) = Y by Th3;

      

       A8: ( proj2 ( dom f)) = Y by A2, A3, Th3;

      ( rng g) c= ( rng f)

      proof

        let z be object;

        assume z in ( rng g);

        then

        consider y be object such that

         A9: y in ( dom g) & z = (g . y) by FUNCT_1:def 3;

         [x, y] in ( dom f) & z = (f . (x,y)) by A2, A3, A6, A8, A4, A7, A9, ZFMISC_1: 87;

        hence thesis by FUNCT_1:def 3;

      end;

      hence thesis by A5, A6, A8, A4, A7;

    end;

    theorem :: FUNCT_5:30

    

     Th23: x in ( dom ( curry f)) implies (( curry f) . x) is Function

    proof

      assume

       A1: x in ( dom ( curry f));

      ( dom ( curry f)) = ( proj1 ( dom f)) by Def1;

      then ex g st (( curry f) . x) = g & ( dom g) = ( proj2 (( dom f) /\ [: {x}, ( proj2 ( dom f)):])) & for y st y in ( dom g) holds (g . y) = (f . (x,y)) by A1, Def1;

      hence thesis;

    end;

    theorem :: FUNCT_5:31

    

     Th24: x in ( dom ( curry f)) & g = (( curry f) . x) implies ( dom g) = ( proj2 (( dom f) /\ [: {x}, ( proj2 ( dom f)):])) & ( dom g) c= ( proj2 ( dom f)) & ( rng g) c= ( rng f) & for y st y in ( dom g) holds (g . y) = (f . (x,y)) & [x, y] in ( dom f)

    proof

      assume that

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

       A2: g = (( curry f) . x);

      ( dom ( curry f)) = ( proj1 ( dom f)) by Def1;

      then

      consider h such that

       A3: (( curry f) . x) = h and

       A4: ( dom h) = ( proj2 (( dom f) /\ [: {x}, ( proj2 ( dom f)):])) and

       A5: for y st y in ( dom h) holds (h . y) = (f . (x,y)) by A1, Def1;

      thus ( dom g) = ( proj2 (( dom f) /\ [: {x}, ( proj2 ( dom f)):])) by A2, A3, A4;

      (( dom f) /\ [: {x}, ( proj2 ( dom f)):]) c= ( dom f) by XBOOLE_1: 17;

      hence ( dom g) c= ( proj2 ( dom f)) by A2, A3, A4, XTUPLE_0: 9;

      thus ( rng g) c= ( rng f)

      proof

        let y be object;

        assume y in ( rng g);

        then

        consider z be object such that

         A6: z in ( dom g) and

         A7: y = (g . z) by FUNCT_1:def 3;

        consider t be object such that

         A8: [t, z] in (( dom f) /\ [: {x}, ( proj2 ( dom f)):]) by A2, A3, A4, A6, XTUPLE_0:def 13;

         [t, z] in ( dom f) & [t, z] in [: {x}, ( proj2 ( dom f)):] by A8, XBOOLE_0:def 4;

        then

         A9: [x, z] in ( dom f) by ZFMISC_1: 105;

        (h . z) = (f . (x,z)) by A2, A3, A5, A6;

        hence thesis by A2, A3, A7, A9, FUNCT_1:def 3;

      end;

      let y;

      assume

       A10: y in ( dom g);

      then

      consider t be object such that

       A11: [t, y] in (( dom f) /\ [: {x}, ( proj2 ( dom f)):]) by A2, A3, A4, XTUPLE_0:def 13;

       [t, y] in ( dom f) & [t, y] in [: {x}, ( proj2 ( dom f)):] by A11, XBOOLE_0:def 4;

      hence thesis by A2, A3, A5, A10, ZFMISC_1: 105;

    end;

    theorem :: FUNCT_5:32

    

     Th25: [:X, Y:] <> {} & ( dom f) = [:X, Y:] & y in Y implies ex g st (( curry' f) . y) = g & ( dom g) = X & ( rng g) c= ( rng f) & for x st x in X holds (g . x) = (f . (x,y))

    proof

      assume that

       A1: [:X, Y:] <> {} and

       A2: ( dom f) = [:X, Y:] and

       A3: y in Y;

      

       A4: ( dom ( ~ f)) = [:Y, X:] by A2, FUNCT_4: 46;

      X <> {} by A1, ZFMISC_1: 90;

      then

      consider g such that

       A5: (( curry ( ~ f)) . y) = g & ( dom g) = X & ( rng g) c= ( rng ( ~ f)) and

       A6: for x st x in X holds (g . x) = (( ~ f) . (y,x)) by A3, A4, Th22;

      take g;

      ( rng ( ~ f)) c= ( rng f) by FUNCT_4: 41;

      hence (( curry' f) . y) = g & ( dom g) = X & ( rng g) c= ( rng f) by A5;

      let x;

      assume

       A7: x in X;

      then

       A8: (g . x) = (( ~ f) . (y,x)) by A6;

       [y, x] in ( dom ( ~ f)) by A3, A4, A7, ZFMISC_1: 87;

      hence thesis by A8, FUNCT_4: 43;

    end;

    theorem :: FUNCT_5:33

    x in ( dom ( curry' f)) implies (( curry' f) . x) is Function by Th23;

    theorem :: FUNCT_5:34

    x in ( dom ( curry' f)) & g = (( curry' f) . x) implies ( dom g) = ( proj1 (( dom f) /\ [:( proj1 ( dom f)), {x}:])) & ( dom g) c= ( proj1 ( dom f)) & ( rng g) c= ( rng f) & for y st y in ( dom g) holds (g . y) = (f . (y,x)) & [y, x] in ( dom f)

    proof

      

       A1: ( rng ( ~ f)) c= ( rng f) by FUNCT_4: 41;

      assume

       A2: x in ( dom ( curry' f)) & g = (( curry' f) . x);

      then ( dom g) = ( proj2 (( dom ( ~ f)) /\ [: {x}, ( proj2 ( dom ( ~ f))):])) by Th24;

      then

       A3: ( dom g) = ( proj2 (( dom ( ~ f)) /\ [: {x}, ( proj1 ( dom f)):])) by Th11;

      thus

       A4: ( dom g) c= ( proj1 (( dom f) /\ [:( proj1 ( dom f)), {x}:]))

      proof

        let z be object;

        assume z in ( dom g);

        then

        consider y be object such that

         A5: [y, z] in (( dom ( ~ f)) /\ [: {x}, ( proj1 ( dom f)):]) by A3, XTUPLE_0:def 13;

         [y, z] in [: {x}, ( proj1 ( dom f)):] by A5, XBOOLE_0:def 4;

        then

         A6: [z, y] in [:( proj1 ( dom f)), {x}:] by ZFMISC_1: 88;

         [y, z] in ( dom ( ~ f)) by A5, XBOOLE_0:def 4;

        then [z, y] in ( dom f) by FUNCT_4: 42;

        then [z, y] in (( dom f) /\ [:( proj1 ( dom f)), {x}:]) by A6, XBOOLE_0:def 4;

        hence thesis by XTUPLE_0:def 12;

      end;

      thus ( proj1 (( dom f) /\ [:( proj1 ( dom f)), {x}:])) c= ( dom g)

      proof

        let z be object;

        assume z in ( proj1 (( dom f) /\ [:( proj1 ( dom f)), {x}:]));

        then

        consider y be object such that

         A7: [z, y] in (( dom f) /\ [:( proj1 ( dom f)), {x}:]) by XTUPLE_0:def 12;

         [z, y] in [:( proj1 ( dom f)), {x}:] by A7, XBOOLE_0:def 4;

        then

         A8: [y, z] in [: {x}, ( proj1 ( dom f)):] by ZFMISC_1: 88;

         [z, y] in ( dom f) by A7, XBOOLE_0:def 4;

        then [y, z] in ( dom ( ~ f)) by FUNCT_4: 42;

        then [y, z] in (( dom ( ~ f)) /\ [: {x}, ( proj1 ( dom f)):]) by A8, XBOOLE_0:def 4;

        hence thesis by A3, XTUPLE_0:def 13;

      end;

      ( dom g) c= ( proj2 ( dom ( ~ f))) & ( rng g) c= ( rng ( ~ f)) by A2, Th24;

      hence ( dom g) c= ( proj1 ( dom f)) & ( rng g) c= ( rng f) by A1, Th11;

      let y;

      assume

       A9: y in ( dom g);

      then

      consider z be object such that

       A10: [y, z] in (( dom f) /\ [:( proj1 ( dom f)), {x}:]) by A4, XTUPLE_0:def 12;

       [y, z] in [:( proj1 ( dom f)), {x}:] by A10, XBOOLE_0:def 4;

      then

       A11: z = x by ZFMISC_1: 106;

       [y, z] in ( dom f) by A10, XBOOLE_0:def 4;

      then [z, y] in ( dom ( ~ f)) by FUNCT_4: 42;

      then (( ~ f) . (x,y)) = (f . (y,x)) by A11, FUNCT_4: 43;

      hence thesis by A2, A9, A10, A11, Th24, XBOOLE_0:def 4;

    end;

    theorem :: FUNCT_5:35

    

     Th28: ( dom f) = [:X, Y:] implies ( rng ( curry f)) c= ( Funcs (Y,( rng f))) & ( rng ( curry' f)) c= ( Funcs (X,( rng f)))

    proof

      assume

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

       A2:

      now

        assume

         A3: [:X, Y:] <> {} ;

        then

         A4: ( dom ( curry f)) = X by A1, Th17;

        thus ( rng ( curry f)) c= ( Funcs (Y,( rng f)))

        proof

          let z be object;

          assume z in ( rng ( curry f));

          then

          consider x be object such that

           A5: x in ( dom ( curry f)) and

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

          ex g st (( curry f) . x) = g & ( dom g) = Y & ( rng g) c= ( rng f) & for y st y in Y holds (g . y) = (f . (x,y)) by A1, A3, A4, A5, Th22;

          hence thesis by A6, FUNCT_2:def 2;

        end;

        

         A7: ( dom ( curry' f)) = Y by A1, A3, Th17;

        thus ( rng ( curry' f)) c= ( Funcs (X,( rng f)))

        proof

          let z be object;

          assume z in ( rng ( curry' f));

          then

          consider y be object such that

           A8: y in ( dom ( curry' f)) and

           A9: z = (( curry' f) . y) by FUNCT_1:def 3;

          ex g st (( curry' f) . y) = g & ( dom g) = X & ( rng g) c= ( rng f) & for x st x in X holds (g . x) = (f . (x,y)) by A1, A3, A7, A8, Th25;

          hence thesis by A9, FUNCT_2:def 2;

        end;

      end;

      now

        assume

         A10: ( dom f) = {} ;

        then X = {} or Y = {} by A1;

        then

         A11: [:Y, X:] = {} by ZFMISC_1: 90;

         {} = ( dom ( curry f)) by A10, Def1, Th2;

        then

         A12: ( rng ( curry f)) = {} by RELAT_1: 42;

        ( dom ( ~ f)) = [:Y, X:] & ( dom ( curry ( ~ f))) = ( proj1 ( dom ( ~ f))) by A1, Def1, FUNCT_4: 46;

        then ( rng ( curry' f)) = {} by A11, Th2, RELAT_1: 42;

        hence thesis by A12;

      end;

      hence thesis by A1, A2;

    end;

    theorem :: FUNCT_5:36

    ( rng ( curry f)) c= ( PFuncs (( proj2 ( dom f)),( rng f))) & ( rng ( curry' f)) c= ( PFuncs (( proj1 ( dom f)),( rng f)))

    proof

      

       A1: ( rng ( ~ f)) c= ( rng f) by FUNCT_4: 41;

      thus ( rng ( curry f)) c= ( PFuncs (( proj2 ( dom f)),( rng f)))

      proof

        let t be object;

        assume t in ( rng ( curry f));

        then

        consider z be object such that

         A2: z in ( dom ( curry f)) and

         A3: t = (( curry f) . z) by FUNCT_1:def 3;

        ( dom ( curry f)) = ( proj1 ( dom f)) by Def1;

        then

        consider g such that

         A4: (( curry f) . z) = g and ( dom g) = ( proj2 (( dom f) /\ [: {z}, ( proj2 ( dom f)):])) and for y st y in ( dom g) holds (g . y) = (f . (z,y)) by A2, Def1;

        ( dom g) c= ( proj2 ( dom f)) & ( rng g) c= ( rng f) by A2, A4, Th24;

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

      end;

      let t be object;

      assume t in ( rng ( curry' f));

      then

      consider z be object such that

       A5: z in ( dom ( curry' f)) and

       A6: t = (( curry' f) . z) by FUNCT_1:def 3;

      ( dom ( curry ( ~ f))) = ( proj1 ( dom ( ~ f))) by Def1;

      then

      consider g such that

       A7: (( curry ( ~ f)) . z) = g and ( dom g) = ( proj2 (( dom ( ~ f)) /\ [: {z}, ( proj2 ( dom ( ~ f))):])) and for y st y in ( dom g) holds (g . y) = (( ~ f) . (z,y)) by A5, Def1;

      ( rng g) c= ( rng ( ~ f)) by A5, A7, Th24;

      then

       A8: ( rng g) c= ( rng f) by A1;

      ( dom g) c= ( proj2 ( dom ( ~ f))) by A5, A7, Th24;

      then ( dom g) c= ( proj1 ( dom f)) by Th11;

      hence thesis by A6, A7, A8, PARTFUN1:def 3;

    end;

    theorem :: FUNCT_5:37

    

     Th30: ( rng f) c= ( PFuncs (X,Y)) implies ( dom ( uncurry f)) c= [:( dom f), X:] & ( dom ( uncurry' f)) c= [:X, ( dom f):]

    proof

      assume

       A1: ( rng f) c= ( PFuncs (X,Y));

      thus

       A2: ( dom ( uncurry f)) c= [:( dom f), X:]

      proof

        let x be object;

        assume x in ( dom ( uncurry f));

        then

        consider y, g, z such that

         A3: x = [y, z] and

         A4: y in ( dom f) and

         A5: g = (f . y) and

         A6: z in ( dom g) by Def2;

        g in ( rng f) by A4, A5, FUNCT_1:def 3;

        then g is PartFunc of X, Y by A1, PARTFUN1: 46;

        then ( dom g) c= X by RELAT_1:def 18;

        hence thesis by A3, A4, A6, ZFMISC_1: 87;

      end;

      let x be object;

      assume x in ( dom ( uncurry' f));

      then ex y,z be object st x = [z, y] & [y, z] in ( dom ( uncurry f)) by FUNCT_4:def 2;

      hence thesis by A2, ZFMISC_1: 88;

    end;

    theorem :: FUNCT_5:38

    

     Th31: x in ( dom f) & g = (f . x) & y in ( dom g) implies [x, y] in ( dom ( uncurry f)) & (( uncurry f) . (x,y)) = (g . y) & (g . y) in ( rng ( uncurry f))

    proof

      assume that

       A1: x in ( dom f) and

       A2: g = (f . x) and

       A3: y in ( dom g);

      thus

       A4: [x, y] in ( dom ( uncurry f)) by A1, A2, A3, Def2;

      ( [x, y] `1 ) = x & ( [x, y] `2 ) = y;

      hence (( uncurry f) . (x,y)) = (g . y) by A2, A4, Def2;

      hence thesis by A4, FUNCT_1:def 3;

    end;

    theorem :: FUNCT_5:39

    x in ( dom f) & g = (f . x) & y in ( dom g) implies [y, x] in ( dom ( uncurry' f)) & (( uncurry' f) . (y,x)) = (g . y) & (g . y) in ( rng ( uncurry' f))

    proof

      assume

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

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

      hence

       A2: [y, x] in ( dom ( uncurry' f)) by FUNCT_4: 42;

      (( uncurry f) . (x,y)) = (g . y) by A1, Th31;

      hence (( uncurry' f) . (y,x)) = (g . y) by A2, FUNCT_4: 43;

      hence thesis by A2, FUNCT_1:def 3;

    end;

    theorem :: FUNCT_5:40

    

     Th33: ( rng f) c= ( PFuncs (X,Y)) implies ( rng ( uncurry f)) c= Y & ( rng ( uncurry' f)) c= Y

    proof

      assume

       A1: ( rng f) c= ( PFuncs (X,Y));

      thus

       A2: ( rng ( uncurry f)) c= Y

      proof

        let x be object;

        assume x in ( rng ( uncurry f));

        then

        consider y be object such that

         A3: y in ( dom ( uncurry f)) and

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

        consider z, g, t such that

         A5: y = [z, t] and

         A6: z in ( dom f) & g = (f . z) and

         A7: t in ( dom g) by A3, Def2;

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

        then

         A8: ex g1 st g = g1 & ( dom g1) c= X & ( rng g1) c= Y by A1, PARTFUN1:def 3;

        (( uncurry f) . (z,t)) = (g . t) & (g . t) in ( rng g) by A6, A7, Th31, FUNCT_1:def 3;

        hence thesis by A4, A5, A8;

      end;

      ( rng ( uncurry' f)) c= ( rng ( uncurry f)) by FUNCT_4: 41;

      hence thesis by A2;

    end;

    theorem :: FUNCT_5:41

    

     Th34: ( rng f) c= ( Funcs (X,Y)) implies ( rng ( uncurry f)) c= Y & ( rng ( uncurry' f)) c= Y

    proof

      

       A1: ( Funcs (X,Y)) c= ( PFuncs (X,Y)) by FUNCT_2: 72;

      assume ( rng f) c= ( Funcs (X,Y));

      then ( rng f) c= ( PFuncs (X,Y)) by A1;

      hence thesis by Th33;

    end;

    theorem :: FUNCT_5:42

    

     Th35: ( curry {} ) = {} & ( curry' {} ) = {} by Def1, Th1;

    theorem :: FUNCT_5:43

    

     Th36: ( uncurry {} ) = {} & ( uncurry' {} ) = {}

    proof

       A1:

      now

        set t = the Element of ( dom ( uncurry {} ));

        assume ( dom ( uncurry {} )) <> {} ;

        then ex x, g, y st t = [x, y] & x in ( dom {} ) & g = ( {} . x) & y in ( dom g) by Def2;

        hence contradiction;

      end;

      hence ( uncurry {} ) = {} ;

      thus thesis by A1, Th1, RELAT_1: 41;

    end;

    theorem :: FUNCT_5:44

    

     Th37: ( dom f1) = [:X, Y:] & ( dom f2) = [:X, Y:] & ( curry f1) = ( curry f2) implies f1 = f2

    proof

      assume that

       A1: ( dom f1) = [:X, Y:] and

       A2: ( dom f2) = [:X, Y:] and

       A3: ( curry f1) = ( curry f2);

       A4:

      now

        assume [:X, Y:] <> {} ;

        now

          let z be object;

          assume

           A5: z in [:X, Y:];

          then

          consider g1 be Function such that

           A6: (( curry f1) . (z `1 )) = g1 and ( dom g1) = Y and ( rng g1) c= ( rng f1) and

           A7: for y st y in Y holds (g1 . y) = (f1 . ((z `1 ),y)) by A1, Th22, MCART_1: 10;

          

           A8: z = [(z `1 ), (z `2 )] by A5, MCART_1: 21;

          

           A9: (z `2 ) in Y by A5, MCART_1: 10;

          then

           A10: (f1 . ((z `1 ),(z `2 ))) = (g1 . (z `2 )) by A7;

          ex g2 be Function st (( curry f2) . (z `1 )) = g2 & ( dom g2) = Y & ( rng g2) c= ( rng f2) & for y st y in Y holds (g2 . y) = (f2 . ((z `1 ),y)) by A2, A5, Th22, MCART_1: 10;

          then (f2 . ((z `1 ),(z `2 ))) = (g1 . (z `2 )) by A3, A9, A6;

          hence (f1 . z) = (f2 . z) by A8, A10;

        end;

        hence thesis by A1, A2;

      end;

       [:X, Y:] = {} implies f1 = {} & f2 = {} by A1, A2;

      hence thesis by A4;

    end;

    theorem :: FUNCT_5:45

    

     Th38: ( dom f1) = [:X, Y:] & ( dom f2) = [:X, Y:] & ( curry' f1) = ( curry' f2) implies f1 = f2

    proof

      assume that

       A1: ( dom f1) = [:X, Y:] and

       A2: ( dom f2) = [:X, Y:] and

       A3: ( curry' f1) = ( curry' f2);

      ( dom ( ~ f1)) = [:Y, X:] & ( dom ( ~ f2)) = [:Y, X:] by A1, A2, FUNCT_4: 46;

      then

       A4: ( ~ f1) = ( ~ f2) by A3, Th37;

      ( ~ ( ~ f1)) = f1 by A1, FUNCT_4: 52;

      hence thesis by A2, A4, FUNCT_4: 52;

    end;

    theorem :: FUNCT_5:46

    

     Th39: ( rng f1) c= ( Funcs (X,Y)) & ( rng f2) c= ( Funcs (X,Y)) & X <> {} & ( uncurry f1) = ( uncurry f2) implies f1 = f2

    proof

      assume that

       A1: ( rng f1) c= ( Funcs (X,Y)) and

       A2: ( rng f2) c= ( Funcs (X,Y)) and

       A3: X <> {} and

       A4: ( uncurry f1) = ( uncurry f2);

      

       A5: ( dom ( uncurry f1)) = [:( dom f1), X:] & ( dom ( uncurry f2)) = [:( dom f2), X:] by A1, A2, Th19;

      then ( dom f1) = {} implies ( dom f1) = ( dom f2) by A3, A4;

      then

       A6: ( dom f1) = ( dom f2) by A3, A4, A5, ZFMISC_1: 110;

      now

        let x be object;

        assume

         A7: x in ( dom f1);

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

        then

        consider g1 such that

         A8: (f1 . x) = g1 and

         A9: ( dom g1) = X and ( rng g1) c= Y by A1, FUNCT_2:def 2;

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

        then

        consider g2 such that

         A10: (f2 . x) = g2 and

         A11: ( dom g2) = X and ( rng g2) c= Y by A2, FUNCT_2:def 2;

        now

          let y be object;

          

           A12: ( [x, y] `1 ) = x & ( [x, y] `2 ) = y;

          assume

           A13: y in X;

          then

           A14: [x, y] in ( dom ( uncurry f2)) by A4, A7, A8, A9, Def2;

           [x, y] in ( dom ( uncurry f1)) by A7, A8, A9, A13, Def2;

          then (( uncurry f1) . [x, y]) = (g1 . y) by A8, A12, Def2;

          hence (g1 . y) = (g2 . y) by A4, A10, A14, A12, Def2;

        end;

        hence (f1 . x) = (f2 . x) by A8, A9, A10, A11, FUNCT_1: 2;

      end;

      hence thesis by A6;

    end;

    theorem :: FUNCT_5:47

    ( rng f1) c= ( Funcs (X,Y)) & ( rng f2) c= ( Funcs (X,Y)) & X <> {} & ( uncurry' f1) = ( uncurry' f2) implies f1 = f2

    proof

      assume that

       A1: ( rng f1) c= ( Funcs (X,Y)) and

       A2: ( rng f2) c= ( Funcs (X,Y)) and

       A3: X <> {} & ( uncurry' f1) = ( uncurry' f2);

      ( dom ( uncurry f1)) = [:( dom f1), X:] by A1, Th19;

      then

       A4: ( uncurry f1) = ( ~ ( ~ ( uncurry f1))) by FUNCT_4: 52;

      ( dom ( uncurry f2)) = [:( dom f2), X:] by A2, Th19;

      hence thesis by A1, A2, A3, A4, Th39, FUNCT_4: 52;

    end;

    theorem :: FUNCT_5:48

    

     Th41: ( rng f) c= ( Funcs (X,Y)) & X <> {} implies ( curry ( uncurry f)) = f & ( curry' ( uncurry' f)) = f

    proof

      assume that

       A1: ( rng f) c= ( Funcs (X,Y)) and

       A2: X <> {} ;

      

       A3: ( dom ( uncurry f)) = [:( dom f), X:] by A1, Th19;

       A4:

      now

         A5:

        now

          let x be object;

          assume

           A6: x in ( dom f);

          then

          consider h such that

           A7: (( curry ( uncurry f)) . x) = h & ( dom h) = X & ( rng h) c= ( rng ( uncurry f)) and

           A8: y in X implies (h . y) = (( uncurry f) . (x,y)) by A2, A3, Th22;

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

          then

          consider g such that

           A9: (f . x) = g & ( dom g) = X and ( rng g) c= Y by A1, FUNCT_2:def 2;

          now

            let y be object;

            assume

             A10: y in X;

            then (( uncurry f) . (x,y)) = (g . y) by A6, A9, Th31;

            hence (g . y) = (h . y) by A8, A10;

          end;

          hence (f . x) = (( curry ( uncurry f)) . x) by A9, A7, FUNCT_1: 2;

        end;

        assume ( dom f) <> {} ;

        then ( dom ( curry ( uncurry f))) = ( dom f) by A2, A3, Th17;

        hence ( curry ( uncurry f)) = f by A5;

      end;

       A11:

      now

        assume ( dom f) = {} ;

        then ( dom ( uncurry f)) = {} & f = {} by A3;

        hence ( curry ( uncurry f)) = f by Th35, RELAT_1: 41;

      end;

      hence ( curry ( uncurry f)) = f by A4;

      thus thesis by A3, A11, A4, FUNCT_4: 52;

    end;

    theorem :: FUNCT_5:49

    ( dom f) = [:X, Y:] implies ( uncurry ( curry f)) = f & ( uncurry' ( curry' f)) = f

    proof

      assume

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

       A2:

      now

        

         A3: ( rng ( curry' f)) c= ( Funcs (X,( rng f))) by A1, Th28;

        assume

         A4: ( dom f) <> {} ;

        then X <> {} by A1;

        then

         A5: ( curry' ( uncurry' ( curry' f))) = ( curry' f) by A3, Th41;

        ( dom ( curry' f)) = Y by A1, A4, Th17;

        then

         A6: ( dom ( uncurry' ( curry' f))) = [:X, Y:] by A3, Th19;

        

         A7: ( rng ( curry f)) c= ( Funcs (Y,( rng f))) by A1, Th28;

        Y <> {} by A1, A4;

        then

         A8: ( curry ( uncurry ( curry f))) = ( curry f) by A7, Th41;

        ( dom ( curry f)) = X by A1, A4, Th17;

        then ( dom ( uncurry ( curry f))) = [:X, Y:] by A7, Th19;

        hence thesis by A1, A8, A5, A6, Th37, Th38;

      end;

      now

        assume ( dom f) = {} ;

        then f = {} ;

        hence thesis by Th35, Th36;

      end;

      hence thesis by A2;

    end;

    theorem :: FUNCT_5:50

    

     Th43: ( dom f) c= [:X, Y:] implies ( uncurry ( curry f)) = f & ( uncurry' ( curry' f)) = f

    proof

      assume

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

       A2:

      now

        let X, Y, f such that

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

        

         A4: ( dom ( uncurry ( curry f))) = ( dom f)

        proof

          thus ( dom ( uncurry ( curry f))) c= ( dom f)

          proof

            let x be object;

            assume x in ( dom ( uncurry ( curry f)));

            then ex y, g, z st x = [y, z] & y in ( dom ( curry f)) & g = (( curry f) . y) & z in ( dom g) by Def2;

            hence thesis by Th24;

          end;

          let x be object;

          assume

           A5: x in ( dom f);

          then

           A6: x = [(x `1 ), (x `2 )] by A3, MCART_1: 21;

          then (x `1 ) in ( dom ( curry f)) by A5, Th12;

          then

          reconsider g = (( curry f) . (x `1 )) as Function by FUNCOP_1:def 6;

          (x `2 ) in ( dom g) & (x `1 ) in ( dom ( curry f)) by A5, A6, Th12, Th13;

          hence thesis by A6, Th31;

        end;

        now

          let x be object;

          assume

           A7: x in ( dom f);

          then

           A8: x = [(x `1 ), (x `2 )] by A3, MCART_1: 21;

          then (x `1 ) in ( dom ( curry f)) by A7, Th12;

          then

          reconsider g = (( curry f) . (x `1 )) as Function by FUNCOP_1:def 6;

          (( uncurry ( curry f)) . x) = (g . (x `2 )) by A4, A7, Def2;

          then (f . ((x `1 ),(x `2 ))) = (( uncurry ( curry f)) . ((x `1 ),(x `2 ))) by A7, A8, Th13;

          hence (f . x) = (( uncurry ( curry f)) . x) by A8;

        end;

        hence ( uncurry ( curry f)) = f by A4;

      end;

      hence ( uncurry ( curry f)) = f by A1;

      ( dom ( ~ f)) c= [:Y, X:] by A1, FUNCT_4: 45;

      then ( uncurry ( curry ( ~ f))) = ( ~ f) by A2;

      hence thesis by A1, FUNCT_4: 52;

    end;

    theorem :: FUNCT_5:51

    

     Th44: ( rng f) c= ( PFuncs (X,Y)) & not {} in ( rng f) implies ( curry ( uncurry f)) = f & ( curry' ( uncurry' f)) = f

    proof

      assume that

       A1: ( rng f) c= ( PFuncs (X,Y)) and

       A2: not {} in ( rng f);

      

       A3: ( dom ( curry ( uncurry f))) = ( dom f)

      proof

        ( dom ( uncurry f)) c= [:( dom f), X:] by A1, Th30;

        hence ( dom ( curry ( uncurry f))) c= ( dom f) by Th18;

        let x be object;

        assume

         A4: x in ( dom f);

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

        then

        consider g such that

         A5: (f . x) = g and ( dom g) c= X and ( rng g) c= Y by A1, PARTFUN1:def 3;

        set y = the Element of ( dom g);

        g <> {} by A2, A4, A5, FUNCT_1:def 3;

        then

         A6: [x, y] in ( dom ( uncurry f)) by A4, A5, Th31;

        ( dom ( curry ( uncurry f))) = ( proj1 ( dom ( uncurry f))) by Def1;

        hence thesis by A6, XTUPLE_0:def 12;

      end;

      now

        let x be object;

        assume

         A7: x in ( dom f);

        then

        reconsider h = (( curry ( uncurry f)) . x) as Function by A3, Th23;

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

        then

        consider g such that

         A8: (f . x) = g and ( dom g) c= X and ( rng g) c= Y by A1, PARTFUN1:def 3;

        

         A9: ( dom h) = ( proj2 (( dom ( uncurry f)) /\ [: {x}, ( proj2 ( dom ( uncurry f))):])) by A3, A7, Th24;

        

         A10: ( dom h) = ( dom g)

        proof

          thus ( dom h) c= ( dom g)

          proof

            let z be object;

            assume z in ( dom h);

            then

            consider t be object such that

             A11: [t, z] in (( dom ( uncurry f)) /\ [: {x}, ( proj2 ( dom ( uncurry f))):]) by A9, XTUPLE_0:def 13;

             [t, z] in [: {x}, ( proj2 ( dom ( uncurry f))):] by A11, XBOOLE_0:def 4;

            then

             A12: t = x by ZFMISC_1: 105;

             [t, z] in ( dom ( uncurry f)) by A11, XBOOLE_0:def 4;

            then

            consider x1, g1, x2 such that

             A13: [t, z] = [x1, x2] and x1 in ( dom f) and

             A14: g1 = (f . x1) & x2 in ( dom g1) by Def2;

            t = x1 by A13, XTUPLE_0: 1;

            hence thesis by A8, A13, A14, A12, XTUPLE_0: 1;

          end;

          let y be object;

          assume y in ( dom g);

          then [x, y] in ( dom ( uncurry f)) by A7, A8, Th31;

          hence thesis by Th13;

        end;

        now

          let y be object;

          assume

           A15: y in ( dom h);

          

          hence (h . y) = (( uncurry f) . (x,y)) by A3, A7, Th24

          .= (g . y) by A7, A8, A10, A15, Th31;

        end;

        hence (f . x) = (( curry ( uncurry f)) . x) by A8, A10, FUNCT_1: 2;

      end;

      hence

       A16: ( curry ( uncurry f)) = f by A3;

      ( dom ( uncurry f)) c= [:( dom f), X:] by A1, Th30;

      hence thesis by A16, FUNCT_4: 52;

    end;

    theorem :: FUNCT_5:52

    ( dom f1) c= [:X, Y:] & ( dom f2) c= [:X, Y:] & ( curry f1) = ( curry f2) implies f1 = f2

    proof

      assume that

       A1: ( dom f1) c= [:X, Y:] and

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

      ( uncurry ( curry f1)) = f1 by A1, Th43;

      hence thesis by A2, Th43;

    end;

    theorem :: FUNCT_5:53

    ( dom f1) c= [:X, Y:] & ( dom f2) c= [:X, Y:] & ( curry' f1) = ( curry' f2) implies f1 = f2

    proof

      assume that

       A1: ( dom f1) c= [:X, Y:] and

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

      ( uncurry' ( curry' f1)) = f1 by A1, Th43;

      hence thesis by A2, Th43;

    end;

    theorem :: FUNCT_5:54

    ( rng f1) c= ( PFuncs (X,Y)) & ( rng f2) c= ( PFuncs (X,Y)) & not {} in ( rng f1) & not {} in ( rng f2) & ( uncurry f1) = ( uncurry f2) implies f1 = f2

    proof

      assume that

       A1: ( rng f1) c= ( PFuncs (X,Y)) and

       A2: ( rng f2) c= ( PFuncs (X,Y)) and

       A3: not {} in ( rng f1) and

       A4: not {} in ( rng f2);

      ( curry ( uncurry f1)) = f1 by A1, A3, Th44;

      hence thesis by A2, A4, Th44;

    end;

    theorem :: FUNCT_5:55

    ( rng f1) c= ( PFuncs (X,Y)) & ( rng f2) c= ( PFuncs (X,Y)) & not {} in ( rng f1) & not {} in ( rng f2) & ( uncurry' f1) = ( uncurry' f2) implies f1 = f2

    proof

      assume that

       A1: ( rng f1) c= ( PFuncs (X,Y)) and

       A2: ( rng f2) c= ( PFuncs (X,Y)) and

       A3: not {} in ( rng f1) and

       A4: not {} in ( rng f2);

      ( curry' ( uncurry' f1)) = f1 by A1, A3, Th44;

      hence thesis by A2, A4, Th44;

    end;

    theorem :: FUNCT_5:56

    

     Th49: X c= Y implies ( Funcs (Z,X)) c= ( Funcs (Z,Y))

    proof

      assume

       A1: X c= Y;

      let x be object;

      assume x in ( Funcs (Z,X));

      then

      consider f such that

       A2: x = f & ( dom f) = Z and

       A3: ( rng f) c= X by FUNCT_2:def 2;

      ( rng f) c= Y by A1, A3;

      hence thesis by A2, FUNCT_2:def 2;

    end;

    theorem :: FUNCT_5:57

    

     Th50: ( Funcs ( {} ,X)) = { {} }

    proof

      thus ( Funcs ( {} ,X)) c= { {} }

      proof

        let x be object;

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

        then ex f st x = f & ( dom f) = {} & ( rng f) c= X by FUNCT_2:def 2;

        then x = {} ;

        hence thesis by TARSKI:def 1;

      end;

      let x be object;

      

       A1: {} c= X;

      assume x in { {} };

      then

       A2: x = {} by TARSKI:def 1;

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

      hence thesis by A2, A1, FUNCT_2:def 2;

    end;

    theorem :: FUNCT_5:58

    for x be object holds (X,( Funcs ( {x},X))) are_equipotent & ( card X) = ( card ( Funcs ( {x},X)))

    proof

      let x be object;

      deffunc F( object) = ( {x} --> $1);

      consider f such that

       A1: ( dom f) = X & for y be object st y in X holds (f . y) = F(y) from FUNCT_1:sch 3;

      

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

      thus (X,( Funcs ( {x},X))) are_equipotent

      proof

        take f;

        thus f is one-to-one

        proof

          let y,z be object;

          assume y in ( dom f) & z in ( dom f);

          then

           A3: (f . y) = ( {x} --> y) & (f . z) = ( {x} --> z) by A1;

          (( {x} --> y) . x) = y by A2, FUNCOP_1: 7;

          hence thesis by A2, A3, FUNCOP_1: 7;

        end;

        thus ( dom f) = X by A1;

        thus ( rng f) c= ( Funcs ( {x},X))

        proof

          let y be object;

          assume y in ( rng f);

          then

          consider z be object such that

           A4: z in ( dom f) & y = (f . z) by FUNCT_1:def 3;

          

           A5: ( dom ( {x} --> z)) = {x} & ( rng ( {x} --> z)) = {z} by FUNCOP_1: 8, FUNCOP_1: 13;

          y = ( {x} --> z) & {z} c= X by A1, A4, ZFMISC_1: 31;

          hence thesis by A5, FUNCT_2:def 2;

        end;

        let y be object;

        assume y in ( Funcs ( {x},X));

        then

        consider g such that

         A6: y = g and

         A7: ( dom g) = {x} and

         A8: ( rng g) c= X by FUNCT_2:def 2;

        

         A9: (g . x) in {(g . x)} by TARSKI:def 1;

        

         A10: ( rng g) = {(g . x)} by A7, FUNCT_1: 4;

        then g = ( {x} --> (g . x)) by A7, FUNCOP_1: 9;

        then (f . (g . x)) = g by A1, A8, A10, A9;

        hence thesis by A1, A6, A8, A10, A9, FUNCT_1:def 3;

      end;

      hence thesis by CARD_1: 5;

    end;

    theorem :: FUNCT_5:59

    

     Th52: ( Funcs (X, {x})) = {(X --> x)}

    proof

      thus ( Funcs (X, {x})) c= {(X --> x)}

      proof

        let y be object;

        assume y in ( Funcs (X, {x}));

        then

        consider f such that

         A1: y = f and

         A2: ( dom f) = X and

         A3: ( rng f) c= {x} by FUNCT_2:def 2;

         A4:

        now

          set z = the Element of X;

          

           A5: X <> {} implies z in X;

          assume for z holds not z in X;

          hence f = (X --> x) by A2, A5;

        end;

        now

          given z such that

           A6: z in X;

          (f . z) in ( rng f) by A2, A6, FUNCT_1:def 3;

          then (f . z) = x & {(f . z)} c= ( rng f) by A3, TARSKI:def 1;

          then ( rng f) = {x} by A3;

          hence f = (X --> x) by A2, FUNCOP_1: 9;

        end;

        hence thesis by A1, A4, TARSKI:def 1;

      end;

      let y be object;

      assume y in {(X --> x)};

      then

       A7: y = (X --> x) by TARSKI:def 1;

      ( dom (X --> x)) = X & ( rng (X --> x)) c= {x} by FUNCOP_1: 13;

      hence thesis by A7, FUNCT_2:def 2;

    end;

    theorem :: FUNCT_5:60

    

     Th53: (X1,Y1) are_equipotent & (X2,Y2) are_equipotent implies (( Funcs (X1,X2)),( Funcs (Y1,Y2))) are_equipotent & ( card ( Funcs (X1,X2))) = ( card ( Funcs (Y1,Y2)))

    proof

      assume that

       A1: (X1,Y1) are_equipotent and

       A2: (X2,Y2) are_equipotent ;

      consider f1 such that

       A3: f1 is one-to-one and

       A4: ( dom f1) = Y1 and

       A5: ( rng f1) = X1 by A1, WELLORD2:def 4;

      consider f2 such that

       A6: f2 is one-to-one and

       A7: ( dom f2) = X2 and

       A8: ( rng f2) = Y2 by A2;

      (( Funcs (X1,X2)),( Funcs (Y1,Y2))) are_equipotent

      proof

        

         A9: ( rng (f1 " )) = Y1 by A3, A4, FUNCT_1: 33;

        deffunc F( Function) = (f2 * ($1 * f1));

        consider F be Function such that

         A10: ( dom F) = ( Funcs (X1,X2)) & for g st g in ( Funcs (X1,X2)) holds (F . g) = F(g) from LambdaFS;

        take F;

        thus F is one-to-one

        proof

          let x,y be object;

          assume that

           A11: x in ( dom F) and

           A12: y in ( dom F) and

           A13: (F . x) = (F . y);

          consider g1 be Function such that

           A14: x = g1 and

           A15: ( dom g1) = X1 and

           A16: ( rng g1) c= X2 by A10, A11, FUNCT_2:def 2;

          

           A17: (F . x) = (f2 * (g1 * f1)) by A10, A11, A14;

          

           A18: ( rng (g1 * f1)) c= X2 & ( dom (g1 * f1)) = Y1 by A4, A5, A15, A16, RELAT_1: 27, RELAT_1: 28;

          consider g2 be Function such that

           A19: y = g2 and

           A20: ( dom g2) = X1 and

           A21: ( rng g2) c= X2 by A10, A12, FUNCT_2:def 2;

          

           A22: ( rng (g2 * f1)) c= X2 & ( dom (g2 * f1)) = Y1 by A4, A5, A20, A21, RELAT_1: 27, RELAT_1: 28;

          (F . x) = (f2 * (g2 * f1)) by A10, A12, A13, A19;

          then

           A23: (g1 * f1) = (g2 * f1) by A6, A7, A17, A18, A22, FUNCT_1: 27;

          now

            let z be object;

            assume z in X1;

            then

            consider z9 be object such that

             A24: z9 in Y1 & (f1 . z9) = z by A4, A5, FUNCT_1:def 3;

            

            thus (g1 . z) = ((g1 * f1) . z9) by A4, A24, FUNCT_1: 13

            .= (g2 . z) by A4, A23, A24, FUNCT_1: 13;

          end;

          hence thesis by A14, A15, A19, A20, FUNCT_1: 2;

        end;

        thus ( dom F) = ( Funcs (X1,X2)) by A10;

        thus ( rng F) c= ( Funcs (Y1,Y2))

        proof

          let x be object;

          assume x in ( rng F);

          then

          consider y be object such that

           A25: y in ( dom F) and

           A26: x = (F . y) by FUNCT_1:def 3;

          consider g such that

           A27: y = g and

           A28: ( dom g) = X1 & ( rng g) c= X2 by A10, A25, FUNCT_2:def 2;

          ( dom (g * f1)) = Y1 & ( rng (g * f1)) c= X2 by A4, A5, A28, RELAT_1: 27, RELAT_1: 28;

          then

           A29: ( dom (f2 * (g * f1))) = Y1 by A7, RELAT_1: 27;

          

           A30: ( rng (f2 * (g * f1))) c= Y2 by A8, RELAT_1: 26;

          x = (f2 * (g * f1)) by A10, A25, A26, A27;

          hence thesis by A29, A30, FUNCT_2:def 2;

        end;

        let x be object;

        assume x in ( Funcs (Y1,Y2));

        then

        consider g such that

         A31: x = g and

         A32: ( dom g) = Y1 and

         A33: ( rng g) c= Y2 by FUNCT_2:def 2;

        

         A34: (f2 * ((((f2 " ) * g) * (f1 " )) * f1)) = (f2 * (((f2 " ) * g) * ((f1 " ) * f1))) by RELAT_1: 36

        .= ((f2 * ((f2 " ) * g)) * ((f1 " ) * f1)) by RELAT_1: 36

        .= (((f2 * (f2 " )) * g) * ((f1 " ) * f1)) by RELAT_1: 36

        .= ((( id Y2) * g) * ((f1 " ) * f1)) by A6, A8, FUNCT_1: 39

        .= ((( id Y2) * g) * ( id Y1)) by A3, A4, FUNCT_1: 39

        .= (g * ( id Y1)) by A33, RELAT_1: 53

        .= x by A31, A32, RELAT_1: 52;

        ( dom (f2 " )) = Y2 by A6, A8, FUNCT_1: 33;

        then

         A35: ( dom ((f2 " ) * g)) = Y1 by A32, A33, RELAT_1: 27;

        ( rng (f2 " )) = X2 by A6, A7, FUNCT_1: 33;

        then ( rng ((f2 " ) * g)) c= X2 by RELAT_1: 26;

        then

         A36: ( rng (((f2 " ) * g) * (f1 " ))) c= X2 by A9, A35, RELAT_1: 28;

        ( dom (f1 " )) = X1 by A3, A5, FUNCT_1: 33;

        then ( dom (((f2 " ) * g) * (f1 " ))) = X1 by A9, A35, RELAT_1: 27;

        then

         A37: (((f2 " ) * g) * (f1 " )) in ( dom F) by A10, A36, FUNCT_2:def 2;

        then (F . (((f2 " ) * g) * (f1 " ))) = (f2 * ((((f2 " ) * g) * (f1 " )) * f1)) by A10;

        hence thesis by A37, A34, FUNCT_1:def 3;

      end;

      hence thesis by CARD_1: 5;

    end;

    theorem :: FUNCT_5:61

    ( card X1) = ( card Y1) & ( card X2) = ( card Y2) implies ( card ( Funcs (X1,X2))) = ( card ( Funcs (Y1,Y2)))

    proof

      assume ( card X1) = ( card Y1) & ( card X2) = ( card Y2);

      then (X1,Y1) are_equipotent & (X2,Y2) are_equipotent by CARD_1: 5;

      hence thesis by Th53;

    end;

    theorem :: FUNCT_5:62

    X1 misses X2 implies (( Funcs ((X1 \/ X2),X)), [:( Funcs (X1,X)), ( Funcs (X2,X)):]) are_equipotent & ( card ( Funcs ((X1 \/ X2),X))) = ( card [:( Funcs (X1,X)), ( Funcs (X2,X)):])

    proof

      deffunc F( Function) = [($1 | X1), ($1 | X2)];

      consider f such that

       A1: ( dom f) = ( Funcs ((X1 \/ X2),X)) & for g st g in ( Funcs ((X1 \/ X2),X)) holds (f . g) = F(g) from LambdaFS;

      assume

       A2: X1 misses X2;

      thus (( Funcs ((X1 \/ X2),X)), [:( Funcs (X1,X)), ( Funcs (X2,X)):]) are_equipotent

      proof

        take f;

        thus f is one-to-one

        proof

          let x,y be object;

          assume that

           A3: x in ( dom f) and

           A4: y in ( dom f);

          consider g2 be Function such that

           A5: y = g2 and

           A6: ( dom g2) = (X1 \/ X2) and ( rng g2) c= X by A1, A4, FUNCT_2:def 2;

          

           A7: (f . y) = [(g2 | X1), (g2 | X2)] by A1, A4, A5;

          assume

           A8: (f . x) = (f . y);

          consider g1 be Function such that

           A9: x = g1 and

           A10: ( dom g1) = (X1 \/ X2) and ( rng g1) c= X by A1, A3, FUNCT_2:def 2;

          

           A11: (f . x) = [(g1 | X1), (g1 | X2)] by A1, A3, A9;

          now

            let x be object;

            assume x in (X1 \/ X2);

            then x in X1 or x in X2 by XBOOLE_0:def 3;

            then (g1 . x) = ((g1 | X1) . x) & (g2 . x) = ((g2 | X1) . x) or (g1 . x) = ((g1 | X2) . x) & (g2 . x) = ((g2 | X2) . x) by FUNCT_1: 49;

            hence (g1 . x) = (g2 . x) by A11, A7, A8, XTUPLE_0: 1;

          end;

          hence thesis by A9, A10, A5, A6, FUNCT_1: 2;

        end;

        thus ( dom f) = ( Funcs ((X1 \/ X2),X)) by A1;

        thus ( rng f) c= [:( Funcs (X1,X)), ( Funcs (X2,X)):]

        proof

          let x be object;

          assume x in ( rng f);

          then

          consider y be object such that

           A12: y in ( dom f) and

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

          consider g such that

           A14: y = g and

           A15: ( dom g) = (X1 \/ X2) and

           A16: ( rng g) c= X by A1, A12, FUNCT_2:def 2;

          ( rng (g | X2)) c= ( rng g) by RELAT_1: 70;

          then

           A17: ( rng (g | X2)) c= X by A16;

          ( rng (g | X1)) c= ( rng g) by RELAT_1: 70;

          then

           A18: ( rng (g | X1)) c= X by A16;

          ( dom (g | X2)) = X2 by A15, RELAT_1: 62, XBOOLE_1: 7;

          then

           A19: (g | X2) in ( Funcs (X2,X)) by A17, FUNCT_2:def 2;

          ( dom (g | X1)) = X1 by A15, RELAT_1: 62, XBOOLE_1: 7;

          then (g | X1) in ( Funcs (X1,X)) by A18, FUNCT_2:def 2;

          then [(g | X1), (g | X2)] in [:( Funcs (X1,X)), ( Funcs (X2,X)):] by A19, ZFMISC_1: 87;

          hence thesis by A1, A12, A13, A14;

        end;

        let x be object;

        assume

         A20: x in [:( Funcs (X1,X)), ( Funcs (X2,X)):];

        then

         A21: x = [(x `1 ), (x `2 )] by MCART_1: 21;

        (x `1 ) in ( Funcs (X1,X)) by A20, MCART_1: 10;

        then

        consider g1 be Function such that

         A22: (x `1 ) = g1 and

         A23: ( dom g1) = X1 and

         A24: ( rng g1) c= X by FUNCT_2:def 2;

        (x `2 ) in ( Funcs (X2,X)) by A20, MCART_1: 10;

        then

        consider g2 be Function such that

         A25: (x `2 ) = g2 and

         A26: ( dom g2) = X2 and

         A27: ( rng g2) c= X by FUNCT_2:def 2;

        ( rng (g1 +* g2)) c= (( rng g1) \/ ( rng g2)) & (( rng g1) \/ ( rng g2)) c= (X \/ X) by A24, A27, FUNCT_4: 17, XBOOLE_1: 13;

        then

         A28: ( rng (g1 +* g2)) c= X;

        ( dom (g1 +* g2)) = (X1 \/ X2) by A23, A26, FUNCT_4:def 1;

        then

         A29: (g1 +* g2) in ( dom f) by A1, A28, FUNCT_2:def 2;

        

        then (f . (g1 +* g2)) = [((g1 +* g2) | X1), ((g1 +* g2) | X2)] by A1

        .= [((g1 +* g2) | X1), g2] by A26, FUNCT_4: 23

        .= x by A2, A21, A22, A23, A25, A26, FUNCT_4: 33;

        hence thesis by A29, FUNCT_1:def 3;

      end;

      hence thesis by CARD_1: 5;

    end;

    theorem :: FUNCT_5:63

    (( Funcs ( [:X, Y:],Z)),( Funcs (X,( Funcs (Y,Z))))) are_equipotent & ( card ( Funcs ( [:X, Y:],Z))) = ( card ( Funcs (X,( Funcs (Y,Z)))))

    proof

      deffunc F( Function) = ( curry $1);

      consider f such that

       A1: ( dom f) = ( Funcs ( [:X, Y:],Z)) & for g st g in ( Funcs ( [:X, Y:],Z)) holds (f . g) = F(g) from LambdaFS;

       A2:

      now

        assume

         A3: [:X, Y:] <> {} ;

        thus (( Funcs ( [:X, Y:],Z)),( Funcs (X,( Funcs (Y,Z))))) are_equipotent

        proof

          take f;

          thus f is one-to-one

          proof

            let x1,x2 be object;

            assume that

             A4: x1 in ( dom f) and

             A5: x2 in ( dom f) and

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

            consider g2 such that

             A7: x2 = g2 and

             A8: ( dom g2) = [:X, Y:] and ( rng g2) c= Z by A1, A5, FUNCT_2:def 2;

            

             A9: (f . x2) = ( curry g2) by A1, A5, A7;

            consider g1 such that

             A10: x1 = g1 and

             A11: ( dom g1) = [:X, Y:] and ( rng g1) c= Z by A1, A4, FUNCT_2:def 2;

            (f . x1) = ( curry g1) by A1, A4, A10;

            hence thesis by A6, A10, A11, A7, A8, A9, Th37;

          end;

          thus ( dom f) = ( Funcs ( [:X, Y:],Z)) by A1;

          thus ( rng f) c= ( Funcs (X,( Funcs (Y,Z))))

          proof

            let y be object;

            assume y in ( rng f);

            then

            consider x be object such that

             A12: x in ( dom f) and

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

            consider g such that

             A14: x = g and

             A15: ( dom g) = [:X, Y:] and

             A16: ( rng g) c= Z by A1, A12, FUNCT_2:def 2;

            

             A17: ( dom ( curry g)) = X by A3, A15, Th17;

            ( rng ( curry g)) c= ( Funcs (Y,( rng g))) & ( Funcs (Y,( rng g))) c= ( Funcs (Y,Z)) by A15, A16, Th28, Th49;

            then

             A18: ( rng ( curry g)) c= ( Funcs (Y,Z));

            y = ( curry g) by A1, A12, A13, A14;

            hence thesis by A17, A18, FUNCT_2:def 2;

          end;

          let y be object;

          assume y in ( Funcs (X,( Funcs (Y,Z))));

          then

          consider g such that

           A19: y = g and

           A20: ( dom g) = X and

           A21: ( rng g) c= ( Funcs (Y,Z)) by FUNCT_2:def 2;

          ( dom ( uncurry g)) = [:X, Y:] & ( rng ( uncurry g)) c= Z by A20, A21, Th19, Th34;

          then

           A22: ( uncurry g) in ( Funcs ( [:X, Y:],Z)) by FUNCT_2:def 2;

          Y <> {} by A3, ZFMISC_1: 90;

          then ( curry ( uncurry g)) = g by A21, Th41;

          then (f . ( uncurry g)) = y by A1, A19, A22;

          hence thesis by A1, A22, FUNCT_1:def 3;

        end;

        hence ( card ( Funcs ( [:X, Y:],Z))) = ( card ( Funcs (X,( Funcs (Y,Z))))) by CARD_1: 5;

      end;

      now

        assume

         A23: [:X, Y:] = {} ;

        then

         A24: ( Funcs ( [:X, Y:],Z)) = { {} } by Th50;

         A25:

        now

          assume Y = {} ;

          then ( Funcs (Y,Z)) = { {} } by Th50;

          then ( Funcs (X,( Funcs (Y,Z)))) = {(X --> {} )} by Th52;

          hence (( Funcs ( [:X, Y:],Z)),( Funcs (X,( Funcs (Y,Z))))) are_equipotent by A24, CARD_1: 28;

        end;

        X = {} or Y = {} by A23;

        hence (( Funcs ( [:X, Y:],Z)),( Funcs (X,( Funcs (Y,Z))))) are_equipotent by A24, A25, Th50;

        X = {} implies ( Funcs (X,( Funcs (Y,Z)))) = { {} } by Th50;

        hence ( card ( Funcs ( [:X, Y:],Z))) = ( card ( Funcs (X,( Funcs (Y,Z))))) by A23, A25, Th50, CARD_1: 5;

      end;

      hence thesis by A2;

    end;

    theorem :: FUNCT_5:64

    (( Funcs (Z, [:X, Y:])), [:( Funcs (Z,X)), ( Funcs (Z,Y)):]) are_equipotent & ( card ( Funcs (Z, [:X, Y:]))) = ( card [:( Funcs (Z,X)), ( Funcs (Z,Y)):])

    proof

      deffunc F( Function) = [(( pr1 (X,Y)) * $1), (( pr2 (X,Y)) * $1)];

      consider f such that

       A1: ( dom f) = ( Funcs (Z, [:X, Y:])) & for g st g in ( Funcs (Z, [:X, Y:])) holds (f . g) = F(g) from LambdaFS;

      thus (( Funcs (Z, [:X, Y:])), [:( Funcs (Z,X)), ( Funcs (Z,Y)):]) are_equipotent

      proof

        take f;

        thus f is one-to-one

        proof

          let x1,x2 be object;

          assume that

           A2: x1 in ( dom f) and

           A3: x2 in ( dom f) and

           A4: (f . x1) = (f . x2);

          consider g1 such that

           A5: x1 = g1 and

           A6: ( dom g1) = Z and

           A7: ( rng g1) c= [:X, Y:] by A1, A2, FUNCT_2:def 2;

          consider g2 such that

           A8: x2 = g2 and

           A9: ( dom g2) = Z and

           A10: ( rng g2) c= [:X, Y:] by A1, A3, FUNCT_2:def 2;

           [(( pr1 (X,Y)) * g1), (( pr2 (X,Y)) * g1)] = (f . x1) by A1, A2, A5

          .= [(( pr1 (X,Y)) * g2), (( pr2 (X,Y)) * g2)] by A1, A3, A4, A8;

          then

           A11: (( pr1 (X,Y)) * g1) = (( pr1 (X,Y)) * g2) & (( pr2 (X,Y)) * g1) = (( pr2 (X,Y)) * g2) by XTUPLE_0: 1;

          now

            let x be object;

            assume

             A12: x in Z;

            then

             A13: ((( pr2 (X,Y)) * g1) . x) = (( pr2 (X,Y)) . (g1 . x)) by A6, FUNCT_1: 13;

            

             A14: (g2 . x) in ( rng g2) by A9, A12, FUNCT_1:def 3;

            then

             A15: (g2 . x) = [((g2 . x) `1 ), ((g2 . x) `2 )] by A10, MCART_1: 21;

            

             A16: (g1 . x) in ( rng g1) by A6, A12, FUNCT_1:def 3;

            then

             A17: (g1 . x) = [((g1 . x) `1 ), ((g1 . x) `2 )] by A7, MCART_1: 21;

            ((g2 . x) `1 ) in X & ((g2 . x) `2 ) in Y by A10, A14, MCART_1: 10;

            then

             A18: (( pr1 (X,Y)) . (((g2 . x) `1 ),((g2 . x) `2 ))) = ((g2 . x) `1 ) & (( pr2 (X,Y)) . (((g2 . x) `1 ),((g2 . x) `2 ))) = ((g2 . x) `2 ) by FUNCT_3:def 4, FUNCT_3:def 5;

            ((g1 . x) `1 ) in X & ((g1 . x) `2 ) in Y by A7, A16, MCART_1: 10;

            then

             A19: (( pr1 (X,Y)) . (((g1 . x) `1 ),((g1 . x) `2 ))) = ((g1 . x) `1 ) & (( pr2 (X,Y)) . (((g1 . x) `1 ),((g1 . x) `2 ))) = ((g1 . x) `2 ) by FUNCT_3:def 4, FUNCT_3:def 5;

            ((( pr1 (X,Y)) * g1) . x) = (( pr1 (X,Y)) . (g1 . x)) & ((( pr1 (X,Y)) * g2) . x) = (( pr1 (X,Y)) . (g2 . x)) by A6, A9, A12, FUNCT_1: 13;

            hence (g1 . x) = (g2 . x) by A9, A11, A12, A13, A17, A15, A19, A18, FUNCT_1: 13;

          end;

          hence thesis by A5, A6, A8, A9, FUNCT_1: 2;

        end;

        thus ( dom f) = ( Funcs (Z, [:X, Y:])) by A1;

        thus ( rng f) c= [:( Funcs (Z,X)), ( Funcs (Z,Y)):]

        proof

          let x be object;

          assume x in ( rng f);

          then

          consider y be object such that

           A20: y in ( dom f) and

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

          consider g such that

           A22: y = g and

           A23: ( dom g) = Z & ( rng g) c= [:X, Y:] by A1, A20, FUNCT_2:def 2;

          

           A24: ( rng (( pr1 (X,Y)) * g)) c= X;

          

           A25: ( rng (( pr2 (X,Y)) * g)) c= Y;

          ( dom ( pr2 (X,Y))) = [:X, Y:] by FUNCT_3:def 5;

          then ( dom (( pr2 (X,Y)) * g)) = Z by A23, RELAT_1: 27;

          then

           A26: (( pr2 (X,Y)) * g) in ( Funcs (Z,Y)) by A25, FUNCT_2:def 2;

          ( dom ( pr1 (X,Y))) = [:X, Y:] by FUNCT_3:def 4;

          then ( dom (( pr1 (X,Y)) * g)) = Z by A23, RELAT_1: 27;

          then

           A27: (( pr1 (X,Y)) * g) in ( Funcs (Z,X)) by A24, FUNCT_2:def 2;

          x = [(( pr1 (X,Y)) * g), (( pr2 (X,Y)) * g)] by A1, A20, A21, A22;

          hence thesis by A27, A26, ZFMISC_1: 87;

        end;

        let x be object;

        assume

         A28: x in [:( Funcs (Z,X)), ( Funcs (Z,Y)):];

        then

         A29: x = [(x `1 ), (x `2 )] by MCART_1: 21;

        (x `2 ) in ( Funcs (Z,Y)) by A28, MCART_1: 10;

        then

        consider g2 such that

         A30: (x `2 ) = g2 and

         A31: ( dom g2) = Z and

         A32: ( rng g2) c= Y by FUNCT_2:def 2;

        (x `1 ) in ( Funcs (Z,X)) by A28, MCART_1: 10;

        then

        consider g1 such that

         A33: (x `1 ) = g1 and

         A34: ( dom g1) = Z and

         A35: ( rng g1) c= X by FUNCT_2:def 2;

        ( rng <:g1, g2:>) c= [:( rng g1), ( rng g2):] & [:( rng g1), ( rng g2):] c= [:X, Y:] by A35, A32, FUNCT_3: 51, ZFMISC_1: 96;

        then

         A36: ( rng <:g1, g2:>) c= [:X, Y:];

        ( dom <:g1, g2:>) = (Z /\ Z) by A34, A31, FUNCT_3:def 7;

        then

         A37: <:g1, g2:> in ( Funcs (Z, [:X, Y:])) by A36, FUNCT_2:def 2;

        (( pr1 (X,Y)) * <:g1, g2:>) = g1 & (( pr2 (X,Y)) * <:g1, g2:>) = g2 by A34, A35, A31, A32, FUNCT_3: 52;

        then (f . <:g1, g2:>) = [g1, g2] by A1, A37;

        hence thesis by A1, A29, A33, A30, A37, FUNCT_1:def 3;

      end;

      hence thesis by CARD_1: 5;

    end;

    theorem :: FUNCT_5:65

    x <> y implies (( Funcs (X, {x, y})),( bool X)) are_equipotent & ( card ( Funcs (X, {x, y}))) = ( card ( bool X))

    proof

      deffunc F( Function) = ($1 " {x});

      consider f such that

       A1: ( dom f) = ( Funcs (X, {x, y})) & for g st g in ( Funcs (X, {x, y})) holds (f . g) = F(g) from LambdaFS;

      assume

       A2: x <> y;

      thus (( Funcs (X, {x, y})),( bool X)) are_equipotent

      proof

        deffunc F( object) = x;

        take f;

        thus f is one-to-one

        proof

          let x1,x2 be object;

          assume that

           A3: x1 in ( dom f) and

           A4: x2 in ( dom f) and

           A5: (f . x1) = (f . x2);

          consider g2 be Function such that

           A6: x2 = g2 and

           A7: ( dom g2) = X and

           A8: ( rng g2) c= {x, y} by A1, A4, FUNCT_2:def 2;

          

           A9: (f . x2) = (g2 " {x}) by A1, A4, A6;

          consider g1 be Function such that

           A10: x1 = g1 and

           A11: ( dom g1) = X and

           A12: ( rng g1) c= {x, y} by A1, A3, FUNCT_2:def 2;

          

           A13: (f . x1) = (g1 " {x}) by A1, A3, A10;

          now

            let z be object such that

             A14: z in X;

             A15:

            now

              assume

               A16: not (g1 . z) in {x};

              then

               A17: (g1 . z) <> x by TARSKI:def 1;

               not z in (g2 " {x}) by A5, A13, A9, A16, FUNCT_1:def 7;

              then not (g2 . z) in {x} by A7, A14, FUNCT_1:def 7;

              then

               A18: (g2 . z) <> x by TARSKI:def 1;

              (g1 . z) in ( rng g1) by A11, A14, FUNCT_1:def 3;

              then

               A19: (g1 . z) = y by A12, A17, TARSKI:def 2;

              (g2 . z) in ( rng g2) by A7, A14, FUNCT_1:def 3;

              hence (g1 . z) = (g2 . z) by A8, A18, A19, TARSKI:def 2;

            end;

            now

              assume

               A20: (g1 . z) in {x};

              then z in (g2 " {x}) by A5, A11, A13, A9, A14, FUNCT_1:def 7;

              then (g2 . z) in {x} by FUNCT_1:def 7;

              then (g2 . z) = x by TARSKI:def 1;

              hence (g1 . z) = (g2 . z) by A20, TARSKI:def 1;

            end;

            hence (g1 . z) = (g2 . z) by A15;

          end;

          hence thesis by A10, A11, A6, A7, FUNCT_1: 2;

        end;

        thus ( dom f) = ( Funcs (X, {x, y})) by A1;

        thus ( rng f) c= ( bool X)

        proof

          let z be object;

          assume z in ( rng f);

          then

          consider t be object such that

           A21: t in ( dom f) and

           A22: z = (f . t) by FUNCT_1:def 3;

          consider g such that

           A23: t = g and

           A24: ( dom g) = X and ( rng g) c= {x, y} by A1, A21, FUNCT_2:def 2;

          

           A25: (g " {x}) c= X by A24, RELAT_1: 132;

          z = (g " {x}) by A1, A21, A22, A23;

          hence thesis by A25;

        end;

        deffunc G( object) = y;

        let z be object;

        reconsider zz = z as set by TARSKI: 1;

        defpred P[ object] means $1 in zz;

        consider g such that

         A26: ( dom g) = X & for t be object st t in X holds ( P[t] implies (g . t) = F(t)) & ( not P[t] implies (g . t) = G(t)) from PARTFUN1:sch 1;

        assume

         A27: z in ( bool X);

        

         A28: (g " {x}) = zz

        proof

          thus (g " {x}) c= zz

          proof

            let t be object;

            assume

             A29: t in (g " {x});

            then (g . t) in {x} by FUNCT_1:def 7;

            then

             A30: (g . t) = x by TARSKI:def 1;

            t in ( dom g) by A29, FUNCT_1:def 7;

            hence thesis by A2, A26, A30;

          end;

          let t be object;

          assume

           A31: t in zz;

          then (g . t) = x by A27, A26;

          then (g . t) in {x} by TARSKI:def 1;

          hence thesis by A27, A26, A31, FUNCT_1:def 7;

        end;

        ( rng g) c= {x, y}

        proof

          let t be object;

          assume t in ( rng g);

          then ex v be object st v in ( dom g) & t = (g . v) by FUNCT_1:def 3;

          then t = x or t = y by A26;

          hence thesis by TARSKI:def 2;

        end;

        then

         A32: g in ( Funcs (X, {x, y})) by A26, FUNCT_2:def 2;

        then (f . g) = (g " {x}) by A1;

        hence thesis by A1, A32, A28, FUNCT_1:def 3;

      end;

      hence thesis by CARD_1: 5;

    end;

    theorem :: FUNCT_5:66

    x <> y implies (( Funcs ( {x, y},X)), [:X, X:]) are_equipotent & ( card ( Funcs ( {x, y},X))) = ( card [:X, X:])

    proof

      deffunc F( Function) = [($1 . x), ($1 . y)];

      consider f such that

       A1: ( dom f) = ( Funcs ( {x, y},X)) & for g st g in ( Funcs ( {x, y},X)) holds (f . g) = F(g) from LambdaFS;

      assume

       A2: x <> y;

      thus (( Funcs ( {x, y},X)), [:X, X:]) are_equipotent

      proof

        defpred P[ object] means $1 = x;

        take f;

        thus f is one-to-one

        proof

          let x1,x2 be object;

          assume that

           A3: x1 in ( dom f) and

           A4: x2 in ( dom f) and

           A5: (f . x1) = (f . x2);

          consider g2 such that

           A6: x2 = g2 and

           A7: ( dom g2) = {x, y} and ( rng g2) c= X by A1, A4, FUNCT_2:def 2;

          consider g1 such that

           A8: x1 = g1 and

           A9: ( dom g1) = {x, y} and ( rng g1) c= X by A1, A3, FUNCT_2:def 2;

          

           A10: [(g1 . x), (g1 . y)] = (f . x1) by A1, A3, A8

          .= [(g2 . x), (g2 . y)] by A1, A4, A5, A6;

          now

            let z be object;

            assume z in {x, y};

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

            hence (g1 . z) = (g2 . z) by A10, XTUPLE_0: 1;

          end;

          hence thesis by A8, A9, A6, A7, FUNCT_1: 2;

        end;

        thus ( dom f) = ( Funcs ( {x, y},X)) by A1;

        thus ( rng f) c= [:X, X:]

        proof

          let z be object;

          assume z in ( rng f);

          then

          consider t be object such that

           A11: t in ( dom f) and

           A12: z = (f . t) by FUNCT_1:def 3;

          consider g such that

           A13: t = g and

           A14: ( dom g) = {x, y} and

           A15: ( rng g) c= X by A1, A11, FUNCT_2:def 2;

          x in {x, y} by TARSKI:def 2;

          then

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

          y in {x, y} by TARSKI:def 2;

          then

           A17: (g . y) in ( rng g) by A14, FUNCT_1:def 3;

          z = [(g . x), (g . y)] by A1, A11, A12, A13;

          hence thesis by A15, A16, A17, ZFMISC_1: 87;

        end;

        let z be object;

        deffunc F( object) = (z `1 );

        deffunc G( object) = (z `2 );

        consider g such that

         A18: ( dom g) = {x, y} & for t be object st t in {x, y} holds ( P[t] implies (g . t) = F(t)) & ( not P[t] implies (g . t) = G(t)) from PARTFUN1:sch 1;

        x in {x, y} by TARSKI:def 2;

        then

         A19: (g . x) = (z `1 ) by A18;

        y in {x, y} by TARSKI:def 2;

        then

         A20: (g . y) = (z `2 ) by A2, A18;

        assume

         A21: z in [:X, X:];

        then

         A22: z = [(z `1 ), (z `2 )] by MCART_1: 21;

        

         A23: (z `1 ) in X & (z `2 ) in X by A21, MCART_1: 10;

        ( rng g) c= X

        proof

          let t be object;

          assume t in ( rng g);

          then ex a be object st a in ( dom g) & t = (g . a) by FUNCT_1:def 3;

          hence thesis by A23, A18;

        end;

        then

         A24: g in ( Funcs ( {x, y},X)) by A18, FUNCT_2:def 2;

        then (f . g) = [(g . x), (g . y)] by A1;

        hence thesis by A1, A22, A24, A19, A20, FUNCT_1:def 3;

      end;

      hence thesis by CARD_1: 5;

    end;

    begin

    notation

      synonym op0 for 0 ;

    end

    definition

      :: original: op0

      redefine

      func op0 -> Element of { 0 } ;

      coherence by TARSKI:def 1;

    end

    definition

      :: FUNCT_5:def5

      func op1 -> set equals ( 0 .--> 0 );

      coherence ;

      :: FUNCT_5:def6

      func op2 -> set equals (( 0 , 0 ) :-> 0 );

      coherence ;

    end

    definition

      :: original: op1

      redefine

      func op1 -> UnOp of { 0 } ;

      coherence ;

      :: original: op2

      redefine

      func op2 -> BinOp of { 0 } ;

      coherence ;

    end

    reserve C,D,E for non empty set;

    reserve c for Element of C,

d for Element of D;

    definition

      let D, X, E;

      let F be FUNCTION_DOMAIN of X, E;

      let f be Function of D, F;

      let d be Element of D;

      :: original: .

      redefine

      func f . d -> Element of F ;

      coherence

      proof

        thus (f . d) is Element of F;

      end;

    end

    reserve f for Function of [:C, D:], E;

    theorem :: FUNCT_5:67

    

     Th60: ( curry f) is Function of C, ( Funcs (D,E))

    proof

      

       A1: ( dom f) = [:C, D:] by FUNCT_2:def 1;

      

       A2: ( rng ( curry f)) c= ( Funcs (D,E))

      proof

        

         A3: ( rng ( curry f)) c= ( Funcs (D,( rng f))) by A1, Th28;

        let x be object;

        assume x in ( rng ( curry f));

        then

        consider g be Function such that

         A4: x = g and

         A5: ( dom g) = D and

         A6: ( rng g) c= ( rng f) by A3, FUNCT_2:def 2;

        ( rng g) c= E by A6, XBOOLE_1: 1;

        then g is Function of D, E by A5, FUNCT_2:def 1, RELSET_1: 4;

        hence thesis by A4, FUNCT_2: 8;

      end;

      ( dom ( curry f)) = C by A1, Th17;

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

    end;

    theorem :: FUNCT_5:68

    

     Th61: ( curry' f) is Function of D, ( Funcs (C,E))

    proof

      

       A1: ( dom f) = [:C, D:] by FUNCT_2:def 1;

      

       A2: ( rng ( curry' f)) c= ( Funcs (C,E))

      proof

        

         A3: ( rng ( curry' f)) c= ( Funcs (C,( rng f))) by A1, Th28;

        let x be object;

        assume x in ( rng ( curry' f));

        then

        consider g be Function such that

         A4: x = g and

         A5: ( dom g) = C and

         A6: ( rng g) c= ( rng f) by A3, FUNCT_2:def 2;

        ( rng g) c= E by A6, XBOOLE_1: 1;

        then g is Function of C, E by A5, FUNCT_2:def 1, RELSET_1: 4;

        hence thesis by A4, FUNCT_2: 8;

      end;

      ( dom ( curry' f)) = D by A1, Th17;

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

    end;

    definition

      let C, D, E, f;

      :: original: curry

      redefine

      func curry f -> Function of C, ( Funcs (D,E)) ;

      coherence by Th60;

      :: original: curry'

      redefine

      func curry' f -> Function of D, ( Funcs (C,E)) ;

      coherence by Th61;

    end

    theorem :: FUNCT_5:69

    (f . (c,d)) = ((( curry f) . c) . d)

    proof

       [c, d] in [:C, D:];

      then [c, d] in ( dom f) by FUNCT_2:def 1;

      hence thesis by Th13;

    end;

    theorem :: FUNCT_5:70

    (f . (c,d)) = ((( curry' f) . d) . c)

    proof

       [c, d] in [:C, D:];

      then [c, d] in ( dom f) by FUNCT_2:def 1;

      hence thesis by Th15;

    end;

    definition

      let A,B,C be non empty set;

      let f be Function of A, ( Funcs (B,C));

      :: original: uncurry

      redefine

      func uncurry f -> Function of [:A, B:], C ;

      coherence

      proof

        

         A1: ( rng f) c= ( Funcs (B,C));

        then

         A2: ( rng ( uncurry f)) c= C by Th34;

        ( dom ( uncurry f)) = [:( dom f), B:] by A1, Th19

        .= [:A, B:] by FUNCT_2:def 1;

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

      end;

    end

    theorem :: FUNCT_5:71

    for A,B,C be non empty set, f be Function of A, ( Funcs (B,C)) holds ( curry ( uncurry f)) = f

    proof

      let A,B,C be non empty set, f be Function of A, ( Funcs (B,C));

      ( rng f) c= ( Funcs (B,C));

      hence thesis by Th41;

    end;

    theorem :: FUNCT_5:72

    for A,B,C be non empty set, f be Function of A, ( Funcs (B,C)) holds for a be Element of A, b be Element of B holds (( uncurry f) . (a,b)) = ((f . a) . b)

    proof

      let A,B,C be non empty set, f be Function of A, ( Funcs (B,C));

      let a be Element of A, b be Element of B;

      ( dom f) = A & ( dom (f . a)) = B by FUNCT_2:def 1;

      hence thesis by Th31;

    end;