:: Cartesian Product of Functions
:: by Grzegorz Bancerek
::
:: Received September 30, 1991
:: Copyright (c) 1991-2012 Association of Mizar Users


begin

theorem Th1: :: FUNCT_6:1
for f being Function holds product f c= Funcs ((dom f),(Union f))
proofend;

begin

theorem Th2: :: FUNCT_6:2
for x being set
for f being Function st x in dom (~ f) holds
ex y, z being set st x = [y,z]
proofend;

theorem Th3: :: FUNCT_6:3
for X, Y, z being set holds ~ ([:X,Y:] --> z) = [:Y,X:] --> z
proofend;

theorem Th4: :: FUNCT_6:4
for f being Function holds
( curry f = curry' (~ f) & uncurry f = ~ (uncurry' f) )
proofend;

theorem :: FUNCT_6:5
for X, Y, z being set st [:X,Y:] <> {} holds
( curry ([:X,Y:] --> z) = X --> (Y --> z) &amp; curry' ([:X,Y:] --> z) = Y --> (X --> z) )
proofend;

theorem :: FUNCT_6:6
for X, Y, z being set holds
( uncurry (X --> (Y --> z)) = [:X,Y:] --> z &amp; uncurry' (X --> (Y --> z)) = [:Y,X:] --> z )
proofend;

theorem Th7: :: FUNCT_6:7
for x being set
for f, g being Function st x in dom f &amp; g = f . x holds
( rng g c= rng (uncurry f) &amp; rng g c= rng (uncurry' f) )
proofend;

theorem Th8: :: FUNCT_6:8
for X being set
for f being Function holds
( dom (uncurry (X --> f)) = [:X,(dom f):] &amp; rng (uncurry (X --> f)) c= rng f &amp; dom (uncurry' (X --> f)) = [:(dom f),X:] &amp; rng (uncurry' (X --> f)) c= rng f )
proofend;

theorem :: FUNCT_6:9
for X being set
for f being Function st X <> {} holds
( rng (uncurry (X --> f)) = rng f &amp; rng (uncurry' (X --> f)) = rng f )
proofend;

theorem Th10: :: FUNCT_6:10
for X, Y, Z being set
for f being Function st [:X,Y:] <> {} &amp; f in Funcs ([:X,Y:],Z) holds
( curry f in Funcs (X,(Funcs (Y,Z))) &amp; curry' f in Funcs (Y,(Funcs (X,Z))) )
proofend;

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) &amp; uncurry' f in Funcs ([:Y,X:],Z) )
proofend;

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))) ) &amp; dom f c= [:V1,V2:] holds
f in Funcs ([:X,Y:],Z)
proofend;

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) ) &amp; rng f c= PFuncs (V1,V2) &amp; dom f = X holds
f in Funcs (X,(Funcs (Y,Z)))
proofend;

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))) &amp; curry' f in PFuncs (Y,(PFuncs (X,Z))) )
proofend;

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) &amp; uncurry' f in PFuncs ([:Y,X:],Z) )
proofend;

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))) ) &amp; dom f c= [:V1,V2:] holds
f in PFuncs ([:X,Y:],Z)
proofend;

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) ) &amp; rng f c= PFuncs (V1,V2) &amp; dom f c= X holds
f in PFuncs (X,(PFuncs (Y,Z)))
proofend;

begin

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 &amp; x is Function ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ( x in X &amp; x is Function ) )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x in X &amp; x is Function ) ) ) &amp; ( for x being set holds
( x in b2 iff ( x in X &amp; x is Function ) ) ) holds
b1 = b2
proofend;
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 &amp; x is Function ) ) );

theorem Th18: :: FUNCT_6:18
for X being set holds SubFuncs X c= X
proofend;

theorem Th19: :: FUNCT_6:19
for x being set
for f being Function holds
( x in f " (SubFuncs (rng f)) iff ( x in dom f &amp; f . x is Function ) )
proofend;

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

theorem :: FUNCT_6:20
for f, g, h being Function holds
( SubFuncs {} = {} &amp; SubFuncs {f} = {f} &amp; SubFuncs {f,g} = {f,g} &amp; SubFuncs {f,g,h} = {f,g,h} )
proofend;

theorem :: FUNCT_6:21
for Y, X being set st Y c= SubFuncs X holds
SubFuncs Y = Y
proofend;

definition
let f be Function;
func doms f ->  Function means :Def2: :: FUNCT_6:def 2
( dom it = f " (SubFuncs (rng f)) &amp; ( 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)) &amp; ( for x being set st x in f " (SubFuncs (rng f)) holds
b1 . x = proj1 (f . x) ) )
proofend;
uniqueness
 for b1, b2 being Function st dom b1 = f " (SubFuncs (rng f)) &amp; ( for x being set st x in f " (SubFuncs (rng f)) holds
b1 . x = proj1 (f . x) ) &amp; dom b2 = f " (SubFuncs (rng f)) &amp; ( for x being set st x in f " (SubFuncs (rng f)) holds
b2 . x = proj1 (f . x) ) holds
b1 = b2
proofend;
func rngs f ->  Function means :Def3: :: FUNCT_6:def 3
( dom it = f " (SubFuncs (rng f)) &amp; ( 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)) &amp; ( for x being set st x in f " (SubFuncs (rng f)) holds
b1 . x = proj2 (f . x) ) )
proofend;
uniqueness
 for b1, b2 being Function st dom b1 = f " (SubFuncs (rng f)) &amp; ( for x being set st x in f " (SubFuncs (rng f)) holds
b1 . x = proj2 (f . x) ) &amp; dom b2 = f " (SubFuncs (rng f)) &amp; ( for x being set st x in f " (SubFuncs (rng f)) holds
b2 . x = proj2 (f . x) ) holds
b1 = b2
proofend;
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)) &amp; ( 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)) &amp; ( 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 Th22: :: FUNCT_6:22
for x being set
for f, g being Function st x in dom f &amp; g = f . x holds
( x in dom (doms f) &amp; (doms f) . x = dom g &amp; x in dom (rngs f) &amp; (rngs f) . x = rng g )
proofend;

theorem :: FUNCT_6:23
( doms {} = {} &amp; rngs {} = {} )
proofend;

theorem Th24: :: FUNCT_6:24
for X being set
for f being Function holds
( doms (X --> f) = X --> (dom f) &amp; rngs (X --> f) = X --> (rng f) )
proofend;

theorem Th25: :: FUNCT_6:25
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 )
proofend;

theorem :: FUNCT_6:26
for Y being set holds
( Union ({} --> Y) = {} &amp; meet ({} --> Y) = {} )
proofend;

theorem Th27: :: FUNCT_6:27
for X, Y being set st X <> {} holds
( Union (X --> Y) = Y &amp; meet (X --> Y) = Y )
proofend;

definition
let f be Function;
let x, y be set ;
funcf .. (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 :: FUNCT_6:28
for x, X, y being set
for f being Function st x in X &amp; y in dom f holds
(X --> f) .. (x,y) = f . y
proofend;

begin

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 Th29: :: FUNCT_6:29
for f being Function holds
( dom <:f:> = meet (doms f) &amp; rng <:f:> c= product (rngs f) )
proofend;

theorem Th30: :: FUNCT_6:30
for x being set
for f being Function st x in dom <:f:> holds
<:f:> . x is Function
proofend;

theorem Th31: :: FUNCT_6:31
for x being set
for f, g being Function st x in dom <:f:> &amp; g = <:f:> . x holds
( dom g = f " (SubFuncs (rng f)) &amp; ( for y being set st y in dom g holds
( [y,x] in dom (uncurry f) &amp; g . y = (uncurry f) . (y,x) ) ) )
proofend;

theorem Th32: :: FUNCT_6:32
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
proofend;

theorem :: FUNCT_6:33
for x being set
for g, f being Function st g in rng f &amp; ( for g being Function st g in rng f holds
x in dom g ) holds
x in dom <:f:>
proofend;

theorem Th34: :: FUNCT_6:34
for x, y being set
for f, g, h being Function st x in dom f &amp; g = f . x &amp; y in dom <:f:> &amp; h = <:f:> . y holds
g . y = h . x
proofend;

theorem :: FUNCT_6:35
for x, y being set
for f being Function st x in dom f &amp; f . x is Function &amp; y in dom <:f:> holds
f .. (x,y) = <:f:> .. (y,x)
proofend;

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

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

theorem :: FUNCT_6:36
for x being set
for g, f being Function st g in product (doms f) &amp; x in dom g holds
(Frege f) .. (g,x) = f .. (x,(g . x))
proofend;

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

theorem :: FUNCT_6:37
for x being set
for f, g, h, h9 being Function st x in dom f &amp; g = f . x &amp; h in product (doms f) &amp; h9 = (Frege f) . h holds
( h . x in dom g &amp; h9 . x = g . (h . x) &amp; h9 in product (rngs f) )
proofend;

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

theorem Th38: :: FUNCT_6:38
for f being Function holds rng (Frege f) = product (rngs f)
proofend;

theorem Th39: :: FUNCT_6:39
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 )
proofend;

begin

theorem :: FUNCT_6:40
( <:{}:> = {} &amp; Frege {} = {} .--> {} )
proofend;

theorem :: FUNCT_6:41
for X being set
for f being Function st X <> {} holds
( dom <:(X --> f):> = dom f &amp; ( for x being set st x in dom f holds
<:(X --> f):> . x = X --> (f . x) ) )
proofend;

theorem :: FUNCT_6:42
for X being set
for f being Function holds
( dom (Frege (X --> f)) = Funcs (X,(dom f)) &amp; rng (Frege (X --> f)) = Funcs (X,(rng f)) &amp; ( for g being Function st g in Funcs (X,(dom f)) holds
(Frege (X --> f)) . g = f * g ) )
proofend;

theorem Th43: :: FUNCT_6:43
for X being set
for f, g being Function st dom f = X &amp; dom g = X &amp; ( for x being set st x in X holds
f . x,g . x are_equipotent ) holds
product f, product g are_equipotent
proofend;

theorem Th44: :: FUNCT_6:44
for f, h, g being Function st dom f = dom h &amp; dom g = rng h &amp; h is one-to-one &amp; ( for x being set st x in dom h holds
f . x,g . (h . x) are_equipotent ) holds
product f, product g are_equipotent
proofend;

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

begin

definition
let f be Function;
let X be set ;
func Funcs (f,X) ->  Function means :Def8: :: FUNCT_6:def 8
( dom it = dom f &amp; ( 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 &amp; ( for x being set st x in dom f holds
b1 . x = Funcs ((f . x),X) ) )
proofend;
uniqueness
 for b1, b2 being Function st dom b1 = dom f &amp; ( for x being set st x in dom f holds
b1 . x = Funcs ((f . x),X) ) &amp; dom b2 = dom f &amp; ( for x being set st x in dom f holds
b2 . x = Funcs ((f . x),X) ) holds
b1 = b2
proofend;
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 &amp; ( for x being set st x in dom f holds
b3 . x = Funcs ((f . x),X) ) ) );

theorem :: FUNCT_6:46
for f being Function st not {} in rng f holds
Funcs (f,{}) = (dom f) --> {}
proofend;

theorem :: FUNCT_6:47
for X being set holds Funcs ({},X) = {}
proofend;

theorem :: FUNCT_6:48
for X, Y, Z being set holds Funcs ((X --> Y),Z) = X --> (Funcs (Y,Z))
proofend;

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

theorem :: FUNCT_6:49
for X being set
for f being Function holds Funcs ((Union (disjoin f)),X), product (Funcs (f,X)) are_equipotent
proofend;

definition
let X be set ;
let f be Function;
func Funcs (X,f) ->  Function means :Def9: :: FUNCT_6:def 9
( dom it = dom f &amp; ( 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 &amp; ( for x being set st x in dom f holds
b1 . x = Funcs (X,(f . x)) ) )
proofend;
uniqueness
 for b1, b2 being Function st dom b1 = dom f &amp; ( for x being set st x in dom f holds
b1 . x = Funcs (X,(f . x)) ) &amp; dom b2 = dom f &amp; ( for x being set st x in dom f holds
b2 . x = Funcs (X,(f . x)) ) holds
b1 = b2
proofend;
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 &amp; ( 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 <> {} &amp; X <> {} holds
product (Funcs (X,f)), Funcs (X,(product f)) are_equipotent
proofend;

theorem Th50: :: FUNCT_6:50
for f being Function holds Funcs ({},f) = (dom f) --> {{}}
proofend;

theorem Th51: :: FUNCT_6:51
for X being set holds Funcs (X,{}) = {}
proofend;

theorem :: FUNCT_6:52
for X, Y, Z being set holds Funcs (X,(Y --> Z)) = Y --> (Funcs (X,Z))
proofend;

theorem :: FUNCT_6:53
for X being set
for f being Function holds product (Funcs (X,f)), Funcs (X,(product f)) are_equipotent
proofend;

begin

:: from PRALG_2
definition
let f be Function;
func commute f ->  Function-yielding Function equals :: FUNCT_6:def 10
 curry' (uncurry f);
coherence
 curry' (uncurry f) is Function-yielding Function
proofend;
end;

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

theorem :: FUNCT_6:54
for f being Function
for x being set st x in dom (commute f) holds
(commute f) . x is Function ;

theorem Th55: :: FUNCT_6:55
for A, B, C being set
for f being Function st A <> {} &amp; B <> {} &amp; f in Funcs (A,(Funcs (B,C))) holds
commute f in Funcs (B,(Funcs (A,C)))
proofend;

theorem :: FUNCT_6:56
for A, B, C being set
for f being Function st A <> {} &amp; B <> {} &amp; f in Funcs (A,(Funcs (B,C))) holds
for g, h being Function
for x, y being set st x in A &amp; y in B &amp; f . x = g &amp; (commute f) . y = h holds
( h . x = g . y &amp; dom h = A &amp; dom g = B &amp; rng h c= C &amp; rng g c= C )
proofend;

theorem :: FUNCT_6:57
for A, B, C being set
for f being Function st A <> {} &amp; B <> {} &amp; f in Funcs (A,(Funcs (B,C))) holds
commute (commute f) = f
proofend;

theorem :: FUNCT_6:58
commute {} = {} by FUNCT_5:42, FUNCT_5:43;

:: from EXTENS_1
theorem :: FUNCT_6:59
for f being Function-yielding Function holds dom (doms f) = dom f
proofend;

theorem :: FUNCT_6:60
for f being Function-yielding Function holds dom (rngs f) = dom f
proofend;