:: Cartesian Product of Functions
:: by Grzegorz Bancerek
::
:: Copyright (c) 1991-2021 Association of Mizar Users

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

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

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

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

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) )
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 )
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 () & rng g c= rng () )
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 )
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 )
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))) )
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) )
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)
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)))
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))) )
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) )
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)
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)))
proof end;

definition
end;

:: deftheorem FUNCT_6:def 1 :
canceled;

::$CD theorem :: FUNCT_6:18 canceled; ::$CD
theorem :: FUNCT_6:19
canceled;

::$CD theorem :: FUNCT_6:20 canceled; ::$CD
theorem :: FUNCT_6:21
canceled;

::$CT 4 definition let f be Function-yielding Function; 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 ex b1 being Function st ( dom b1 = dom f & ( for x being object st x in dom f holds b1 . x = proj1 (f . x) ) ) proof end; uniqueness for b1, b2 being Function st dom b1 = dom f & ( for x being object st x in dom f holds b1 . x = proj1 (f . x) ) & dom b2 = dom f & ( for x being object st x in dom f holds b2 . x = proj1 (f . x) ) holds b1 = b2 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 ex b1 being Function st ( dom b1 = dom f & ( for x being object st x in dom f holds b1 . x = proj2 (f . x) ) ) proof end; uniqueness for b1, b2 being Function st dom b1 = dom f & ( for x being object st x in dom f holds b1 . x = proj2 (f . x) ) & dom b2 = dom f & ( for x being object st x in dom f holds b2 . x = proj2 (f . x) ) holds b1 = b2 proof end; end; :: deftheorem Def1 defines doms FUNCT_6:def 2 : for f being Function-yielding Function for b2 being Function holds ( b2 = doms f iff ( dom b2 = dom f & ( for x being object st x in dom f holds b2 . x = proj1 (f . x) ) ) ); :: deftheorem Def2 defines rngs FUNCT_6:def 3 : for f being Function-yielding Function for b2 being Function holds ( b2 = rngs f iff ( dom b2 = dom f & ( for x being object st x in dom f holds b2 . x = proj2 (f . x) ) ) ); definition let f be Function; func meet f -> set equals :: FUNCT_6:def 4 meet (rng f); correctness coherence meet (rng f) is set ; ; end; :: deftheorem defines meet FUNCT_6:def 4 : for f being Function holds meet f = meet (rng f); theorem Th18: :: FUNCT_6:22 for x being object for g being Function for f being Function-yielding 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 ) by ; theorem :: FUNCT_6:23 ( doms {} = {} & rngs {} = {} ) by ; 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) ) 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 ) proof end; theorem :: FUNCT_6:26 for Y being set holds ( Union () = {} & meet () = {} ) proof end; theorem Th23: :: FUNCT_6:27 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 object ; func f .. (x,y) -> set equals :: FUNCT_6:def 5 () . (x,y); correctness coherence () . (x,y) is set ; ; end; :: deftheorem defines .. FUNCT_6:def 5 : for f being Function for x, y being object holds f .. (x,y) = () . (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 proof end; definition let f be Function-yielding Function; func <:f:> -> Function equals :: FUNCT_6:def 6 curry (() | [:(meet (doms f)),(dom f):]); correctness coherence curry (() | [:(meet (doms f)),(dom f):]) is Function ; ; end; :: deftheorem defines <: FUNCT_6:def 6 : for f being Function-yielding Function holds <:f:> = curry (() | [:(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) ) proof end; registration let f be Function-yielding Function; coherence ; end; theorem :: FUNCT_6:30 canceled; ::$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 () & g . y = () . (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
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:>
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
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)
proof end;

definition
let f be Function-yielding Function;
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 = () . (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 = dom f & ( for x being object st x in dom h holds
h . x = () . (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 = dom f & ( for x being object st x in dom h holds
h . x = () . (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 = dom f & ( for x being object st x in dom h holds
h . x = () . (x,(g . x)) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines Frege FUNCT_6:def 7 :
for f being Function-yielding Function
for 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 = dom f & ( for x being object st x in dom h holds
h . x = () . (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
() .. (g,x) = f .. (x,(g . x))
proof end;

Lm1: for f being Function-yielding Function holds rng () 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 = () . 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 ()
proof end;

theorem Th33: :: FUNCT_6:38
for f being Function-yielding Function holds rng () = product (rngs f) by ;

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

theorem :: FUNCT_6:40
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) ) )
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 ) )
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
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
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
proof end;

definition
let f be Function;
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
ex b1 being Function st
( dom b1 = dom f & ( for x being object 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 object st x in dom f holds
b1 . x = Funcs ((f . x),X) ) & dom b2 = dom f & ( for x being object st x in dom f holds
b2 . x = Funcs ((f . x),X) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 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 object 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) --> {}
proof end;

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

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

Lm3: for f, g being Function
for x, y, z being object st [x,y] in dom f & g = () . 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 ()),X), product (Funcs (f,X)) are_equipotent
proof end;

definition
let X be set ;
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
ex b1 being Function st
( dom b1 = dom f & ( for x being object 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 object st x in dom f holds
b1 . x = Funcs (X,(f . x)) ) & dom b2 = dom f & ( for x being object st x in dom f holds
b2 . x = Funcs (X,(f . x)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 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 object st x in dom f holds
b3 . x = Funcs (X,(f . x)) ) ) );

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

proof end;

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

theorem Th46: :: FUNCT_6:51
for X being set holds Funcs (X,{}) = {}
proof end;

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

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

:: from PRALG_2
definition
let f be Function;
coherence ;
end;

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

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

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)))
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 & () . 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 () = f
proof end;

theorem :: FUNCT_6:58

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

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