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

theorem Th1: :: FUNCT_6:1  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 in product <*X*> iff ex y being set st
( y in X & x = <*y*> ) )
proof end;

theorem Th2: :: FUNCT_6:2  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
( z in product <*X,Y*> iff ex x, y being set st
( x in X & y in Y & z = <*x,y*> ) )
proof end;

theorem Th3: :: FUNCT_6:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, X, Y, Z being set holds
( a in product <*X,Y,Z*> iff ex x, y, z being set st
( x in X & y in Y & z in Z & a = <*x,y,z*> ) )
proof end;

theorem :: FUNCT_6:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set holds product <*D*> = 1 -tuples_on D
proof end;

theorem Th5: :: FUNCT_6:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D1, D2 being non empty set holds product <*D1,D2*> = { <*d1,d2*> where d1 is Element of D1, d2 is Element of D2 : verum }
proof end;

theorem :: FUNCT_6:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set holds product <*D,D*> = 2 -tuples_on D
proof end;

theorem Th7: :: FUNCT_6:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D1, D2, D3 being non empty set holds product <*D1,D2,D3*> = { <*d1,d2,d3*> where d1 is Element of D1, d2 is Element of D2, d3 is Element of D3 : verum }
proof end;

theorem :: FUNCT_6:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set holds product <*D,D,D*> = 3 -tuples_on D
proof end;

theorem :: FUNCT_6:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for D being non empty set holds product (i |-> D) = i -tuples_on D
proof end;

theorem Th10: :: FUNCT_6:10  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 product f c= Funcs (dom f),(Union f)
proof end;

theorem Th11: :: FUNCT_6:11  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 (~ f) holds
ex y, z being set st x = [y,z]
proof end;

theorem Th12: :: FUNCT_6:12  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 ~ ([:X,Y:] --> z) = [:Y,X:] --> z
proof end;

theorem Th13: :: FUNCT_6:13  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
( curry f = curry' (~ f) & uncurry f = ~ (uncurry' f) )
proof end;

theorem :: FUNCT_6:14  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,Y:] <> {} holds
( curry ([:X,Y:] --> z) = X --> (Y --> z) & curry' ([:X,Y:] --> z) = Y --> (X --> z) )
proof end;

theorem :: FUNCT_6:15  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
( uncurry (X --> (Y --> z)) = [:X,Y:] --> z & uncurry' (X --> (Y --> z)) = [:Y,X:] --> z )
proof end;

theorem Th16: :: FUNCT_6:16  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 f & g = f . x holds
( rng g c= rng (uncurry f) & rng g c= rng (uncurry' f) )
proof end;

theorem Th17: :: FUNCT_6: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
for f being Function holds
( dom (uncurry (X --> f)) = [:X,(dom f):] & rng (uncurry (X --> f)) c= rng f & dom (uncurry' (X --> f)) = [:(dom f),X:] & rng (uncurry' (X --> f)) c= rng f )
proof end;

theorem :: FUNCT_6: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
for f being Function st X <> {} holds
( rng (uncurry (X --> f)) = rng f & rng (uncurry' (X --> f)) = rng f )
proof end;

theorem Th19: :: FUNCT_6:19  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
for f being Function st [:X,Y:] <> {} & f in Funcs [:X,Y:],Z holds
( curry f in Funcs X,(Funcs Y,Z) & curry' f in Funcs Y,(Funcs X,Z) )
proof end;

theorem Th20: :: FUNCT_6:20  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
for f being Function st f in Funcs X,(Funcs Y,Z) holds
( uncurry f in Funcs [:X,Y:],Z & uncurry' f in Funcs [:Y,X:],Z )
proof end;

theorem :: FUNCT_6:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y, Z, V1, V2 being set
for f being Function st ( curry f in Funcs X,(Funcs Y,Z) or curry' f in Funcs Y,(Funcs X,Z) ) & dom f c= [:V1,V2:] holds
f in Funcs [:X,Y:],Z
proof end;

theorem :: FUNCT_6:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y, Z, V1, V2 being set
for f being Function st ( uncurry f in Funcs [:X,Y:],Z or uncurry' f in Funcs [:Y,X:],Z ) & rng f c= PFuncs V1,V2 & dom f = X holds
f in Funcs X,(Funcs Y,Z)
proof end;

theorem :: FUNCT_6:23  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
for f being Function st f in PFuncs [:X,Y:],Z holds
( curry f in PFuncs X,(PFuncs Y,Z) & curry' f in PFuncs Y,(PFuncs X,Z) )
proof end;

theorem Th24: :: FUNCT_6:24  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
for f being Function st f in PFuncs X,(PFuncs Y,Z) holds
( uncurry f in PFuncs [:X,Y:],Z & uncurry' f in PFuncs [:Y,X:],Z )
proof end;

theorem :: FUNCT_6:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y, Z, V1, V2 being set
for f being Function st ( curry f in PFuncs X,(PFuncs Y,Z) or curry' f in PFuncs Y,(PFuncs X,Z) ) & dom f c= [:V1,V2:] holds
f in PFuncs [:X,Y:],Z
proof end;

theorem :: FUNCT_6:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y, Z, V1, V2 being set
for f being Function st ( uncurry f in PFuncs [:X,Y:],Z or uncurry' f in PFuncs [:Y,X:],Z ) & rng f c= PFuncs V1,V2 & dom f c= X holds
f in PFuncs X,(PFuncs Y,Z)
proof end;

definition
let X be set ;
func SubFuncs X -> set means :Def1: :: FUNCT_6:def 1
for x being set holds
( x in it iff ( x in X & x is Function ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ( x in X & x is Function ) )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x in X & x is Function ) ) ) & ( for x being set holds
( x in b2 iff ( x in X & x is Function ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines SubFuncs FUNCT_6:def 1 :
for X being set
for b2 being set holds
( b2 = SubFuncs X iff for x being set holds
( x in b2 iff ( x in X & x is Function ) ) );

theorem Th27: :: FUNCT_6:27  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 SubFuncs X c= X
proof end;

theorem Th28: :: FUNCT_6:28  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 holds
( x in f " (SubFuncs (rng f)) iff ( x in dom f & f . x is Function ) )
proof end;

Lm1: for X being set st ( for x being set st x in X holds
x is Function ) holds
SubFuncs X = X
proof end;

theorem Th29: :: FUNCT_6:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g, h being Function holds
( SubFuncs {} = {} & SubFuncs {f} = {f} & SubFuncs {f,g} = {f,g} & SubFuncs {f,g,h} = {f,g,h} )
proof end;

theorem :: FUNCT_6:30  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 c= SubFuncs X holds
SubFuncs Y = Y
proof end;

definition
let f be Function;
func doms f -> Function means :Def2: :: FUNCT_6:def 2
( dom it = f " (SubFuncs (rng f)) & ( for x being set st x in f " (SubFuncs (rng f)) holds
it . x = proj1 (f . x) ) );
existence
ex b1 being Function st
( dom b1 = f " (SubFuncs (rng f)) & ( for x being set st x in f " (SubFuncs (rng f)) holds
b1 . x = proj1 (f . x) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = f " (SubFuncs (rng f)) & ( for x being set st x in f " (SubFuncs (rng f)) holds
b1 . x = proj1 (f . x) ) & dom b2 = f " (SubFuncs (rng f)) & ( for x being set st x in f " (SubFuncs (rng f)) holds
b2 . x = proj1 (f . x) ) holds
b1 = b2
proof end;
func rngs f -> Function means :Def3: :: FUNCT_6:def 3
( dom it = f " (SubFuncs (rng f)) & ( for x being set st x in f " (SubFuncs (rng f)) holds
it . x = proj2 (f . x) ) );
existence
ex b1 being Function st
( dom b1 = f " (SubFuncs (rng f)) & ( for x being set st x in f " (SubFuncs (rng f)) holds
b1 . x = proj2 (f . x) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = f " (SubFuncs (rng f)) & ( for x being set st x in f " (SubFuncs (rng f)) holds
b1 . x = proj2 (f . x) ) & dom b2 = f " (SubFuncs (rng f)) & ( for x being set st x in f " (SubFuncs (rng f)) holds
b2 . x = proj2 (f . x) ) holds
b1 = b2
proof end;
func meet f -> set equals :: FUNCT_6:def 4
meet (rng f);
correctness
coherence
meet (rng f) is set
;
;
end;

:: deftheorem Def2 defines doms FUNCT_6:def 2 :
for f, b2 being Function holds
( b2 = doms f iff ( dom b2 = f " (SubFuncs (rng f)) & ( for x being set st x in f " (SubFuncs (rng f)) holds
b2 . x = proj1 (f . x) ) ) );

:: deftheorem Def3 defines rngs FUNCT_6:def 3 :
for f, b2 being Function holds
( b2 = rngs f iff ( dom b2 = f " (SubFuncs (rng f)) & ( for x being set st x in f " (SubFuncs (rng f)) holds
b2 . x = proj2 (f . x) ) ) );

:: deftheorem defines meet FUNCT_6:def 4 :
for f being Function holds meet f = meet (rng f);

theorem Th31: :: FUNCT_6:31  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 f & g = f . x holds
( x in dom (doms f) & (doms f) . x = dom g & x in dom (rngs f) & (rngs f) . x = rng g )
proof end;

theorem :: FUNCT_6:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( doms {} = {} & rngs {} = {} )
proof end;

theorem Th33: :: FUNCT_6:33  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
( doms <*f*> = <*(dom f)*> & rngs <*f*> = <*(rng f)*> )
proof end;

theorem Th34: :: FUNCT_6:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being Function holds
( doms <*f,g*> = <*(dom f),(dom g)*> & rngs <*f,g*> = <*(rng f),(rng g)*> )
proof end;

theorem :: FUNCT_6:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g, h being Function holds
( doms <*f,g,h*> = <*(dom f),(dom g),(dom h)*> & rngs <*f,g,h*> = <*(rng f),(rng g),(rng h)*> )
proof end;

theorem Th36: :: FUNCT_6:36  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 holds
( doms (X --> f) = X --> (dom f) & rngs (X --> f) = X --> (rng f) )
proof end;

theorem Th37: :: FUNCT_6: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 f <> {} holds
( x in meet f iff for y being set st y in dom f holds
x in f . y )
proof end;

theorem :: FUNCT_6:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
meet {} = {} by SETFAM_1:2;

theorem Th39: :: FUNCT_6:39  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
( Union <*X*> = X & meet <*X*> = X )
proof end;

theorem Th40: :: FUNCT_6:40  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
( Union <*X,Y*> = X \/ Y & meet <*X,Y*> = X /\ Y )
proof end;

theorem :: FUNCT_6:41  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
( Union <*X,Y,Z*> = (X \/ Y) \/ Z & meet <*X,Y,Z*> = (X /\ Y) /\ Z )
proof end;

theorem :: FUNCT_6:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being set holds
( Union ({} --> Y) = {} & meet ({} --> Y) = {} )
proof end;

theorem Th43: :: FUNCT_6:43  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 <> {} holds
( Union (X --> Y) = Y & meet (X --> Y) = Y )
proof end;

definition
let f be Function;
let x, y be set ;
func f .. x,y -> set equals :: FUNCT_6:def 5
(uncurry f) . [x,y];
correctness
coherence
(uncurry f) . [x,y] is set
;
;
end;

:: deftheorem defines .. FUNCT_6:def 5 :
for f being Function
for x, y being set holds f .. x,y = (uncurry f) . [x,y];

theorem Th44: :: FUNCT_6: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, g being Function st x in dom f & g = f . x & y in dom g holds
f .. x,y = g . y by FUNCT_5:45;

theorem :: FUNCT_6:45  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, h being Function st x in dom f holds
( <*f*> .. 1,x = f . x & <*f,g*> .. 1,x = f . x & <*f,g,h*> .. 1,x = f . x )
proof end;

theorem :: FUNCT_6:46  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 g, f, h being Function st x in dom g holds
( <*f,g*> .. 2,x = g . x & <*f,g,h*> .. 2,x = g . x )
proof end;

theorem :: FUNCT_6:47  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 h, f, g being Function st x in dom h holds
<*f,g,h*> .. 3,x = h . x
proof end;

theorem :: FUNCT_6:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, X, y being set
for f being Function st x in X & y in dom f holds
(X --> f) .. x,y = f . y
proof end;

definition
let f be Function;
func <:f:> -> Function equals :: FUNCT_6:def 6
curry ((uncurry' f) | [:(meet (doms f)),(dom f):]);
correctness
coherence
curry ((uncurry' f) | [:(meet (doms f)),(dom f):]) is Function
;
;
end;

:: deftheorem defines <: FUNCT_6:def 6 :
for f being Function holds <:f:> = curry ((uncurry' f) | [:(meet (doms f)),(dom f):]);

theorem Th49: :: FUNCT_6:49  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 <:f:> = meet (doms f) & rng <:f:> c= product (rngs f) )
proof end;

theorem Th50: :: FUNCT_6:50  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 <:f:> holds
<:f:> . x is Function
proof end;

theorem Th51: :: FUNCT_6:51  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 <:f:> & g = <:f:> . x holds
( dom g = f " (SubFuncs (rng f)) & ( for y being set st y in dom g holds
( [y,x] in dom (uncurry f) & g . y = (uncurry f) . [y,x] ) ) )
proof end;

theorem Th52: :: FUNCT_6:52  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 <:f:> holds
for g being Function st g in rng f holds
x in dom g
proof end;

theorem :: FUNCT_6:53  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 g, f being Function st g in rng f & ( for g being Function st g in rng f holds
x in dom g ) holds
x in dom <:f:>
proof end;

theorem Th54: :: FUNCT_6: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 f, g, h being Function st x in dom f & g = f . x & y in dom <:f:> & h = <:f:> . y holds
g . y = h . x
proof end;

theorem :: FUNCT_6: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 x in dom f & f . x is Function & y in dom <:f:> holds
f .. x,y = <:f:> .. y,x
proof end;

definition
let f be Function;
func Frege f -> Function means :Def7: :: FUNCT_6:def 7
( dom it = product (doms f) & ( for g being Function st g in product (doms f) holds
ex h being Function st
( it . g = h & dom h = f " (SubFuncs (rng f)) & ( for x being set st x in dom h holds
h . x = (uncurry f) . [x,(g . x)] ) ) ) );
existence
ex b1 being Function st
( dom b1 = product (doms f) & ( for g being Function st g in product (doms f) holds
ex h being Function st
( b1 . g = h & dom h = f " (SubFuncs (rng f)) & ( for x being set st x in dom h holds
h . x = (uncurry f) . [x,(g . x)] ) ) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = product (doms f) & ( for g being Function st g in product (doms f) holds
ex h being Function st
( b1 . g = h & dom h = f " (SubFuncs (rng f)) & ( for x being set st x in dom h holds
h . x = (uncurry f) . [x,(g . x)] ) ) ) & dom b2 = product (doms f) & ( for g being Function st g in product (doms f) holds
ex h being Function st
( b2 . g = h & dom h = f " (SubFuncs (rng f)) & ( for x being set st x in dom h holds
h . x = (uncurry f) . [x,(g . x)] ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines Frege FUNCT_6:def 7 :
for f, b2 being Function holds
( b2 = Frege f iff ( dom b2 = product (doms f) & ( for g being Function st g in product (doms f) holds
ex h being Function st
( b2 . g = h & dom h = f " (SubFuncs (rng f)) & ( for x being set st x in dom h holds
h . x = (uncurry f) . [x,(g . x)] ) ) ) ) );

theorem :: FUNCT_6:56  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 g, f being Function st g in product (doms f) & x in dom g holds
(Frege f) .. g,x = f .. x,(g . x)
proof end;

Lm2: for f being Function holds rng (Frege f) c= product (rngs f)
proof end;

theorem Th57: :: FUNCT_6:57  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, h, h' being Function st x in dom f & g = f . x & h in product (doms f) & h' = (Frege f) . h holds
( h . x in dom g & h' . x = g . (h . x) & h' in product (rngs f) )
proof end;

Lm3: for f being Function holds product (rngs f) c= rng (Frege f)
proof end;

theorem Th58: :: FUNCT_6:58  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 (Frege f) = product (rngs f)
proof end;

theorem Th59: :: FUNCT_6:59  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 not {} in rng f holds
( Frege f is one-to-one iff for g being Function st g in rng f holds
g is one-to-one )
proof end;

theorem :: FUNCT_6:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( <:{} :> = {} & Frege {} = {{} } --> {} )
proof end;

theorem :: FUNCT_6:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for h being Function holds
( dom <:<*h*>:> = dom h & ( for x being set st x in dom h holds
<:<*h*>:> . x = <*(h . x)*> ) )
proof end;

theorem Th62: :: FUNCT_6:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f1, f2 being Function holds
( dom <:<*f1,f2*>:> = (dom f1) /\ (dom f2) & ( for x being set st x in (dom f1) /\ (dom f2) holds
<:<*f1,f2*>:> . x = <*(f1 . x),(f2 . x)*> ) )
proof end;

theorem :: FUNCT_6:63  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 <> {} holds
( dom <:(X --> f):> = dom f & ( for x being set st x in dom f holds
<:(X --> f):> . x = X --> (f . x) ) )
proof end;

theorem :: FUNCT_6:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for h being Function holds
( dom (Frege <*h*>) = product <*(dom h)*> & rng (Frege <*h*>) = product <*(rng h)*> & ( for x being set st x in dom h holds
(Frege <*h*>) . <*x*> = <*(h . x)*> ) )
proof end;

theorem Th65: :: FUNCT_6:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f1, f2 being Function holds
( dom (Frege <*f1,f2*>) = product <*(dom f1),(dom f2)*> & rng (Frege <*f1,f2*>) = product <*(rng f1),(rng f2)*> & ( for x, y being set st x in dom f1 & y in dom f2 holds
(Frege <*f1,f2*>) . <*x,y*> = <*(f1 . x),(f2 . y)*> ) )
proof end;

theorem :: FUNCT_6:66  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 holds
( dom (Frege (X --> f)) = Funcs X,(dom f) & rng (Frege (X --> f)) = Funcs X,(rng f) & ( for g being Function st g in Funcs X,(dom f) holds
(Frege (X --> f)) . g = f * g ) )
proof end;

theorem :: FUNCT_6:67  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 f1, f2 being Function st x in dom f1 & x in dom f2 holds
for y1, y2 being set holds
( <:f1,f2:> . x = [y1,y2] iff <:<*f1,f2*>:> . x = <*y1,y2*> )
proof end;

theorem :: FUNCT_6:68  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 x in dom f1 & y in dom f2 holds
for y1, y2 being set holds
( [:f1,f2:] . [x,y] = [y1,y2] iff (Frege <*f1,f2*>) . <*x,y*> = <*y1,y2*> )
proof end;

theorem Th69: :: FUNCT_6:69  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 dom f = X & dom g = X & ( for x being set st x in X holds
f . x,g . x are_equipotent ) holds
product f, product g are_equipotent
proof end;

theorem Th70: :: FUNCT_6:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, h, g being Function st dom f = dom h & dom g = rng h & h is one-to-one & ( for x being set st x in dom h holds
f . x,g . (h . x) are_equipotent ) holds
product f, product g are_equipotent
proof end;

theorem :: FUNCT_6:71  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
for P being Permutation of X st dom f = X holds
product f, product (f * P) are_equipotent
proof end;

definition
let f be Function;
let X be set ;
func Funcs f,X -> Function means :Def8: :: FUNCT_6:def 8
( dom it = dom f & ( for x being set st x in dom f holds
it . x = Funcs (f . x),X ) );
existence
ex b1 being Function st
( dom b1 = dom f & ( for x being set st x in dom f holds
b1 . x = Funcs (f . x),X ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = dom f & ( for x being set st x in dom f holds
b1 . x = Funcs (f . x),X ) & dom b2 = dom f & ( for x being set st x in dom f holds
b2 . x = Funcs (f . x),X ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines Funcs FUNCT_6:def 8 :
for f being Function
for X being set
for b3 being Function holds
( b3 = Funcs f,X iff ( dom b3 = dom f & ( for x being set st x in dom f holds
b3 . x = Funcs (f . x),X ) ) );

theorem :: FUNCT_6:72  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 not {} in rng f holds
Funcs f,{} = (dom f) --> {}
proof end;

theorem :: FUNCT_6:73  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_6:74  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 Funcs <*X*>,Y = <*(Funcs X,Y)*>
proof end;

theorem :: FUNCT_6:75  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,Z),(Funcs Y,Z)*>
proof end;

theorem :: FUNCT_6:76  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 = X --> (Funcs Y,Z)
proof end;

Lm4: for x, y, z being set
for f, g being Function st [x,y] in dom f & g = (curry f) . x & z in dom g holds
[x,z] in dom f
proof end;

theorem :: FUNCT_6:77  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 holds Funcs (Union (disjoin f)),X, product (Funcs f,X) are_equipotent
proof end;

definition
let X be set ;
let f be Function;
func Funcs X,f -> Function means :Def9: :: FUNCT_6:def 9
( dom it = dom f & ( for x being set st x in dom f holds
it . x = Funcs X,(f . x) ) );
existence
ex b1 being Function st
( dom b1 = dom f & ( for x being set st x in dom f holds
b1 . x = Funcs X,(f . x) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = dom f & ( for x being set st x in dom f holds
b1 . x = Funcs X,(f . x) ) & dom b2 = dom f & ( for x being set st x in dom f holds
b2 . x = Funcs X,(f . x) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines Funcs FUNCT_6:def 9 :
for X being set
for f, b3 being Function holds
( b3 = Funcs X,f iff ( dom b3 = dom f & ( for x being set st x in dom f holds
b3 . x = Funcs X,(f . x) ) ) );

Lm5: for X being set
for f being Function st f <> {} & X <> {} holds
product (Funcs X,f), Funcs X,(product f) are_equipotent
proof end;

theorem Th78: :: FUNCT_6:78  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 Funcs {} ,f = (dom f) --> {{} }
proof end;

theorem Th79: :: FUNCT_6:79  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_6:80  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 Funcs X,<*Y*> = <*(Funcs X,Y)*>
proof end;

theorem :: FUNCT_6:81  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,Y),(Funcs X,Z)*>
proof end;

theorem :: FUNCT_6:82  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) = Y --> (Funcs X,Z)
proof end;

theorem :: FUNCT_6:83  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 holds product (Funcs X,f), Funcs X,(product f) are_equipotent
proof end;

definition
let f be Function;
canceled;
canceled;
func commute f -> Function-yielding Function equals :: FUNCT_6:def 12
curry' (uncurry f);
coherence
curry' (uncurry f) is Function-yielding Function
proof end;
end;

:: deftheorem FUNCT_6:def 10 :
canceled;

:: deftheorem FUNCT_6:def 11 :
canceled;

:: deftheorem defines commute FUNCT_6:def 12 :
for f being Function holds commute f = curry' (uncurry f);

theorem :: FUNCT_6:84  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Function
for x being set st x in dom (commute f) holds
(commute f) . x is Function ;

theorem Th85: :: FUNCT_6:85  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C being set
for f being Function st A <> {} & B <> {} & f in Funcs A,(Funcs B,C) holds
commute f in Funcs B,(Funcs A,C)
proof end;

theorem :: FUNCT_6:86  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C being set
for f being Function st A <> {} & B <> {} & f in Funcs A,(Funcs B,C) holds
for g, h being Function
for x, y being set st x in A & y in B & f . x = g & (commute f) . y = h holds
( h . x = g . y & dom h = A & dom g = B & rng h c= C & rng g c= C )
proof end;

theorem :: FUNCT_6:87  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C being set
for f being Function st A <> {} & B <> {} & f in Funcs A,(Funcs B,C) holds
commute (commute f) = f
proof end;

Lm6: for f being Function st dom f = {} holds
commute f = {}
by RELAT_1:64, FUNCT_5:49, FUNCT_5:50;

theorem :: FUNCT_6:88  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
commute {} = {} by Lm6, RELAT_1:60;

theorem :: FUNCT_6:89  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Function-yielding Function holds dom (doms f) = dom f
proof end;

theorem :: FUNCT_6:90  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Function-yielding Function holds dom (rngs f) = dom f
proof end;