:: by Grzegorz Bancerek

::

:: Received September 30, 1991

:: Copyright (c) 1991-2021 Association of Mizar Users

theorem :: FUNCT_6:5

for z being object

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

( curry ([:X,Y:] --> z) = X --> (Y --> z) & curry' ([:X,Y:] --> z) = Y --> (X --> z) )

for X, Y 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:6

for z being object

for X, Y being set holds

( uncurry (X --> (Y --> z)) = [:X,Y:] --> z & uncurry' (X --> (Y --> z)) = [:Y,X:] --> z )

for X, Y being set holds

( uncurry (X --> (Y --> z)) = [:X,Y:] --> z & uncurry' (X --> (Y --> z)) = [:Y,X:] --> z )

proof end;

theorem Th7: :: FUNCT_6:7

for x being object

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) )

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 Th8: :: FUNCT_6:8

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 )

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:9

for X being set

for f being Function st X <> {} holds

( rng (uncurry (X --> f)) = rng f & rng (uncurry' (X --> f)) = rng f )

for f being Function st X <> {} holds

( rng (uncurry (X --> f)) = rng f & rng (uncurry' (X --> f)) = rng f )

proof end;

theorem Th10: :: FUNCT_6:10

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))) )

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 Th11: :: FUNCT_6:11

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) )

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:12

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)

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:13

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)))

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:14

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))) )

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 Th15: :: FUNCT_6:15

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) )

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:16

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)

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:17

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)))

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

::$CD

::$CD

::$CD

::$CD

::$CT 4

definition

let f be Function-yielding Function;

ex b_{1} being Function st

( dom b_{1} = dom f & ( for x being object st x in dom f holds

b_{1} . x = proj1 (f . x) ) )

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

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

b_{2} . x = proj1 (f . x) ) holds

b_{1} = b_{2}

ex b_{1} being Function st

( dom b_{1} = dom f & ( for x being object st x in dom f holds

b_{1} . x = proj2 (f . x) ) )

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

b_{1} . x = proj2 (f . x) ) & dom b_{2} = dom f & ( for x being object st x in dom f holds

b_{2} . x = proj2 (f . x) ) holds

b_{1} = b_{2}

end;
func doms f -> Function means :Def1: :: FUNCT_6:def 2

( dom it = dom f & ( for x being object st x in dom f holds

it . x = proj1 (f . x) ) );

existence ( dom it = dom f & ( for x being object st x in dom f holds

it . x = proj1 (f . x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

func rngs f -> Function means :Def2: :: FUNCT_6:def 3

( dom it = dom f & ( for x being object st x in dom f holds

it . x = proj2 (f . x) ) );

existence ( dom it = dom f & ( for x being object st x in dom f holds

it . x = proj2 (f . x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def1 defines doms FUNCT_6:def 2 :

for f being Function-yielding Function

for b_{2} being Function holds

( b_{2} = doms f iff ( dom b_{2} = dom f & ( for x being object st x in dom f holds

b_{2} . x = proj1 (f . x) ) ) );

for f being Function-yielding Function

for b

( b

b

:: deftheorem Def2 defines rngs FUNCT_6:def 3 :

for f being Function-yielding Function

for b_{2} being Function holds

( b_{2} = rngs f iff ( dom b_{2} = dom f & ( for x being object st x in dom f holds

b_{2} . x = proj2 (f . x) ) ) );

for f being Function-yielding Function

for b

( b

b

theorem Th20: :: FUNCT_6:24

for X being set

for f being Function holds

( doms (X --> f) = X --> (dom f) & rngs (X --> f) = X --> (rng f) )

for f being Function holds

( doms (X --> f) = X --> (dom f) & rngs (X --> f) = X --> (rng f) )

proof end;

theorem Th21: :: FUNCT_6:25

for f being Function st f <> {} holds

for x being object holds

( x in meet f iff for y being object st y in dom f holds

x in f . y )

for x being object holds

( x in meet f iff for y being object st y in dom f holds

x in f . y )

proof end;

definition
end;

:: deftheorem defines .. FUNCT_6:def 5 :

for f being Function

for x, y being object holds f .. (x,y) = (uncurry f) . (x,y);

for f being Function

for x, y being object holds f .. (x,y) = (uncurry f) . (x,y);

theorem :: FUNCT_6:28

for x, y being object

for X being set

for f being Function st x in X & y in dom f holds

(X --> f) .. (x,y) = f . y

for X 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-yielding Function;

correctness

coherence

curry ((uncurry' f) | [:(meet (doms f)),(dom f):]) is Function;

;

end;
correctness

coherence

curry ((uncurry' f) | [:(meet (doms f)),(dom f):]) is Function;

;

:: deftheorem defines <: FUNCT_6:def 6 :

for f being Function-yielding Function holds <:f:> = curry ((uncurry' f) | [:(meet (doms f)),(dom f):]);

for f being Function-yielding Function holds <:f:> = curry ((uncurry' f) | [:(meet (doms f)),(dom f):]);

theorem Th25: :: FUNCT_6:29

for f being Function-yielding Function holds

( dom <:f:> = meet (doms f) & rng <:f:> c= product (rngs f) )

( dom <:f:> = meet (doms f) & rng <:f:> c= product (rngs f) )

proof end;

::$CT

theorem Th26: :: FUNCT_6:31

for x being object

for g being Function

for f being Function-yielding Function st x in dom <:f:> & g = <:f:> . x holds

( dom g = dom f & ( for y being object st y in dom g holds

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

for g being Function

for f being Function-yielding Function st x in dom <:f:> & g = <:f:> . x holds

( dom g = dom f & ( for y being object st y in dom g holds

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

proof end;

theorem Th27: :: FUNCT_6:32

for x being object

for f being Function-yielding Function st x in dom <:f:> holds

for g being Function st g in rng f holds

x in dom g

for f being Function-yielding 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:33

for g being Function

for x being object

for f being Function-yielding 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:>

for x being object

for f being Function-yielding 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 Th29: :: FUNCT_6:34

for x, y being object

for g, h being Function

for f being Function-yielding Function st x in dom f & g = f . x & y in dom <:f:> & h = <:f:> . y holds

g . y = h . x

for g, h being Function

for f being Function-yielding 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:35

for x, y being object

for f being Function-yielding Function st x in dom f & f . x is Function & y in dom <:f:> holds

f .. (x,y) = <:f:> .. (y,x)

for f being Function-yielding 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-yielding Function;

ex b_{1} being Function st

( dom b_{1} = product (doms f) & ( for g being Function st g in product (doms f) holds

ex h being Function st

( b_{1} . g = h & dom h = dom f & ( for x being object st x in dom h holds

h . x = (uncurry f) . (x,(g . x)) ) ) ) )

for b_{1}, b_{2} being Function st dom b_{1} = product (doms f) & ( for g being Function st g in product (doms f) holds

ex h being Function st

( b_{1} . g = h & dom h = dom f & ( for x being object st x in dom h holds

h . x = (uncurry f) . (x,(g . x)) ) ) ) & dom b_{2} = product (doms f) & ( for g being Function st g in product (doms f) holds

ex h being Function st

( b_{2} . g = h & dom h = dom f & ( for x being object st x in dom h holds

h . x = (uncurry f) . (x,(g . x)) ) ) ) holds

b_{1} = b_{2}

end;
func Frege f -> Function means :Def6: :: 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 = dom f & ( for x being object st x in dom h holds

h . x = (uncurry f) . (x,(g . x)) ) ) ) );

existence ( 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 = dom f & ( for x being object st x in dom h holds

h . x = (uncurry f) . (x,(g . x)) ) ) ) );

ex b

( dom b

ex h being Function st

( b

h . x = (uncurry f) . (x,(g . x)) ) ) ) )

proof end;

uniqueness for b

ex h being Function st

( b

h . x = (uncurry f) . (x,(g . x)) ) ) ) & dom b

ex h being Function st

( b

h . x = (uncurry f) . (x,(g . x)) ) ) ) holds

b

proof end;

:: deftheorem Def6 defines Frege FUNCT_6:def 7 :

for f being Function-yielding Function

for b_{2} being Function holds

( b_{2} = Frege f iff ( dom b_{2} = product (doms f) & ( for g being Function st g in product (doms f) holds

ex h being Function st

( b_{2} . g = h & dom h = dom f & ( for x being object st x in dom h holds

h . x = (uncurry f) . (x,(g . x)) ) ) ) ) );

for f being Function-yielding Function

for b

( b

ex h being Function st

( b

h . x = (uncurry f) . (x,(g . x)) ) ) ) ) );

theorem :: FUNCT_6:36

for x being object

for g being Function

for f being Function-yielding Function st g in product (doms f) & x in dom g holds

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

for g being Function

for f being Function-yielding Function st g in product (doms f) & x in dom g holds

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

proof end;

Lm1: for f being Function-yielding Function holds rng (Frege f) c= product (rngs f)

proof end;

theorem :: FUNCT_6:37

for x being object

for g, h, h9 being Function

for f being Function-yielding Function st x in dom f & g = f . x & h in product (doms f) & h9 = (Frege f) . h holds

( h . x in dom g & h9 . x = g . (h . x) & h9 in product (rngs f) )

for g, h, h9 being Function

for f being Function-yielding Function st x in dom f & g = f . x & h in product (doms f) & h9 = (Frege f) . h holds

( h . x in dom g & h9 . x = g . (h . x) & h9 in product (rngs f) )

proof end;

Lm2: for f being Function-yielding Function holds product (rngs f) c= rng (Frege f)

proof end;

theorem Th34: :: FUNCT_6:39

for f being Function-yielding 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 )

( 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:41

for X being set

for f being Function st X <> {} holds

( dom <:(X --> f):> = dom f & ( for x being object st x in dom f holds

<:(X --> f):> . x = X --> (f . x) ) )

for f being Function st X <> {} holds

( dom <:(X --> f):> = dom f & ( for x being object st x in dom f holds

<:(X --> f):> . x = X --> (f . x) ) )

proof end;

theorem :: FUNCT_6:42

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 ) )

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 Th38: :: FUNCT_6:43

for X being set

for f, g being Function st dom f = X & dom g = X & ( for x being object st x in X holds

f . x,g . x are_equipotent ) holds

product f, product g are_equipotent

for f, g being Function st dom f = X & dom g = X & ( for x being object st x in X holds

f . x,g . x are_equipotent ) holds

product f, product g are_equipotent

proof end;

theorem Th39: :: FUNCT_6:44

for f, g, h being Function st dom f = dom h & dom g = rng h & h is one-to-one & ( for x being object st x in dom h holds

f . x,g . (h . x) are_equipotent ) holds

product f, product g are_equipotent

f . x,g . (h . x) are_equipotent ) holds

product f, product g are_equipotent

proof end;

theorem :: FUNCT_6:45

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

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 ;

ex b_{1} being Function st

( dom b_{1} = dom f & ( for x being object st x in dom f holds

b_{1} . x = Funcs ((f . x),X) ) )

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

b_{1} . x = Funcs ((f . x),X) ) & dom b_{2} = dom f & ( for x being object st x in dom f holds

b_{2} . x = Funcs ((f . x),X) ) holds

b_{1} = b_{2}

end;
let X be set ;

func Funcs (f,X) -> Function means :Def7: :: FUNCT_6:def 8

( dom it = dom f & ( for x being object st x in dom f holds

it . x = Funcs ((f . x),X) ) );

existence ( dom it = dom f & ( for x being object st x in dom f holds

it . x = Funcs ((f . x),X) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def7 defines Funcs FUNCT_6:def 8 :

for f being Function

for X being set

for b_{3} being Function holds

( b_{3} = Funcs (f,X) iff ( dom b_{3} = dom f & ( for x being object st x in dom f holds

b_{3} . x = Funcs ((f . x),X) ) ) );

for f being Function

for X being set

for b

( b

b

Lm3: for f, g being Function

for x, y, z being object 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:49

for X being set

for f being Function holds Funcs ((Union (disjoin f)),X), product (Funcs (f,X)) are_equipotent

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;

ex b_{1} being Function st

( dom b_{1} = dom f & ( for x being object st x in dom f holds

b_{1} . x = Funcs (X,(f . x)) ) )

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

b_{1} . x = Funcs (X,(f . x)) ) & dom b_{2} = dom f & ( for x being object st x in dom f holds

b_{2} . x = Funcs (X,(f . x)) ) holds

b_{1} = b_{2}

end;
let f be Function;

func Funcs (X,f) -> Function means :Def8: :: FUNCT_6:def 9

( dom it = dom f & ( for x being object st x in dom f holds

it . x = Funcs (X,(f . x)) ) );

existence ( dom it = dom f & ( for x being object st x in dom f holds

it . x = Funcs (X,(f . x)) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def8 defines Funcs FUNCT_6:def 9 :

for X being set

for f, b_{3} being Function holds

( b_{3} = Funcs (X,f) iff ( dom b_{3} = dom f & ( for x being object st x in dom f holds

b_{3} . x = Funcs (X,(f . x)) ) ) );

for X being set

for f, b

( b

b

Lm4: 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 :: FUNCT_6:53

for X being set

for f being Function holds product (Funcs (X,f)), Funcs (X,(product f)) are_equipotent

for f being Function holds product (Funcs (X,f)), Funcs (X,(product f)) are_equipotent

proof end;

:: from PRALG_2

:: deftheorem defines commute FUNCT_6:def 10 :

for f being Function holds commute f = curry' (uncurry f);

for f being Function holds commute f = curry' (uncurry f);

theorem :: FUNCT_6:54

theorem Th50: :: FUNCT_6:55

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)))

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:56

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 )

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:57

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

for f being Function st A <> {} & B <> {} & f in Funcs (A,(Funcs (B,C))) holds

commute (commute f) = f

proof end;

:: from EXTENS_1