:: FUNCT_5 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

scheme :: FUNCT_5:sch 1
LambdaFS{ F1() -> set , F2( set ) -> set } :
ex f being Function st
( dom f = F1() & ( for g being Function st g in F1() holds
f . g = F2(g) ) )
proof end;

theorem Th1: :: FUNCT_5:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
~ {} = {}
proof end;

definition
let X be set ;
func proj1 X -> set means :Def1: :: FUNCT_5:def 1
for x being set holds
( x in it iff ex y being set st [x,y] in X );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ex y being set st [x,y] in X )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ex y being set st [x,y] in X ) ) & ( for x being set holds
( x in b2 iff ex y being set st [x,y] in X ) ) holds
b1 = b2
proof end;
func proj2 X -> set means :Def2: :: FUNCT_5:def 2
for y being set holds
( y in it iff ex x being set st [x,y] in X );
existence
ex b1 being set st
for y being set holds
( y in b1 iff ex x being set st [x,y] in X )
proof end;
uniqueness
for b1, b2 being set st ( for y being set holds
( y in b1 iff ex x being set st [x,y] in X ) ) & ( for y being set holds
( y in b2 iff ex x being set st [x,y] in X ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines proj1 FUNCT_5:def 1 :
for X, b2 being set holds
( b2 = proj1 X iff for x being set holds
( x in b2 iff ex y being set st [x,y] in X ) );

:: deftheorem Def2 defines proj2 FUNCT_5:def 2 :
for X, b2 being set holds
( b2 = proj2 X iff for y being set holds
( y in b2 iff ex x being set st [x,y] in X ) );

theorem :: FUNCT_5:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FUNCT_5:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FUNCT_5:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, X being set st [x,y] in X holds
( x in proj1 X & y in proj2 X ) by Def1, Def2;

theorem Th5: :: FUNCT_5:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set st X c= Y holds
( proj1 X c= proj1 Y & proj2 X c= proj2 Y )
proof end;

theorem Th6: :: FUNCT_5:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set holds
( proj1 (X \/ Y) = (proj1 X) \/ (proj1 Y) & proj2 (X \/ Y) = (proj2 X) \/ (proj2 Y) )
proof end;

theorem :: FUNCT_5:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set holds
( proj1 (X /\ Y) c= (proj1 X) /\ (proj1 Y) & proj2 (X /\ Y) c= (proj2 X) /\ (proj2 Y) )
proof end;

theorem Th8: :: FUNCT_5:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set holds
( (proj1 X) \ (proj1 Y) c= proj1 (X \ Y) & (proj2 X) \ (proj2 Y) c= proj2 (X \ Y) )
proof end;

theorem :: FUNCT_5:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set holds
( (proj1 X) \+\ (proj1 Y) c= proj1 (X \+\ Y) & (proj2 X) \+\ (proj2 Y) c= proj2 (X \+\ Y) )
proof end;

theorem Th10: :: FUNCT_5:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( proj1 {} = {} & proj2 {} = {} )
proof end;

theorem Th11: :: FUNCT_5:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y, X being set st ( Y <> {} or [:X,Y:] <> {} or [:Y,X:] <> {} ) holds
( proj1 [:X,Y:] = X & proj2 [:Y,X:] = X )
proof end;

theorem Th12: :: FUNCT_5:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set holds
( proj1 [:X,Y:] c= X & proj2 [:X,Y:] c= Y )
proof end;

theorem Th13: :: FUNCT_5:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Z, X, Y being set st Z c= [:X,Y:] holds
( proj1 Z c= X & proj2 Z c= Y )
proof end;

theorem :: FUNCT_5:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th15: :: FUNCT_5:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being set holds
( proj1 {[x,y]} = {x} & proj2 {[x,y]} = {y} )
proof end;

theorem :: FUNCT_5:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z, t being set holds
( proj1 {[x,y],[z,t]} = {x,z} & proj2 {[x,y],[z,t]} = {y,t} )
proof end;

theorem Th17: :: FUNCT_5:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set st ( for x, y being set holds not [x,y] in X ) holds
( proj1 X = {} & proj2 X = {} )
proof end;

theorem :: FUNCT_5:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set st ( proj1 X = {} or proj2 X = {} ) holds
for x, y being set holds not [x,y] in X by Def1, Def2;

theorem :: FUNCT_5:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds
( proj1 X = {} iff proj2 X = {} )
proof end;

theorem Th20: :: FUNCT_5:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Function holds
( proj1 (dom f) = proj2 (dom (~ f)) & proj2 (dom f) = proj1 (dom (~ f)) )
proof end;

theorem :: FUNCT_5:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Relation holds
( proj1 f = dom f & proj2 f = rng f )
proof end;

definition
let f be Function;
func curry f -> Function means :Def3: :: FUNCT_5:def 3
( 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
ex b1 being Function st
( dom b1 = proj1 (dom f) & ( for x being set st x in proj1 (dom f) holds
ex g being Function st
( b1 . 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] ) ) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = proj1 (dom f) & ( for x being set st x in proj1 (dom f) holds
ex g being Function st
( b1 . 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 b2 = proj1 (dom f) & ( for x being set st x in proj1 (dom f) holds
ex g being Function st
( b2 . 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
b1 = b2
proof end;
func uncurry f -> Function means :Def4: :: FUNCT_5:def 4
( ( 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
ex b1 being Function st
( ( for t being set holds
( t in dom b1 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 b1 & g = f . (x `1 ) holds
b1 . x = g . (x `2 ) ) )
proof end;
uniqueness
for b1, b2 being Function st ( for t being set holds
( t in dom b1 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 b1 & g = f . (x `1 ) holds
b1 . x = g . (x `2 ) ) & ( for t being set holds
( t in dom b2 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 b2 & g = f . (x `1 ) holds
b2 . x = g . (x `2 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines curry FUNCT_5:def 3 :
for f, b2 being Function holds
( b2 = curry f iff ( dom b2 = proj1 (dom f) & ( for x being set st x in proj1 (dom f) holds
ex g being Function st
( b2 . 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] ) ) ) ) );

:: deftheorem Def4 defines uncurry FUNCT_5:def 4 :
for f, b2 being Function holds
( b2 = uncurry f iff ( ( for t being set holds
( t in dom b2 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 b2 & g = f . (x `1 ) holds
b2 . x = g . (x `2 ) ) ) );

definition
let f be Function;
func curry' f -> Function equals :: FUNCT_5:def 5
curry (~ f);
correctness
coherence
curry (~ f) is Function
;
;
func uncurry' f -> Function equals :: FUNCT_5:def 6
~ (uncurry f);
correctness
coherence
~ (uncurry f) is Function
;
;
end;

:: deftheorem defines curry' FUNCT_5:def 5 :
for f being Function holds curry' f = curry (~ f);

:: deftheorem defines uncurry' FUNCT_5:def 6 :
for f being Function holds uncurry' f = ~ (uncurry f);

theorem :: FUNCT_5:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FUNCT_5:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FUNCT_5:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FUNCT_5:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th26: :: FUNCT_5:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th27: :: FUNCT_5:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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] )
proof end;

theorem :: FUNCT_5:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: FUNCT_5:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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] )
proof end;

theorem :: FUNCT_5:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Function holds dom (curry' f) = proj2 (dom f)
proof end;

theorem Th31: :: FUNCT_5:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th32: :: FUNCT_5:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th33: :: FUNCT_5:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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):] )
proof end;

theorem :: FUNCT_5:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Function st ( for x, y being set holds not [x,y] in dom f ) holds
( curry f = {} & curry' f = {} )
proof end;

theorem :: FUNCT_5:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 = {} )
proof end;

theorem Th36: :: FUNCT_5:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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] ) )
proof end;

theorem Th37: :: FUNCT_5:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for f being Function st x in dom (curry f) holds
(curry f) . x is Function
proof end;

theorem Th38: :: FUNCT_5:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) ) )
proof end;

theorem Th39: :: FUNCT_5:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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] ) )
proof end;

theorem :: FUNCT_5:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for f being Function st x in dom (curry' f) holds
(curry' f) . x is Function by Th37;

theorem :: FUNCT_5:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) ) )
proof end;

theorem Th42: :: FUNCT_5:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem :: FUNCT_5:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem Th44: :: FUNCT_5:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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):] )
proof end;

theorem Th45: :: FUNCT_5:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem :: FUNCT_5:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem Th47: :: FUNCT_5:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th48: :: FUNCT_5:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th49: :: FUNCT_5:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( curry {} = {} & curry' {} = {} )
proof end;

theorem Th50: :: FUNCT_5:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( uncurry {} = {} & uncurry' {} = {} )
proof end;

theorem Th51: :: FUNCT_5:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th52: :: FUNCT_5:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th53: :: FUNCT_5:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: FUNCT_5:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th55: :: FUNCT_5:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: FUNCT_5:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set
for f being Function st dom f = [:X,Y:] holds
( uncurry (curry f) = f & uncurry' (curry' f) = f )
proof end;

theorem Th57: :: FUNCT_5:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set
for f being Function st dom f c= [:X,Y:] holds
( uncurry (curry f) = f & uncurry' (curry' f) = f )
proof end;

theorem Th58: :: FUNCT_5:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: FUNCT_5:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: FUNCT_5:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: FUNCT_5:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: FUNCT_5:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th63: :: FUNCT_5:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y, Z being set st X c= Y holds
Funcs Z,X c= Funcs Z,Y
proof end;

theorem Th64: :: FUNCT_5:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds Funcs {} ,X = {{} }
proof end;

theorem :: FUNCT_5:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, x being set holds
( X, Funcs {x},X are_equipotent & Card X = Card (Funcs {x},X) )
proof end;

theorem Th66: :: FUNCT_5:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, x being set holds Funcs X,{x} = {(X --> x)}
proof end;

theorem Th67: :: FUNCT_5:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem :: FUNCT_5:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem :: FUNCT_5:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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):] )
proof end;

theorem :: FUNCT_5:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)) )
proof end;

theorem :: FUNCT_5:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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):] )
proof end;

theorem :: FUNCT_5:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem :: FUNCT_5:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:] )
proof end;