:: by Grzegorz Bancerek

::

:: Received March 6, 1990

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

theorem Th9: :: FUNCT_5:9

for Y, X being set st ( Y <> {} or [:X,Y:] <> {} or [:Y,X:] <> {} ) holds

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

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

proof end;

theorem Th14: :: FUNCT_5:14

for X being set st ( for x, y being set holds not [x,y] in X ) holds

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

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

proof end;

theorem :: FUNCT_5:15

theorem Th17: :: FUNCT_5:17

for f being Function holds

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

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

proof end;

definition

let f be Function;

ex b_{1} being Function st

( dom b_{1} = proj1 (dom f) & ( for x being set st x in proj1 (dom f) holds

ex g being Function st

( b_{1} . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in dom g holds

g . y = f . (x,y) ) ) ) )

for b_{1}, b_{2} being Function st dom b_{1} = proj1 (dom f) & ( for x being set st x in proj1 (dom f) holds

ex g being Function st

( b_{1} . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in dom g holds

g . y = f . (x,y) ) ) ) & dom b_{2} = proj1 (dom f) & ( for x being set st x in proj1 (dom f) holds

ex g being Function st

( b_{2} . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in dom g holds

g . y = f . (x,y) ) ) ) holds

b_{1} = b_{2}

ex b_{1} being Function st

( ( for t being set holds

( t in dom b_{1} iff ex x being set ex g being Function ex y being set st

( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) ) & ( for x being set

for g being Function st x in dom b_{1} & g = f . (x `1) holds

b_{1} . x = g . (x `2) ) )

for b_{1}, b_{2} being Function st ( for t being set holds

( t in dom b_{1} iff ex x being set ex g being Function ex y being set st

( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) ) & ( for x being set

for g being Function st x in dom b_{1} & g = f . (x `1) holds

b_{1} . x = g . (x `2) ) & ( for t being set holds

( t in dom b_{2} iff ex x being set ex g being Function ex y being set st

( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) ) & ( for x being set

for g being Function st x in dom b_{2} & g = f . (x `1) holds

b_{2} . x = g . (x `2) ) holds

b_{1} = b_{2}

end;
func curry f -> Function means :Def1: :: FUNCT_5:def 1

( dom it = proj1 (dom f) & ( for x being set st x in proj1 (dom f) holds

ex g being Function st

( it . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in dom g holds

g . y = f . (x,y) ) ) ) );

existence ( dom it = proj1 (dom f) & ( for x being set st x in proj1 (dom f) holds

ex g being Function st

( it . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in dom g holds

g . y = f . (x,y) ) ) ) );

ex b

( dom b

ex g being Function st

( b

g . y = f . (x,y) ) ) ) )

proof end;

uniqueness for b

ex g being Function st

( b

g . y = f . (x,y) ) ) ) & dom b

ex g being Function st

( b

g . y = f . (x,y) ) ) ) holds

b

proof end;

func uncurry f -> Function means :Def2: :: FUNCT_5:def 2

( ( for t being set holds

( t in dom it iff ex x being set ex g being Function ex y being set st

( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) ) & ( for x being set

for g being Function st x in dom it & g = f . (x `1) holds

it . x = g . (x `2) ) );

existence ( ( for t being set holds

( t in dom it iff ex x being set ex g being Function ex y being set st

( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) ) & ( for x being set

for g being Function st x in dom it & g = f . (x `1) holds

it . x = g . (x `2) ) );

ex b

( ( for t being set holds

( t in dom b

( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) ) & ( for x being set

for g being Function st x in dom b

b

proof end;

uniqueness for b

( t in dom b

( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) ) & ( for x being set

for g being Function st x in dom b

b

( t in dom b

( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) ) & ( for x being set

for g being Function st x in dom b

b

b

proof end;

:: deftheorem Def1 defines curry FUNCT_5:def 1 :

for f, b_{2} being Function holds

( b_{2} = curry f iff ( dom b_{2} = proj1 (dom f) & ( for x being set st x in proj1 (dom f) holds

ex g being Function st

( b_{2} . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in dom g holds

g . y = f . (x,y) ) ) ) ) );

for f, b

( b

ex g being Function st

( b

g . y = f . (x,y) ) ) ) ) );

:: deftheorem Def2 defines uncurry FUNCT_5:def 2 :

for f, b_{2} being Function holds

( b_{2} = uncurry f iff ( ( for t being set holds

( t in dom b_{2} iff ex x being set ex g being Function ex y being set st

( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) ) & ( for x being set

for g being Function st x in dom b_{2} & g = f . (x `1) holds

b_{2} . x = g . (x `2) ) ) );

for f, b

( b

( t in dom b

( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) ) & ( for x being set

for g being Function st x in dom b

b

definition

let f be Function;

correctness

coherence

curry (~ f) is Function;

;

correctness

coherence

~ (uncurry f) is Function;

;

end;
correctness

coherence

curry (~ f) is Function;

;

correctness

coherence

~ (uncurry f) is Function;

;

:: deftheorem defines uncurry' FUNCT_5:def 4 :

for f being Function holds uncurry' f = ~ (uncurry f);

for f being Function holds uncurry' f = ~ (uncurry f);

theorem Th19: :: FUNCT_5:19

for x, y being set

for f being Function st [x,y] in dom f holds

( x in dom (curry f) & (curry f) . x is Function )

for f being Function st [x,y] in dom f holds

( x in dom (curry f) & (curry f) . x is Function )

proof end;

theorem Th20: :: FUNCT_5:20

for x, y being set

for f, g being Function st [x,y] in dom f & g = (curry f) . x holds

( y in dom g & g . y = f . (x,y) )

for f, g being Function st [x,y] in dom f & g = (curry f) . x holds

( y in dom g & g . y = f . (x,y) )

proof end;

theorem :: FUNCT_5:21

for x, y being set

for f being Function st [x,y] in dom f holds

( y in dom (curry' f) & (curry' f) . y is Function )

for f being Function st [x,y] in dom f holds

( y in dom (curry' f) & (curry' f) . y is Function )

proof end;

theorem Th22: :: FUNCT_5:22

for x, y being set

for f, g being Function st [x,y] in dom f & g = (curry' f) . y holds

( x in dom g & g . x = f . (x,y) )

for f, g being Function st [x,y] in dom f & g = (curry' f) . y holds

( x in dom g & g . x = f . (x,y) )

proof end;

theorem Th24: :: FUNCT_5:24

for X, Y being set

for f being Function st [:X,Y:] <> {} & dom f = [:X,Y:] holds

( dom (curry f) = X & dom (curry' f) = Y )

for f being Function st [:X,Y:] <> {} & dom f = [:X,Y:] holds

( dom (curry f) = X & dom (curry' f) = Y )

proof end;

theorem Th25: :: FUNCT_5:25

for X, Y being set

for f being Function st dom f c= [:X,Y:] holds

( dom (curry f) c= X & dom (curry' f) c= Y )

for f being Function st dom f c= [:X,Y:] holds

( dom (curry f) c= X & dom (curry' f) c= Y )

proof end;

theorem Th26: :: FUNCT_5:26

for X, Y being set

for f being Function st rng f c= Funcs (X,Y) holds

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

for f being Function st rng f c= Funcs (X,Y) holds

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

proof end;

theorem :: FUNCT_5:27

for f being Function st ( for x, y being set holds not [x,y] in dom f ) holds

( curry f = {} & curry' f = {} )

( curry f = {} & curry' f = {} )

proof end;

theorem :: FUNCT_5:28

for f being Function st ( for x being set holds

( not x in dom f or not f . x is Function ) ) holds

( uncurry f = {} & uncurry' f = {} )

( not x in dom f or not f . x is Function ) ) holds

( uncurry f = {} & uncurry' f = {} )

proof end;

theorem Th29: :: FUNCT_5:29

for X, Y, x being set

for f being Function st [:X,Y:] <> {} & dom f = [:X,Y:] & x in X holds

ex g being Function st

( (curry f) . x = g & dom g = Y & rng g c= rng f & ( for y being set st y in Y holds

g . y = f . (x,y) ) )

for f being Function st [:X,Y:] <> {} & dom f = [:X,Y:] & x in X holds

ex g being Function st

( (curry f) . x = g & dom g = Y & rng g c= rng f & ( for y being set st y in Y holds

g . y = f . (x,y) ) )

proof end;

theorem Th31: :: FUNCT_5:31

for x being set

for f, g being Function st x in dom (curry f) & g = (curry f) . x holds

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

( g . y = f . (x,y) & [x,y] in dom f ) ) )

for f, g being Function st x in dom (curry f) & g = (curry f) . x holds

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

( g . y = f . (x,y) & [x,y] in dom f ) ) )

proof end;

theorem Th32: :: FUNCT_5:32

for X, Y, y being set

for f being Function st [:X,Y:] <> {} & dom f = [:X,Y:] & y in Y holds

ex g being Function st

( (curry' f) . y = g & dom g = X & rng g c= rng f & ( for x being set st x in X holds

g . x = f . (x,y) ) )

for f being Function st [:X,Y:] <> {} & dom f = [:X,Y:] & y in Y holds

ex g being Function st

( (curry' f) . y = g & dom g = X & rng g c= rng f & ( for x being set st x in X holds

g . x = f . (x,y) ) )

proof end;

theorem :: FUNCT_5:33

theorem :: FUNCT_5:34

for x being set

for f, g being Function st x in dom (curry' f) & g = (curry' f) . x holds

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

( g . y = f . (y,x) & [y,x] in dom f ) ) )

for f, g being Function st x in dom (curry' f) & g = (curry' f) . x holds

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

( g . y = f . (y,x) & [y,x] in dom f ) ) )

proof end;

theorem Th35: :: FUNCT_5:35

for X, Y being set

for f being Function st dom f = [:X,Y:] holds

( rng (curry f) c= Funcs (Y,(rng f)) & rng (curry' f) c= Funcs (X,(rng f)) )

for f being Function st dom f = [:X,Y:] holds

( rng (curry f) c= Funcs (Y,(rng f)) & rng (curry' f) c= Funcs (X,(rng f)) )

proof end;

theorem :: FUNCT_5:36

for f being Function holds

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

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

proof end;

theorem Th37: :: FUNCT_5:37

for X, Y being set

for f being Function st rng f c= PFuncs (X,Y) holds

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

for f being Function st rng f c= PFuncs (X,Y) holds

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

proof end;

theorem Th38: :: FUNCT_5:38

for x, y being set

for f, g being Function st x in dom f & g = f . x & y in dom g holds

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

for f, g being Function st x in dom f & g = f . x & y in dom g holds

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

proof end;

theorem :: FUNCT_5:39

for x, y being set

for f, g being Function st x in dom f & g = f . x & y in dom g holds

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

for f, g being Function st x in dom f & g = f . x & y in dom g holds

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

proof end;

theorem Th40: :: FUNCT_5:40

for X, Y being set

for f being Function st rng f c= PFuncs (X,Y) holds

( rng (uncurry f) c= Y & rng (uncurry' f) c= Y )

for f being Function st rng f c= PFuncs (X,Y) holds

( rng (uncurry f) c= Y & rng (uncurry' f) c= Y )

proof end;

theorem Th41: :: FUNCT_5:41

for X, Y being set

for f being Function st rng f c= Funcs (X,Y) holds

( rng (uncurry f) c= Y & rng (uncurry' f) c= Y )

for f being Function st rng f c= Funcs (X,Y) holds

( rng (uncurry f) c= Y & rng (uncurry' f) c= Y )

proof end;

theorem Th44: :: FUNCT_5:44

for X, Y being set

for f1, f2 being Function st dom f1 = [:X,Y:] & dom f2 = [:X,Y:] & curry f1 = curry f2 holds

f1 = f2

for f1, f2 being Function st dom f1 = [:X,Y:] & dom f2 = [:X,Y:] & curry f1 = curry f2 holds

f1 = f2

proof end;

theorem Th45: :: FUNCT_5:45

for X, Y being set

for f1, f2 being Function st dom f1 = [:X,Y:] & dom f2 = [:X,Y:] & curry' f1 = curry' f2 holds

f1 = f2

for f1, f2 being Function st dom f1 = [:X,Y:] & dom f2 = [:X,Y:] & curry' f1 = curry' f2 holds

f1 = f2

proof end;

theorem Th46: :: FUNCT_5:46

for X, Y being set

for f1, f2 being Function st rng f1 c= Funcs (X,Y) & rng f2 c= Funcs (X,Y) & X <> {} & uncurry f1 = uncurry f2 holds

f1 = f2

for f1, f2 being Function st rng f1 c= Funcs (X,Y) & rng f2 c= Funcs (X,Y) & X <> {} & uncurry f1 = uncurry f2 holds

f1 = f2

proof end;

theorem :: FUNCT_5:47

for X, Y being set

for f1, f2 being Function st rng f1 c= Funcs (X,Y) & rng f2 c= Funcs (X,Y) & X <> {} & uncurry' f1 = uncurry' f2 holds

f1 = f2

for f1, f2 being Function st rng f1 c= Funcs (X,Y) & rng f2 c= Funcs (X,Y) & X <> {} & uncurry' f1 = uncurry' f2 holds

f1 = f2

proof end;

theorem Th48: :: FUNCT_5:48

for X, Y being set

for f being Function st rng f c= Funcs (X,Y) & X <> {} holds

( curry (uncurry f) = f & curry' (uncurry' f) = f )

for f being Function st rng f c= Funcs (X,Y) & X <> {} holds

( curry (uncurry f) = f & curry' (uncurry' f) = f )

proof end;

theorem :: FUNCT_5:49

for X, Y being set

for f being Function st dom f = [:X,Y:] holds

( uncurry (curry f) = f & uncurry' (curry' f) = f )

for f being Function st dom f = [:X,Y:] holds

( uncurry (curry f) = f & uncurry' (curry' f) = f )

proof end;

theorem Th50: :: FUNCT_5:50

for X, Y being set

for f being Function st dom f c= [:X,Y:] holds

( uncurry (curry f) = f & uncurry' (curry' f) = f )

for f being Function st dom f c= [:X,Y:] holds

( uncurry (curry f) = f & uncurry' (curry' f) = f )

proof end;

theorem Th51: :: FUNCT_5:51

for X, Y being set

for f being Function st rng f c= PFuncs (X,Y) & not {} in rng f holds

( curry (uncurry f) = f & curry' (uncurry' f) = f )

for f being Function st rng f c= PFuncs (X,Y) & not {} in rng f holds

( curry (uncurry f) = f & curry' (uncurry' f) = f )

proof end;

theorem :: FUNCT_5:52

for X, Y being set

for f1, f2 being Function st dom f1 c= [:X,Y:] & dom f2 c= [:X,Y:] & curry f1 = curry f2 holds

f1 = f2

for f1, f2 being Function st dom f1 c= [:X,Y:] & dom f2 c= [:X,Y:] & curry f1 = curry f2 holds

f1 = f2

proof end;

theorem :: FUNCT_5:53

for X, Y being set

for f1, f2 being Function st dom f1 c= [:X,Y:] & dom f2 c= [:X,Y:] & curry' f1 = curry' f2 holds

f1 = f2

for f1, f2 being Function st dom f1 c= [:X,Y:] & dom f2 c= [:X,Y:] & curry' f1 = curry' f2 holds

f1 = f2

proof end;

theorem :: FUNCT_5:54

for X, Y being set

for f1, f2 being Function st rng f1 c= PFuncs (X,Y) & rng f2 c= PFuncs (X,Y) & not {} in rng f1 & not {} in rng f2 & uncurry f1 = uncurry f2 holds

f1 = f2

for f1, f2 being Function st rng f1 c= PFuncs (X,Y) & rng f2 c= PFuncs (X,Y) & not {} in rng f1 & not {} in rng f2 & uncurry f1 = uncurry f2 holds

f1 = f2

proof end;

theorem :: FUNCT_5:55

for X, Y being set

for f1, f2 being Function st rng f1 c= PFuncs (X,Y) & rng f2 c= PFuncs (X,Y) & not {} in rng f1 & not {} in rng f2 & uncurry' f1 = uncurry' f2 holds

f1 = f2

for f1, f2 being Function st rng f1 c= PFuncs (X,Y) & rng f2 c= PFuncs (X,Y) & not {} in rng f1 & not {} in rng f2 & uncurry' f1 = uncurry' f2 holds

f1 = f2

proof end;

theorem Th60: :: FUNCT_5:60

for X1, Y1, X2, Y2 being set st X1,Y1 are_equipotent & X2,Y2 are_equipotent holds

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

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

proof end;

theorem :: FUNCT_5:61

for X1, Y1, X2, Y2 being set st card X1 = card Y1 & card X2 = card Y2 holds

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

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

proof end;

theorem :: FUNCT_5:62

for X1, X2, X being set st X1 misses X2 holds

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

( 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 end;

theorem :: FUNCT_5:63

for X, Y, Z being set holds

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

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

proof end;

theorem :: FUNCT_5:64

for Z, X, Y being set holds

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

( 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 end;

theorem :: FUNCT_5:65

for x, y, X being set st x <> y holds

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

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

proof end;

theorem :: FUNCT_5:66

for x, y, X being set st x <> y holds

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

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

proof end;

begin

definition

:: original: op0

redefine func op0 -> Element of 1;

coherence

op0 is Element of 1 by CARD_1:49, TARSKI:def 1;

end;
redefine func op0 -> Element of 1;

coherence

op0 is Element of 1 by CARD_1:49, TARSKI:def 1;

definition

:: original: op1

redefine func op1 -> UnOp of 1;

coherence

op1 is UnOp of 1 by CARD_1:49;

:: original: op2

redefine func op2 -> BinOp of 1;

coherence

op2 is BinOp of 1 by CARD_1:49;

end;
redefine func op1 -> UnOp of 1;

coherence

op1 is UnOp of 1 by CARD_1:49;

:: original: op2

redefine func op2 -> BinOp of 1;

coherence

op2 is BinOp of 1 by CARD_1:49;

definition

let D be non empty set ;

let X be set ;

let E be non empty set ;

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

f . d is Element of F

end;
let X be set ;

let E be non empty set ;

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

f . d is Element of F

proof end;

theorem Th1: :: FUNCT_5:67

for C, D, E being non empty set

for f being Function of [:C,D:],E holds curry f is Function of C,(Funcs (D,E))

for f being Function of [:C,D:],E holds curry f is Function of C,(Funcs (D,E))

proof end;

theorem Th2: :: FUNCT_5:68

for D, C, E being non empty set

for f being Function of [:C,D:],E holds curry' f is Function of D,(Funcs (C,E))

for f being Function of [:C,D:],E holds curry' f is Function of D,(Funcs (C,E))

proof end;

definition

let C, D, E be non empty set ;

let f be Function of [:C,D:],E;

:: original: curry

redefine func curry f -> Function of C,(Funcs (D,E));

coherence

curry f is Function of C,(Funcs (D,E)) by Th1;

:: original: curry'

redefine func curry' f -> Function of D,(Funcs (C,E));

coherence

curry' f is Function of D,(Funcs (C,E)) by Th2;

end;
let f be Function of [:C,D:],E;

:: original: curry

redefine func curry f -> Function of C,(Funcs (D,E));

coherence

curry f is Function of C,(Funcs (D,E)) by Th1;

:: original: curry'

redefine func curry' f -> Function of D,(Funcs (C,E));

coherence

curry' f is Function of D,(Funcs (C,E)) by Th2;

theorem :: FUNCT_5:69

for C, D, E being non empty set

for c being Element of C

for d being Element of D

for f being Function of [:C,D:],E holds f . (c,d) = ((curry f) . c) . d

for c being Element of C

for d being Element of D

for f being Function of [:C,D:],E holds f . (c,d) = ((curry f) . c) . d

proof end;

theorem :: FUNCT_5:70

for C, D, E being non empty set

for c being Element of C

for d being Element of D

for f being Function of [:C,D:],E holds f . (c,d) = ((curry' f) . d) . c

for c being Element of C

for d being Element of D

for f being Function of [:C,D:],E holds f . (c,d) = ((curry' f) . d) . c

proof end;

:: from ISOCAT_2, 2011.11.25, A.T.

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

uncurry f is Function of [:A,B:],C

end;
let f be Function of A,(Funcs (B,C));

:: original: uncurry

redefine func uncurry f -> Function of [:A,B:],C;

coherence

uncurry f is Function of [:A,B:],C

proof end;

theorem :: FUNCT_5:72

for A, B, C being non empty set

for f being Function of A,(Funcs (B,C))

for a being Element of A

for b being Element of B holds (uncurry f) . (a,b) = (f . a) . b

for f being Function of A,(Funcs (B,C))

for a being Element of A

for b being Element of B holds (uncurry f) . (a,b) = (f . a) . b

proof end;