:: FUNCT_6 semantic presentation

begin


theorem Th1: :: FUNCT_6:1
for f being Function holds product f c= Funcs ((dom f),(Union f))
proof
let f be Function; ::_thesis: product f c= Funcs ((dom f),(Union f))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in product f or x in Funcs ((dom f),(Union f)) )
assume  x in product f ; ::_thesis: x in Funcs ((dom f),(Union f))
then consider g being Function such that
A1: x = g and
A2: dom g = dom f and
A3: for x being set st x in dom f holds
g . x in f . x by CARD_3:def_5;
 rng g c= Union f
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng g or y in Union f )
A4: Union f = union (rng f) by CARD_3:def_4;
assume  y in rng g ; ::_thesis: y in Union f
then consider z being set  such that
A5: ( z in dom g & y = g . z ) by FUNCT_1:def_3;
 ( y in f . z & f . z in rng f ) by A2, A3, A5, FUNCT_1:def_3;
hence  y in Union f by A4, TARSKI:def_4; ::_thesis: verum
end;
hence  x in Funcs ((dom f),(Union f)) by A1, A2, FUNCT_2:def_2; ::_thesis: verum
end;

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]
proof
let x be set ; ::_thesis: for f being Function st x in dom (~ f) holds
ex y, z being set st x = [y,z]
let f be Function; ::_thesis: ( x in dom (~ f) implies ex y, z being set st x = [y,z] )
assume A1: x in dom (~ f) ; ::_thesis: ex y, z being set st x = [y,z]
 ex X, Y being set st dom (~ f) c= [:X,Y:] by FUNCT_4:44;
hence  ex y, z being set st x = [y,z] by A1, RELAT_1:def_1; ::_thesis: verum
end;

theorem Th3: :: FUNCT_6:3
for X, Y, z being set holds ~ ([:X,Y:] --> z) = [:Y,X:] --> z
proof
let X, Y, z be set ; ::_thesis: ~ ([:X,Y:] --> z) = [:Y,X:] --> z
A1: dom ([:X,Y:] --> z) = [:X,Y:] by FUNCOP_1:13;
then A2: dom (~ ([:X,Y:] --> z)) = [:Y,X:] by FUNCT_4:46;
A3: now__::_thesis:_for_x_being_set_st_x_in_[:Y,X:]_holds_
(~_([:X,Y:]_-->_z))_._x_=_([:Y,X:]_-->_z)_._x
let x be set ; ::_thesis: ( x in [:Y,X:] implies (~ ([:X,Y:] --> z)) . x = ([:Y,X:] --> z) . x )
assume A4: x in [:Y,X:] ; ::_thesis: (~ ([:X,Y:] --> z)) . x = ([:Y,X:] --> z) . x
then consider y1, y2 being set  such that
A5: x = [y2,y1] and
A6: [y1,y2] in [:X,Y:] by A1, A2, FUNCT_4:def_2;
A7: ([:X,Y:] --> z) . (y1,y2) = z by A6, FUNCOP_1:7;
 ([:Y,X:] --> z) . (y2,y1) = z by A4, A5, FUNCOP_1:7;
then  (~ ([:X,Y:] --> z)) . (y2,y1) = ([:Y,X:] --> z) . (y2,y1) by A1, A6, A7, FUNCT_4:def_2;
hence  (~ ([:X,Y:] --> z)) . x = ([:Y,X:] --> z) . x by A5; ::_thesis: verum
end;
 dom ([:Y,X:] --> z) = [:Y,X:] by FUNCOP_1:13;
hence  ~ ([:X,Y:] --> z) = [:Y,X:] --> z by A2, A3, FUNCT_1:2; ::_thesis: verum
end;

theorem Th4: :: FUNCT_6:4
for f being Function holds
( curry f = curry' (~ f) & uncurry f = ~ (uncurry' f) )
proof
let f be Function; ::_thesis: ( curry f = curry' (~ f) & uncurry f = ~ (uncurry' f) )
A1: dom (curry (~ (~ f))) = proj1 (dom (~ (~ f))) by FUNCT_5:def_1;
A2: dom (curry f) = proj1 (dom f) by FUNCT_5:def_1;
A3: dom (curry (~ (~ f))) = dom (curry f)
proof
thus  dom (curry (~ (~ f))) c= dom (curry f) :: according to XBOOLE_0:def_10 ::_thesis: dom (curry f) c= dom (curry (~ (~ f)))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (curry (~ (~ f))) or x in dom (curry f) )
assume  x in dom (curry (~ (~ f))) ; ::_thesis: x in dom (curry f)
then consider y being set  such that
A4: [x,y] in dom (~ (~ f)) by A1, XTUPLE_0:def_12;
 [y,x] in dom (~ f) by A4, FUNCT_4:42;
then  [x,y] in dom f by FUNCT_4:42;
hence  x in dom (curry f) by A2, XTUPLE_0:def_12; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (curry f) or x in dom (curry (~ (~ f))) )
assume  x in dom (curry f) ; ::_thesis: x in dom (curry (~ (~ f)))
then consider y being set  such that
A5: [x,y] in dom f by A2, XTUPLE_0:def_12;
 [y,x] in dom (~ f) by A5, FUNCT_4:42;
then  [x,y] in dom (~ (~ f)) by FUNCT_4:42;
hence  x in dom (curry (~ (~ f))) by A1, XTUPLE_0:def_12; ::_thesis: verum
end;
A6: curry' (~ f) = curry (~ (~ f)) by FUNCT_5:def_3;
now__::_thesis:_for_x_being_set_st_x_in_dom_(curry_f)_holds_
(curry_f)_._x_=_(curry'_(~_f))_._x
let x be set ; ::_thesis: ( x in dom (curry f) implies (curry f) . x = (curry' (~ f)) . x )
assume A7: x in dom (curry f) ; ::_thesis: (curry f) . x = (curry' (~ f)) . x
then reconsider g = (curry f) . x, h = (curry' (~ f)) . x as Function by A6, A3, FUNCT_5:30;
A8: dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) by A7, FUNCT_5:31;
A9: dom h = proj1 ((dom (~ f)) /\ [:(proj1 (dom (~ f))),{x}:]) by A6, A3, A7, FUNCT_5:34;
A10: dom g = dom h
proof
thus  dom g c= dom h :: according to XBOOLE_0:def_10 ::_thesis: dom h c= dom g
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in dom g or a in dom h )
assume  a in dom g ; ::_thesis: a in dom h
then consider b being set  such that
A11: [b,a] in (dom f) /\ [:{x},(proj2 (dom f)):] by A8, XTUPLE_0:def_13;
 [b,a] in [:{x},(proj2 (dom f)):] by A11, XBOOLE_0:def_4;
then A12: [a,b] in [:(proj2 (dom f)),{x}:] by ZFMISC_1:88;
 [b,a] in dom f by A11, XBOOLE_0:def_4;
then A13: [a,b] in dom (~ f) by FUNCT_4:42;
 proj2 (dom f) = proj1 (dom (~ f)) by FUNCT_5:17;
then  [a,b] in (dom (~ f)) /\ [:(proj1 (dom (~ f))),{x}:] by A13, A12, XBOOLE_0:def_4;
hence  a in dom h by A9, XTUPLE_0:def_12; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in dom h or a in dom g )
assume  a in dom h ; ::_thesis: a in dom g
then consider b being set  such that
A14: [a,b] in (dom (~ f)) /\ [:(proj1 (dom (~ f))),{x}:] by A9, XTUPLE_0:def_12;
 [a,b] in [:(proj1 (dom (~ f))),{x}:] by A14, XBOOLE_0:def_4;
then A15: [b,a] in [:{x},(proj1 (dom (~ f))):] by ZFMISC_1:88;
 [a,b] in dom (~ f) by A14, XBOOLE_0:def_4;
then A16: [b,a] in dom f by FUNCT_4:42;
 proj2 (dom f) = proj1 (dom (~ f)) by FUNCT_5:17;
then  [b,a] in (dom f) /\ [:{x},(proj2 (dom f)):] by A16, A15, XBOOLE_0:def_4;
hence  a in dom g by A8, XTUPLE_0:def_13; ::_thesis: verum
end;
now__::_thesis:_for_a_being_set_st_a_in_dom_g_holds_
g_._a_=_h_._a
let a be set ; ::_thesis: ( a in dom g implies g . a = h . a )
assume A17: a in dom g ; ::_thesis: g . a = h . a
then A18: ( [x,a] in dom f & g . a = f . (x,a) ) by A7, FUNCT_5:31;
 h . a = (~ f) . (a,x) by A6, A3, A7, A10, A17, FUNCT_5:34;
hence  g . a = h . a by A18, FUNCT_4:def_2; ::_thesis: verum
end;
hence  (curry f) . x = (curry' (~ f)) . x by A10, FUNCT_1:2; ::_thesis: verum
end;
hence  curry f = curry' (~ f) by A6, A3, FUNCT_1:2; ::_thesis: uncurry f = ~ (uncurry' f)
A19: dom (uncurry f) = dom (~ (~ (uncurry f)))
proof
thus  dom (uncurry f) c= dom (~ (~ (uncurry f))) :: according to XBOOLE_0:def_10 ::_thesis: dom (~ (~ (uncurry f))) c= dom (uncurry f)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in dom (uncurry f) or a in dom (~ (~ (uncurry f))) )
assume A20: a in dom (uncurry f) ; ::_thesis: a in dom (~ (~ (uncurry f)))
then consider x being set , g being Function, y being set  such that
A21: a = [x,y] and
 x in dom f and
 g = f . x and
 y in dom g by FUNCT_5:def_2;
 [y,x] in dom (~ (uncurry f)) by A20, A21, FUNCT_4:42;
hence  a in dom (~ (~ (uncurry f))) by A21, FUNCT_4:42; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in dom (~ (~ (uncurry f))) or a in dom (uncurry f) )
assume  a in dom (~ (~ (uncurry f))) ; ::_thesis: a in dom (uncurry f)
then  ex x, y being set st
( a = [y,x] & [x,y] in dom (~ (uncurry f)) ) by FUNCT_4:def_2;
hence  a in dom (uncurry f) by FUNCT_4:42; ::_thesis: verum
end;
A22: now__::_thesis:_for_a_being_set_st_a_in_dom_(~_(~_(uncurry_f)))_holds_
(uncurry_f)_._a_=_(~_(~_(uncurry_f)))_._a
let a be set ; ::_thesis: ( a in dom (~ (~ (uncurry f))) implies (uncurry f) . a = (~ (~ (uncurry f))) . a )
assume  a in dom (~ (~ (uncurry f))) ; ::_thesis: (uncurry f) . a = (~ (~ (uncurry f))) . a
then consider x, y being set  such that
A23: a = [y,x] and
A24: [x,y] in dom (~ (uncurry f)) by FUNCT_4:def_2;
 ( (~ (uncurry f)) . (x,y) = (uncurry f) . (y,x) & (~ (uncurry f)) . (x,y) = (~ (~ (uncurry f))) . (y,x) ) by A24, FUNCT_4:43, FUNCT_4:def_2;
hence  (uncurry f) . a = (~ (~ (uncurry f))) . a by A23; ::_thesis: verum
end;
 uncurry' f = ~ (uncurry f) by FUNCT_5:def_4;
hence  uncurry f = ~ (uncurry' f) by A19, A22, FUNCT_1:2; ::_thesis: verum
end;

theorem :: FUNCT_6:5
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
let X, Y, z be set ; ::_thesis: ( [:X,Y:] <> {} implies ( curry ([:X,Y:] --> z) = X --> (Y --> z) & curry' ([:X,Y:] --> z) = Y --> (X --> z) ) )
assume A1: [:X,Y:] <> {} ; ::_thesis: ( curry ([:X,Y:] --> z) = X --> (Y --> z) & curry' ([:X,Y:] --> z) = Y --> (X --> z) )
A2: dom ([:X,Y:] --> z) = [:X,Y:] by FUNCOP_1:13;
A3: dom (X --> z) = X by FUNCOP_1:13;
A4: now__::_thesis:_for_x_being_set_st_x_in_Y_holds_
(curry'_([:X,Y:]_-->_z))_._x_=_(Y_-->_(X_-->_z))_._x
let x be set ; ::_thesis: ( x in Y implies (curry' ([:X,Y:] --> z)) . x = (Y --> (X --> z)) . x )
assume A5: x in Y ; ::_thesis: (curry' ([:X,Y:] --> z)) . x = (Y --> (X --> z)) . x
then consider f being Function such that
A6: ( (curry' ([:X,Y:] --> z)) . x = f & dom f = X ) and
 rng f c= rng ([:X,Y:] --> z) and
A7: for y being set st y in X holds
f . y = ([:X,Y:] --> z) . (y,x) by A1, A2, FUNCT_5:32;
A8: now__::_thesis:_for_y_being_set_st_y_in_X_holds_
f_._y_=_(X_-->_z)_._y
let y be set ; ::_thesis: ( y in X implies f . y = (X --> z) . y )
assume A9: y in X ; ::_thesis: f . y = (X --> z) . y
then A10: f . y = ([:X,Y:] --> z) . (y,x) by A7;
 ( (X --> z) . y = z & [y,x] in [:X,Y:] ) by A5, A9, FUNCOP_1:7, ZFMISC_1:87;
hence  f . y = (X --> z) . y by A10, FUNCOP_1:7; ::_thesis: verum
end;
 (Y --> (X --> z)) . x = X --> z by A5, FUNCOP_1:7;
hence  (curry' ([:X,Y:] --> z)) . x = (Y --> (X --> z)) . x by A3, A6, A8, FUNCT_1:2; ::_thesis: verum
end;
A11: dom (Y --> z) = Y by FUNCOP_1:13;
A12: now__::_thesis:_for_x_being_set_st_x_in_X_holds_
(curry_([:X,Y:]_-->_z))_._x_=_(X_-->_(Y_-->_z))_._x
let x be set ; ::_thesis: ( x in X implies (curry ([:X,Y:] --> z)) . x = (X --> (Y --> z)) . x )
assume A13: x in X ; ::_thesis: (curry ([:X,Y:] --> z)) . x = (X --> (Y --> z)) . x
then consider f being Function such that
A14: ( (curry ([:X,Y:] --> z)) . x = f & dom f = Y ) and
 rng f c= rng ([:X,Y:] --> z) and
A15: for y being set st y in Y holds
f . y = ([:X,Y:] --> z) . (x,y) by A1, A2, FUNCT_5:29;
A16: now__::_thesis:_for_y_being_set_st_y_in_Y_holds_
f_._y_=_(Y_-->_z)_._y
let y be set ; ::_thesis: ( y in Y implies f . y = (Y --> z) . y )
assume A17: y in Y ; ::_thesis: f . y = (Y --> z) . y
then A18: f . y = ([:X,Y:] --> z) . (x,y) by A15;
 ( (Y --> z) . y = z & [x,y] in [:X,Y:] ) by A13, A17, FUNCOP_1:7, ZFMISC_1:87;
hence  f . y = (Y --> z) . y by A18, FUNCOP_1:7; ::_thesis: verum
end;
 (X --> (Y --> z)) . x = Y --> z by A13, FUNCOP_1:7;
hence  (curry ([:X,Y:] --> z)) . x = (X --> (Y --> z)) . x by A11, A14, A16, FUNCT_1:2; ::_thesis: verum
end;
 ( dom (X --> (Y --> z)) = X & dom (curry ([:X,Y:] --> z)) = X ) by A1, A2, FUNCOP_1:13, FUNCT_5:24;
hence  curry ([:X,Y:] --> z) = X --> (Y --> z) by A12, FUNCT_1:2; ::_thesis: curry' ([:X,Y:] --> z) = Y --> (X --> z)
 ( dom (Y --> (X --> z)) = Y & dom (curry' ([:X,Y:] --> z)) = Y ) by A1, A2, FUNCOP_1:13, FUNCT_5:24;
hence  curry' ([:X,Y:] --> z) = Y --> (X --> z) by A4, FUNCT_1:2; ::_thesis: verum
end;

theorem :: FUNCT_6:6
for X, Y, z being set holds
( uncurry (X --> (Y --> z)) = [:X,Y:] --> z & uncurry' (X --> (Y --> z)) = [:Y,X:] --> z )
proof
let X, Y, z be set ; ::_thesis: ( uncurry (X --> (Y --> z)) = [:X,Y:] --> z & uncurry' (X --> (Y --> z)) = [:Y,X:] --> z )
A1: dom (X --> (Y --> z)) = X by FUNCOP_1:13;
A2: dom (Y --> z) = Y by FUNCOP_1:13;
 rng (Y --> z) c= {z} by FUNCOP_1:13;
then  Y --> z in Funcs (Y,{z}) by A2, FUNCT_2:def_2;
then  ( rng (X --> (Y --> z)) c= {(Y --> z)} & {(Y --> z)} c= Funcs (Y,{z}) ) by FUNCOP_1:13, ZFMISC_1:31;
then  rng (X --> (Y --> z)) c= Funcs (Y,{z}) by XBOOLE_1:1;
then A3: dom (uncurry (X --> (Y --> z))) = [:X,Y:] by A1, FUNCT_5:26;
A4: now__::_thesis:_for_x_being_set_st_x_in_[:X,Y:]_holds_
(uncurry_(X_-->_(Y_-->_z)))_._x_=_([:X,Y:]_-->_z)_._x
let x be set ; ::_thesis: ( x in [:X,Y:] implies (uncurry (X --> (Y --> z))) . x = ([:X,Y:] --> z) . x )
assume A5: x in [:X,Y:] ; ::_thesis: (uncurry (X --> (Y --> z))) . x = ([:X,Y:] --> z) . x
then consider y1 being set , g being Function, y2 being set  such that
A6: x = [y1,y2] and
A7: ( y1 in X & g = (X --> (Y --> z)) . y1 ) and
A8: y2 in dom g by A1, A3, FUNCT_5:def_2;
A9: g = Y --> z by A7, FUNCOP_1:7;
then  (Y --> z) . y2 = z by A2, A8, FUNCOP_1:7;
then  z = (uncurry (X --> (Y --> z))) . (y1,y2) by A1, A7, A8, A9, FUNCT_5:38;
hence  (uncurry (X --> (Y --> z))) . x = ([:X,Y:] --> z) . x by A5, A6, FUNCOP_1:7; ::_thesis: verum
end;
 dom ([:X,Y:] --> z) = [:X,Y:] by FUNCOP_1:13;
hence  uncurry (X --> (Y --> z)) = [:X,Y:] --> z by A3, A4, FUNCT_1:2; ::_thesis: uncurry' (X --> (Y --> z)) = [:Y,X:] --> z
then  ~ (uncurry (X --> (Y --> z))) = [:Y,X:] --> z by Th3;
hence  uncurry' (X --> (Y --> z)) = [:Y,X:] --> z by FUNCT_5:def_4; ::_thesis: verum
end;

theorem Th7: :: FUNCT_6:7
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
let x be set ; ::_thesis: 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) )
let f, g be Function; ::_thesis: ( x in dom f & g = f . x implies ( rng g c= rng (uncurry f) & rng g c= rng (uncurry' f) ) )
assume A1: ( x in dom f & g = f . x ) ; ::_thesis: ( rng g c= rng (uncurry f) & rng g c= rng (uncurry' f) )
thus  rng g c= rng (uncurry f) ::_thesis: rng g c= rng (uncurry' f)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng g or y in rng (uncurry f) )
assume  y in rng g ; ::_thesis: y in rng (uncurry f)
then  ex z being set st
( z in dom g & y = g . z ) by FUNCT_1:def_3;
hence  y in rng (uncurry f) by A1, FUNCT_5:38; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng g or y in rng (uncurry' f) )
assume  y in rng g ; ::_thesis: y in rng (uncurry' f)
then  ex z being set st
( z in dom g & y = g . z ) by FUNCT_1:def_3;
hence  y in rng (uncurry' f) by A1, FUNCT_5:39; ::_thesis: verum
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
let X be set ; ::_thesis: 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 )
let f be Function; ::_thesis: ( 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 )
 f in Funcs ((dom f),(rng f)) by FUNCT_2:def_2;
then  ( rng (X --> f) c= {f} & {f} c= Funcs ((dom f),(rng f)) ) by FUNCOP_1:13, ZFMISC_1:31;
then  ( dom (X --> f) = X & rng (X --> f) c= Funcs ((dom f),(rng f)) ) by FUNCOP_1:13, XBOOLE_1:1;
hence  ( 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 ) by FUNCT_5:26, FUNCT_5:41; ::_thesis: verum
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
let X be set ; ::_thesis: for f being Function st X <> {} holds
( rng (uncurry (X --> f)) = rng f & rng (uncurry' (X --> f)) = rng f )
let f be Function; ::_thesis: ( X <> {} implies ( rng (uncurry (X --> f)) = rng f & rng (uncurry' (X --> f)) = rng f ) )
set x = the Element of X;
assume A1: X <> {} ; ::_thesis: ( rng (uncurry (X --> f)) = rng f & rng (uncurry' (X --> f)) = rng f )
then  ( dom (X --> f) = X & (X --> f) . the Element of X = f ) by FUNCOP_1:7, FUNCOP_1:13;
hence  ( rng (uncurry (X --> f)) c= rng f & rng f c= rng (uncurry (X --> f)) & rng (uncurry' (X --> f)) c= rng f & rng f c= rng (uncurry' (X --> f)) ) by A1, Th7, Th8; :: according to XBOOLE_0:def_10 ::_thesis: verum
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
let X, Y, Z be set ; ::_thesis: 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))) )
let f be Function; ::_thesis: ( [:X,Y:] <> {} & f in Funcs ([:X,Y:],Z) implies ( curry f in Funcs (X,(Funcs (Y,Z))) & curry' f in Funcs (Y,(Funcs (X,Z))) ) )
assume A1: [:X,Y:] <> {} ; ::_thesis: ( not f in Funcs ([:X,Y:],Z) or ( curry f in Funcs (X,(Funcs (Y,Z))) & curry' f in Funcs (Y,(Funcs (X,Z))) ) )
assume  f in Funcs ([:X,Y:],Z) ; ::_thesis: ( curry f in Funcs (X,(Funcs (Y,Z))) & curry' f in Funcs (Y,(Funcs (X,Z))) )
then A2: ex g being Function st
( f = g & dom g = [:X,Y:] & rng g c= Z ) by FUNCT_2:def_2;
then  ( rng (curry f) c= Funcs (Y,(rng f)) & Funcs (Y,(rng f)) c= Funcs (Y,Z) ) by FUNCT_5:35, FUNCT_5:56;
then A3: rng (curry f) c= Funcs (Y,Z) by XBOOLE_1:1;
 ( rng (curry' f) c= Funcs (X,(rng f)) & Funcs (X,(rng f)) c= Funcs (X,Z) ) by A2, FUNCT_5:35, FUNCT_5:56;
then A4: rng (curry' f) c= Funcs (X,Z) by XBOOLE_1:1;
 ( dom (curry f) = X & dom (curry' f) = Y ) by A1, A2, FUNCT_5:24;
hence  ( curry f in Funcs (X,(Funcs (Y,Z))) & curry' f in Funcs (Y,(Funcs (X,Z))) ) by A3, A4, FUNCT_2:def_2; ::_thesis: verum
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
let X, Y, Z be set ; ::_thesis: 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) )
let f be Function; ::_thesis: ( f in Funcs (X,(Funcs (Y,Z))) implies ( uncurry f in Funcs ([:X,Y:],Z) & uncurry' f in Funcs ([:Y,X:],Z) ) )
assume  f in Funcs (X,(Funcs (Y,Z))) ; ::_thesis: ( uncurry f in Funcs ([:X,Y:],Z) & uncurry' f in Funcs ([:Y,X:],Z) )
then A1: ex g being Function st
( f = g & dom g = X & rng g c= Funcs (Y,Z) ) by FUNCT_2:def_2;
then A2: ( dom (uncurry f) = [:X,Y:] & dom (uncurry' f) = [:Y,X:] ) by FUNCT_5:26;
 ( rng (uncurry f) c= Z & rng (uncurry' f) c= Z ) by A1, FUNCT_5:41;
hence  ( uncurry f in Funcs ([:X,Y:],Z) & uncurry' f in Funcs ([:Y,X:],Z) ) by A2, FUNCT_2:def_2; ::_thesis: verum
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
let X, Y, Z, V1, V2 be set ; ::_thesis: 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)
let f be Function; ::_thesis: ( ( curry f in Funcs (X,(Funcs (Y,Z))) or curry' f in Funcs (Y,(Funcs (X,Z))) ) & dom f c= [:V1,V2:] implies f in Funcs ([:X,Y:],Z) )
assume  ( curry f in Funcs (X,(Funcs (Y,Z))) or curry' f in Funcs (Y,(Funcs (X,Z))) ) ; ::_thesis: ( not dom f c= [:V1,V2:] or f in Funcs ([:X,Y:],Z) )
then A1: ( uncurry (curry f) in Funcs ([:X,Y:],Z) or uncurry' (curry' f) in Funcs ([:X,Y:],Z) ) by Th11;
assume  dom f c= [:V1,V2:] ; ::_thesis: f in Funcs ([:X,Y:],Z)
hence  f in Funcs ([:X,Y:],Z) by A1, FUNCT_5:50; ::_thesis: verum
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
let X, Y, Z, V1, V2 be set ; ::_thesis: 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)))
let f be Function; ::_thesis: ( ( uncurry f in Funcs ([:X,Y:],Z) or uncurry' f in Funcs ([:Y,X:],Z) ) & rng f c= PFuncs (V1,V2) & dom f = X implies f in Funcs (X,(Funcs (Y,Z))) )
assume that
A1: ( uncurry f in Funcs ([:X,Y:],Z) or uncurry' f in Funcs ([:Y,X:],Z) ) and
A2: rng f c= PFuncs (V1,V2) and
A3: dom f = X ; ::_thesis: f in Funcs (X,(Funcs (Y,Z)))
A4: uncurry' f = ~ (uncurry f) by FUNCT_5:def_4;
A5: ( ex g being Function st
( uncurry f = g & dom g = [:X,Y:] & rng g c= Z ) or ex g being Function st
( uncurry' f = g & dom g = [:Y,X:] & rng g c= Z ) ) by A1, FUNCT_2:def_2;
then A6: dom (uncurry' f) = [:Y,X:] by A4, FUNCT_4:46;
 rng f c= Funcs (Y,Z)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in Funcs (Y,Z) )
assume A7: y in rng f ; ::_thesis: y in Funcs (Y,Z)
then consider x being set  such that
A8: x in dom f and
A9: y = f . x by FUNCT_1:def_3;
 ex g being Function st
( y = g & dom g c= V1 & rng g c= V2 ) by A2, A7, PARTFUN1:def_3;
then reconsider h = y as Function ;
A10: dom h = Y
proof
thus  dom h c= Y :: according to XBOOLE_0:def_10 ::_thesis: Y c= dom h
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in dom h or z in Y )
assume  z in dom h ; ::_thesis: z in Y
then  [z,x] in dom (uncurry' f) by A8, A9, FUNCT_5:39;
hence  z in Y by A6, ZFMISC_1:87; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Y or z in dom h )
assume  z in Y ; ::_thesis: z in dom h
then  [z,x] in [:Y,X:] by A3, A8, ZFMISC_1:87;
then  [x,z] in dom (uncurry f) by A4, A6, FUNCT_4:42;
then consider y1 being set , f1 being Function, y2 being set  such that
A11: [x,z] = [y1,y2] and
 y1 in dom f and
A12: ( f1 = f . y1 & y2 in dom f1 ) by FUNCT_5:def_2;
 x = y1 by A11, XTUPLE_0:1;
hence  z in dom h by A9, A11, A12, XTUPLE_0:1; ::_thesis: verum
end;
 rng h c= Z
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng h or z in Z )
assume  z in rng h ; ::_thesis: z in Z
then  ex y1 being set st
( y1 in dom h & z = h . y1 ) by FUNCT_1:def_3;
then  ( z in rng (uncurry f) & z in rng (uncurry' f) ) by A8, A9, FUNCT_5:38, FUNCT_5:39;
hence  z in Z by A5; ::_thesis: verum
end;
hence  y in Funcs (Y,Z) by A10, FUNCT_2:def_2; ::_thesis: verum
end;
hence  f in Funcs (X,(Funcs (Y,Z))) by A3, FUNCT_2:def_2; ::_thesis: verum
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
let X, Y, Z be set ; ::_thesis: 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))) )
let f be Function; ::_thesis: ( f in PFuncs ([:X,Y:],Z) implies ( curry f in PFuncs (X,(PFuncs (Y,Z))) & curry' f in PFuncs (Y,(PFuncs (X,Z))) ) )
assume  f in PFuncs ([:X,Y:],Z) ; ::_thesis: ( curry f in PFuncs (X,(PFuncs (Y,Z))) & curry' f in PFuncs (Y,(PFuncs (X,Z))) )
then A1: ex g being Function st
( f = g & dom g c= [:X,Y:] & rng g c= Z ) by PARTFUN1:def_3;
then  ( proj1 [:X,Y:] c= X & proj1 (dom f) c= proj1 [:X,Y:] ) by FUNCT_5:10, XTUPLE_0:8;
then  proj1 (dom f) c= X by XBOOLE_1:1;
then A2: PFuncs ((proj1 (dom f)),(rng f)) c= PFuncs (X,Z) by A1, PARTFUN1:50;
 ( proj2 [:X,Y:] c= Y & proj2 (dom f) c= proj2 [:X,Y:] ) by A1, FUNCT_5:10, XTUPLE_0:9;
then  proj2 (dom f) c= Y by XBOOLE_1:1;
then  ( rng (curry f) c= PFuncs ((proj2 (dom f)),(rng f)) & PFuncs ((proj2 (dom f)),(rng f)) c= PFuncs (Y,Z) ) by A1, FUNCT_5:36, PARTFUN1:50;
then A3: rng (curry f) c= PFuncs (Y,Z) by XBOOLE_1:1;
 rng (curry' f) c= PFuncs ((proj1 (dom f)),(rng f)) by FUNCT_5:36;
then A4: rng (curry' f) c= PFuncs (X,Z) by A2, XBOOLE_1:1;
 ( dom (curry f) c= X & dom (curry' f) c= Y ) by A1, FUNCT_5:25;
hence  ( curry f in PFuncs (X,(PFuncs (Y,Z))) & curry' f in PFuncs (Y,(PFuncs (X,Z))) ) by A3, A4, PARTFUN1:def_3; ::_thesis: verum
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
let X, Y, Z be set ; ::_thesis: 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) )
let f be Function; ::_thesis: ( f in PFuncs (X,(PFuncs (Y,Z))) implies ( uncurry f in PFuncs ([:X,Y:],Z) & uncurry' f in PFuncs ([:Y,X:],Z) ) )
assume  f in PFuncs (X,(PFuncs (Y,Z))) ; ::_thesis: ( uncurry f in PFuncs ([:X,Y:],Z) & uncurry' f in PFuncs ([:Y,X:],Z) )
then A1: ex g being Function st
( f = g & dom g c= X & rng g c= PFuncs (Y,Z) ) by PARTFUN1:def_3;
then  ( dom (uncurry f) c= [:(dom f),Y:] & [:(dom f),Y:] c= [:X,Y:] ) by FUNCT_5:37, ZFMISC_1:96;
then A2: dom (uncurry f) c= [:X,Y:] by XBOOLE_1:1;
 ( dom (uncurry' f) c= [:Y,(dom f):] & [:Y,(dom f):] c= [:Y,X:] ) by A1, FUNCT_5:37, ZFMISC_1:96;
then A3: dom (uncurry' f) c= [:Y,X:] by XBOOLE_1:1;
 ( rng (uncurry f) c= Z & rng (uncurry' f) c= Z ) by A1, FUNCT_5:40;
hence  ( uncurry f in PFuncs ([:X,Y:],Z) & uncurry' f in PFuncs ([:Y,X:],Z) ) by A2, A3, PARTFUN1:def_3; ::_thesis: verum
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
let X, Y, Z, V1, V2 be set ; ::_thesis: 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)
let f be Function; ::_thesis: ( ( curry f in PFuncs (X,(PFuncs (Y,Z))) or curry' f in PFuncs (Y,(PFuncs (X,Z))) ) & dom f c= [:V1,V2:] implies f in PFuncs ([:X,Y:],Z) )
assume  ( curry f in PFuncs (X,(PFuncs (Y,Z))) or curry' f in PFuncs (Y,(PFuncs (X,Z))) ) ; ::_thesis: ( not dom f c= [:V1,V2:] or f in PFuncs ([:X,Y:],Z) )
then A1: ( uncurry (curry f) in PFuncs ([:X,Y:],Z) or uncurry' (curry' f) in PFuncs ([:X,Y:],Z) ) by Th15;
assume  dom f c= [:V1,V2:] ; ::_thesis: f in PFuncs ([:X,Y:],Z)
hence  f in PFuncs ([:X,Y:],Z) by A1, FUNCT_5:50; ::_thesis: verum
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
let X, Y, Z, V1, V2 be set ; ::_thesis: 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)))
let f be Function; ::_thesis: ( ( 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 implies f in PFuncs (X,(PFuncs (Y,Z))) )
assume that
A1: ( uncurry f in PFuncs ([:X,Y:],Z) or uncurry' f in PFuncs ([:Y,X:],Z) ) and
A2: rng f c= PFuncs (V1,V2) and
A3: dom f c= X ; ::_thesis: f in PFuncs (X,(PFuncs (Y,Z)))
A4: ( ex g being Function st
( uncurry f = g & dom g c= [:X,Y:] & rng g c= Z ) or ex g being Function st
( uncurry' f = g & dom g c= [:Y,X:] & rng g c= Z ) ) by A1, PARTFUN1:def_3;
 uncurry' f = ~ (uncurry f) by FUNCT_5:def_4;
then A5: dom (uncurry' f) c= [:Y,X:] by A4, FUNCT_4:45;
 rng f c= PFuncs (Y,Z)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in PFuncs (Y,Z) )
assume A6: y in rng f ; ::_thesis: y in PFuncs (Y,Z)
then consider x being set  such that
A7: ( x in dom f & y = f . x ) by FUNCT_1:def_3;
 ex g being Function st
( y = g & dom g c= V1 & rng g c= V2 ) by A2, A6, PARTFUN1:def_3;
then reconsider h = y as Function ;
A8: rng h c= Z
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng h or z in Z )
assume  z in rng h ; ::_thesis: z in Z
then  ex y1 being set st
( y1 in dom h & z = h . y1 ) by FUNCT_1:def_3;
then  ( z in rng (uncurry f) & z in rng (uncurry' f) ) by A7, FUNCT_5:38, FUNCT_5:39;
hence  z in Z by A4; ::_thesis: verum
end;
 dom h c= Y
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in dom h or z in Y )
assume  z in dom h ; ::_thesis: z in Y
then  [z,x] in dom (uncurry' f) by A7, FUNCT_5:39;
hence  z in Y by A5, ZFMISC_1:87; ::_thesis: verum
end;
hence  y in PFuncs (Y,Z) by A8, PARTFUN1:def_3; ::_thesis: verum
end;
hence  f in PFuncs (X,(PFuncs (Y,Z))) by A3, PARTFUN1:def_3; ::_thesis: verum
end;

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 & 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
defpred S1[ set ] means $1 is Function;
 ex Y being set st
for x being set holds
( x in Y iff ( x in X & S1[x] ) ) from XBOOLE_0:sch_1();
hence  ex b1 being set st
for x being set holds
( x in b1 iff ( x in X & x is Function ) ) ; ::_thesis: verum
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
defpred S1[ set ] means ( $1 in X & $1 is Function );
let X1, X2 be set ; ::_thesis: ( ( for x being set holds
( x in X1 iff ( x in X & x is Function ) ) ) & ( for x being set holds
( x in X2 iff ( x in X & x is Function ) ) ) implies X1 = X2 )
assume that
A1: for x being set holds
( x in X1 iff S1[x] ) and
A2: for x being set holds
( x in X2 iff S1[x] ) ; ::_thesis: X1 = X2
thus  X1 = X2 from XBOOLE_0:sch_2(A1, A2); ::_thesis: verum
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 Th18: :: FUNCT_6:18
for X being set holds SubFuncs X c= X
proof
let X be set ; ::_thesis: SubFuncs X c= X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in SubFuncs X or x in X )
thus  ( not x in SubFuncs X or x in X ) by Def1; ::_thesis: verum
end;

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 & f . x is Function ) )
proof
let x be set ; ::_thesis: for f being Function holds
( x in f " (SubFuncs (rng f)) iff ( x in dom f & f . x is Function ) )
let f be Function; ::_thesis: ( x in f " (SubFuncs (rng f)) iff ( x in dom f & f . x is Function ) )
 ( ( f . x in rng f & f . x is Function ) iff f . x in SubFuncs (rng f) ) by Def1;
hence  ( x in f " (SubFuncs (rng f)) iff ( x in dom f & f . x is Function ) ) by FUNCT_1:def_3, FUNCT_1:def_7; ::_thesis: verum
end;

Lm1:  for X being set st ( for x being set st x in X holds
x is Function ) holds
SubFuncs X = X
proof
let X be set ; ::_thesis: ( ( for x being set st x in X holds
x is Function ) implies SubFuncs X = X )
assume  for x being set st x in X holds
x is Function ; ::_thesis: SubFuncs X = X
then  for x being set holds
( x in X iff ( x in X & x is Function ) ) ;
hence  SubFuncs X = X by Def1; ::_thesis: verum
end;

theorem :: FUNCT_6:20
for f, g, h being Function holds
( SubFuncs {} = {} & SubFuncs {f} = {f} & SubFuncs {f,g} = {f,g} & SubFuncs {f,g,h} = {f,g,h} )
proof
let f, g, h be Function; ::_thesis: ( SubFuncs {} = {} & SubFuncs {f} = {f} & SubFuncs {f,g} = {f,g} & SubFuncs {f,g,h} = {f,g,h} )
thus  SubFuncs {} = {} by Th18, XBOOLE_1:3; ::_thesis: ( SubFuncs {f} = {f} & SubFuncs {f,g} = {f,g} & SubFuncs {f,g,h} = {f,g,h} )
 for x being set st x in {f} holds
x is Function ;
hence  SubFuncs {f} = {f} by Lm1; ::_thesis: ( SubFuncs {f,g} = {f,g} & SubFuncs {f,g,h} = {f,g,h} )
 for x being set st x in {f,g} holds
x is Function ;
hence  SubFuncs {f,g} = {f,g} by Lm1; ::_thesis: SubFuncs {f,g,h} = {f,g,h}
 for x being set st x in {f,g,h} holds
x is Function by ENUMSET1:def_1;
hence  SubFuncs {f,g,h} = {f,g,h} by Lm1; ::_thesis: verum
end;

theorem :: FUNCT_6:21
for Y, X being set st Y c= SubFuncs X holds
SubFuncs Y = Y
proof
let Y, X be set ; ::_thesis: ( Y c= SubFuncs X implies SubFuncs Y = Y )
assume  Y c= SubFuncs X ; ::_thesis: SubFuncs Y = Y
then  for x being set st x in Y holds
x is Function by Def1;
hence  SubFuncs Y = Y by Lm1; ::_thesis: verum
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
deffunc H1( set ) ->  set = proj1 (f . $1);
 ex F being Function st
( dom F = f " (SubFuncs (rng f)) & ( for x being set st x in f " (SubFuncs (rng f)) holds
F . x = H1(x) ) ) from FUNCT_1:sch_3();
hence  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) ) ) ; ::_thesis: verum
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
let f1, f2 be Function; ::_thesis: ( dom f1 = f " (SubFuncs (rng f)) & ( for x being set st x in f " (SubFuncs (rng f)) holds
f1 . x = proj1 (f . x) ) & dom f2 = f " (SubFuncs (rng f)) & ( for x being set st x in f " (SubFuncs (rng f)) holds
f2 . x = proj1 (f . x) ) implies f1 = f2 )
assume that
A1: dom f1 = f " (SubFuncs (rng f)) and
A2: for x being set st x in f " (SubFuncs (rng f)) holds
f1 . x = proj1 (f . x) and
A3: dom f2 = f " (SubFuncs (rng f)) and
A4: for x being set st x in f " (SubFuncs (rng f)) holds
f2 . x = proj1 (f . x) ; ::_thesis: f1 = f2
now__::_thesis:_for_x_being_set_st_x_in_f_"_(SubFuncs_(rng_f))_holds_
f1_._x_=_f2_._x
let x be set ; ::_thesis: ( x in f " (SubFuncs (rng f)) implies f1 . x = f2 . x )
assume A5: x in f " (SubFuncs (rng f)) ; ::_thesis: f1 . x = f2 . x
then  f1 . x = proj1 (f . x) by A2;
hence  f1 . x = f2 . x by A4, A5; ::_thesis: verum
end;
hence  f1 = f2 by A1, A3, FUNCT_1:2; ::_thesis: verum
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
deffunc H1( set ) ->  set = proj2 (f . $1);
 ex F being Function st
( dom F = f " (SubFuncs (rng f)) & ( for x being set st x in f " (SubFuncs (rng f)) holds
F . x = H1(x) ) ) from FUNCT_1:sch_3();
hence  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) ) ) ; ::_thesis: verum
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
let f1, f2 be Function; ::_thesis: ( dom f1 = f " (SubFuncs (rng f)) & ( for x being set st x in f " (SubFuncs (rng f)) holds
f1 . x = proj2 (f . x) ) & dom f2 = f " (SubFuncs (rng f)) & ( for x being set st x in f " (SubFuncs (rng f)) holds
f2 . x = proj2 (f . x) ) implies f1 = f2 )
assume that
A6: dom f1 = f " (SubFuncs (rng f)) and
A7: for x being set st x in f " (SubFuncs (rng f)) holds
f1 . x = proj2 (f . x) and
A8: dom f2 = f " (SubFuncs (rng f)) and
A9: for x being set st x in f " (SubFuncs (rng f)) holds
f2 . x = proj2 (f . x) ; ::_thesis: f1 = f2
now__::_thesis:_for_x_being_set_st_x_in_f_"_(SubFuncs_(rng_f))_holds_
f1_._x_=_f2_._x
let x be set ; ::_thesis: ( x in f " (SubFuncs (rng f)) implies f1 . x = f2 . x )
assume A10: x in f " (SubFuncs (rng f)) ; ::_thesis: f1 . x = f2 . x
then  f1 . x = proj2 (f . x) by A7;
hence  f1 . x = f2 . x by A9, A10; ::_thesis: verum
end;
hence  f1 = f2 by A6, A8, FUNCT_1:2; ::_thesis: verum
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 Th22: :: FUNCT_6:22
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
let x be set ; ::_thesis: 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 )
let f, g be Function; ::_thesis: ( x in dom f & g = f . x implies ( x in dom (doms f) & (doms f) . x = dom g & x in dom (rngs f) & (rngs f) . x = rng g ) )
assume that
A1: x in dom f and
A2: g = f . x ; ::_thesis: ( x in dom (doms f) & (doms f) . x = dom g & x in dom (rngs f) & (rngs f) . x = rng g )
 g in rng f by A1, A2, FUNCT_1:def_3;
then  g in SubFuncs (rng f) by Def1;
then  x in f " (SubFuncs (rng f)) by A1, A2, FUNCT_1:def_7;
hence  ( x in dom (doms f) & (doms f) . x = dom g & x in dom (rngs f) & (rngs f) . x = rng g ) by A2, Def2, Def3; ::_thesis: verum
end;

theorem :: FUNCT_6:23
( doms {} = {} & rngs {} = {} )
proof
 ( dom (doms {}) = {} " (SubFuncs {}) & dom (rngs {}) = {} " (SubFuncs {}) ) by Def2, Def3, RELAT_1:38;
hence  ( doms {} = {} & rngs {} = {} ) ; ::_thesis: verum
end;

theorem Th24: :: 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
let X be set ; ::_thesis: for f being Function holds
( doms (X --> f) = X --> (dom f) & rngs (X --> f) = X --> (rng f) )
let f be Function; ::_thesis: ( doms (X --> f) = X --> (dom f) & rngs (X --> f) = X --> (rng f) )
A1: ( dom (X --> (dom f)) = X & dom (doms (X --> f)) = (X --> f) " (SubFuncs (rng (X --> f))) ) by Def2, FUNCOP_1:13;
A2: rng (X --> f) c= {f} by FUNCOP_1:13;
A3: SubFuncs (rng (X --> f)) = rng (X --> f)
proof
thus  SubFuncs (rng (X --> f)) c= rng (X --> f) by Th18; :: according to XBOOLE_0:def_10 ::_thesis: rng (X --> f) c= SubFuncs (rng (X --> f))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (X --> f) or x in SubFuncs (rng (X --> f)) )
assume  x in rng (X --> f) ; ::_thesis: x in SubFuncs (rng (X --> f))
hence  x in SubFuncs (rng (X --> f)) by A2, Def1; ::_thesis: verum
end;
A4: ( dom (X --> f) = X & (X --> f) " (rng (X --> f)) = dom (X --> f) ) by FUNCOP_1:13, RELAT_1:134;
now__::_thesis:_for_x_being_set_st_x_in_X_holds_
(doms_(X_-->_f))_._x_=_(X_-->_(dom_f))_._x
let x be set ; ::_thesis: ( x in X implies (doms (X --> f)) . x = (X --> (dom f)) . x )
assume A5: x in X ; ::_thesis: (doms (X --> f)) . x = (X --> (dom f)) . x
then  ( (X --> f) . x = f & (X --> (dom f)) . x = dom f ) by FUNCOP_1:7;
hence  (doms (X --> f)) . x = (X --> (dom f)) . x by A4, A3, A5, Def2; ::_thesis: verum
end;
hence  doms (X --> f) = X --> (dom f) by A1, A4, A3, FUNCT_1:2; ::_thesis: rngs (X --> f) = X --> (rng f)
A6: now__::_thesis:_for_x_being_set_st_x_in_X_holds_
(rngs_(X_-->_f))_._x_=_(X_-->_(rng_f))_._x
let x be set ; ::_thesis: ( x in X implies (rngs (X --> f)) . x = (X --> (rng f)) . x )
assume A7: x in X ; ::_thesis: (rngs (X --> f)) . x = (X --> (rng f)) . x
then  ( (X --> f) . x = f & (X --> (rng f)) . x = rng f ) by FUNCOP_1:7;
hence  (rngs (X --> f)) . x = (X --> (rng f)) . x by A4, A3, A7, Def3; ::_thesis: verum
end;
 ( dom (X --> (rng f)) = X & dom (rngs (X --> f)) = (X --> f) " (SubFuncs (rng (X --> f))) ) by Def3, FUNCOP_1:13;
hence  rngs (X --> f) = X --> (rng f) by A4, A3, A6, FUNCT_1:2; ::_thesis: verum
end;

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 )
proof
let x be set ; ::_thesis: 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 )
let f be Function; ::_thesis: ( f <> {} implies ( x in meet f iff for y being set st y in dom f holds
x in f . y ) )
assume A1: f <> {} ; ::_thesis: ( x in meet f iff for y being set st y in dom f holds
x in f . y )
thus  ( x in meet f implies for y being set st y in dom f holds
x in f . y ) ::_thesis: ( ( for y being set st y in dom f holds
x in f . y ) implies x in meet f )
proof
assume A2: x in meet f ; ::_thesis: for y being set st y in dom f holds
x in f . y
let y be set ; ::_thesis: ( y in dom f implies x in f . y )
assume  y in dom f ; ::_thesis: x in f . y
then  f . y in rng f by FUNCT_1:def_3;
then  meet f c= f . y by SETFAM_1:3;
hence  x in f . y by A2; ::_thesis: verum
end;
assume A3: for y being set st y in dom f holds
x in f . y ; ::_thesis: x in meet f
now__::_thesis:_for_z_being_set_st_z_in_rng_f_holds_
x_in_z
let z be set ; ::_thesis: ( z in rng f implies x in z )
assume  z in rng f ; ::_thesis: x in z
then  ex y being set st
( y in dom f & z = f . y ) by FUNCT_1:def_3;
hence  x in z by A3; ::_thesis: verum
end;
hence  x in meet f by A1, SETFAM_1:def_1; ::_thesis: verum
end;

theorem :: FUNCT_6:26
for Y being set holds
( Union ({} --> Y) = {} & meet ({} --> Y) = {} )
proof
let Y be set ; ::_thesis: ( Union ({} --> Y) = {} & meet ({} --> Y) = {} )
 union (rng ({} --> Y)) = {} by ZFMISC_1:2;
hence  ( Union ({} --> Y) = {} & meet ({} --> Y) = {} ) by CARD_3:def_4, SETFAM_1:def_1; ::_thesis: verum
end;

theorem Th27: :: FUNCT_6:27
for X, Y being set st X <> {} holds
( Union (X --> Y) = Y & meet (X --> Y) = Y )
proof
let X, Y be set ; ::_thesis: ( X <> {} implies ( Union (X --> Y) = Y & meet (X --> Y) = Y ) )
assume  X <> {} ; ::_thesis: ( Union (X --> Y) = Y & meet (X --> Y) = Y )
then A1: rng (X --> Y) = {Y} by FUNCOP_1:8;
then  union (rng (X --> Y)) = Y by ZFMISC_1:25;
hence  ( Union (X --> Y) = Y & meet (X --> Y) = Y ) by A1, CARD_3:def_4, SETFAM_1:10; ::_thesis: verum
end;

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 & y in dom f holds
(X --> f) .. (x,y) = f . y
proof
let x, X, y be set ; ::_thesis: for f being Function st x in X & y in dom f holds
(X --> f) .. (x,y) = f . y
let f be Function; ::_thesis: ( x in X & y in dom f implies (X --> f) .. (x,y) = f . y )
A1: ( x in X implies (X --> f) . x = f ) by FUNCOP_1:7;
 dom (X --> f) = X by FUNCOP_1:13;
hence  ( x in X & y in dom f implies (X --> f) .. (x,y) = f . y ) by A1, FUNCT_5:38; ::_thesis: verum
end;

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) & rng <:f:> c= product (rngs f) )
proof
let f be Function; ::_thesis: ( dom <:f:> = meet (doms f) & rng <:f:> c= product (rngs f) )
set f9 = (uncurry' f) | [:(meet (doms f)),(dom f):];
 dom ((uncurry' f) | [:(meet (doms f)),(dom f):]) c= [:(meet (doms f)),(dom f):] by RELAT_1:58;
hence A1: dom <:f:> c= meet (doms f) by FUNCT_5:25; :: according to XBOOLE_0:def_10 ::_thesis: ( meet (doms f) c= dom <:f:> & rng <:f:> c= product (rngs f) )
A2: dom (doms f) = f " (SubFuncs (rng f)) by Def2;
thus  meet (doms f) c= dom <:f:> ::_thesis: rng <:f:> c= product (rngs f)
proof
set y = the Element of rng (doms f);
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet (doms f) or x in dom <:f:> )
assume A3: x in meet (doms f) ; ::_thesis: x in dom <:f:>
then A4: rng (doms f) <> {} by SETFAM_1:def_1;
then A5: x in the Element of rng (doms f) by A3, SETFAM_1:def_1;
consider z being set  such that
A6: z in dom (doms f) and
A7: the Element of rng (doms f) = (doms f) . z by A4, FUNCT_1:def_3;
 f . z in SubFuncs (rng f) by A2, A6, FUNCT_1:def_7;
then reconsider g = f . z as Function by Def1;
A8: z in dom f by A2, A6, FUNCT_1:def_7;
then  the Element of rng (doms f) = dom g by A7, Th22;
then A9: [x,z] in dom (uncurry' f) by A8, A5, FUNCT_5:39;
 [x,z] in [:(meet (doms f)),(dom f):] by A3, A8, ZFMISC_1:87;
then  [x,z] in (dom (uncurry' f)) /\ [:(meet (doms f)),(dom f):] by A9, XBOOLE_0:def_4;
then  [x,z] in dom ((uncurry' f) | [:(meet (doms f)),(dom f):]) by RELAT_1:61;
then  x in proj1 (dom ((uncurry' f) | [:(meet (doms f)),(dom f):])) by XTUPLE_0:def_12;
hence  x in dom <:f:> by FUNCT_5:def_1; ::_thesis: verum
end;
A10: dom (rngs f) = f " (SubFuncs (rng f)) by Def3;
thus  rng <:f:> c= product (rngs f) ::_thesis: verum
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng <:f:> or y in product (rngs f) )
A11: dom ((uncurry' f) | [:(meet (doms f)),(dom f):]) = (dom (uncurry' f)) /\ [:(meet (doms f)),(dom f):] by RELAT_1:61;
A12: uncurry' f = ~ (uncurry f) by FUNCT_5:def_4;
assume  y in rng <:f:> ; ::_thesis: y in product (rngs f)
then consider x being set  such that
A13: x in dom <:f:> and
A14: y = <:f:> . x by FUNCT_1:def_3;
reconsider g = y as Function by A13, A14, FUNCT_5:30;
A15: dom g = proj2 ((dom ((uncurry' f) | [:(meet (doms f)),(dom f):])) /\ [:{x},(proj2 (dom ((uncurry' f) | [:(meet (doms f)),(dom f):]))):]) by A13, A14, FUNCT_5:31;
A16: dom g = dom (rngs f)
proof
thus  dom g c= dom (rngs f) :: according to XBOOLE_0:def_10 ::_thesis: dom (rngs f) c= dom g
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in dom g or z in dom (rngs f) )
assume  z in dom g ; ::_thesis: z in dom (rngs f)
then  [x,z] in dom ((uncurry' f) | [:(meet (doms f)),(dom f):]) by A13, A14, FUNCT_5:31;
then  [x,z] in dom (uncurry' f) by A11, XBOOLE_0:def_4;
then  [z,x] in dom (uncurry f) by A12, FUNCT_4:42;
then consider y1 being set , h being Function, y2 being set  such that
A17: [z,x] = [y1,y2] and
A18: y1 in dom f and
A19: h = f . y1 and
 y2 in dom h by FUNCT_5:def_2;
A20: z = y1 by A17, XTUPLE_0:1;
 h in rng f by A18, A19, FUNCT_1:def_3;
then  f . z in SubFuncs (rng f) by A19, A20, Def1;
hence  z in dom (rngs f) by A10, A18, A20, FUNCT_1:def_7; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in dom (rngs f) or z in dom g )
A21: x in {x} by TARSKI:def_1;
assume A22: z in dom (rngs f) ; ::_thesis: z in dom g
then  f . z in SubFuncs (rng f) by A10, FUNCT_1:def_7;
then reconsider h = f . z as Function by Def1;
A23: z in dom f by A10, A22, FUNCT_1:def_7;
then  dom h = (doms f) . z by Th22;
then  dom h in rng (doms f) by A2, A10, A22, FUNCT_1:def_3;
then  x in dom h by A1, A13, SETFAM_1:def_1;
then  [z,x] in dom (uncurry f) by A23, FUNCT_5:def_2;
then A24: [x,z] in dom (uncurry' f) by A12, FUNCT_4:42;
 [x,z] in [:(meet (doms f)),(dom f):] by A1, A13, A23, ZFMISC_1:87;
then A25: [x,z] in dom ((uncurry' f) | [:(meet (doms f)),(dom f):]) by A11, A24, XBOOLE_0:def_4;
then  z in proj2 (dom ((uncurry' f) | [:(meet (doms f)),(dom f):])) by XTUPLE_0:def_13;
then  [x,z] in [:{x},(proj2 (dom ((uncurry' f) | [:(meet (doms f)),(dom f):]))):] by A21, ZFMISC_1:87;
then  [x,z] in (dom ((uncurry' f) | [:(meet (doms f)),(dom f):])) /\ [:{x},(proj2 (dom ((uncurry' f) | [:(meet (doms f)),(dom f):]))):] by A25, XBOOLE_0:def_4;
hence  z in dom g by A15, XTUPLE_0:def_13; ::_thesis: verum
end;
now__::_thesis:_for_z_being_set_st_z_in_dom_(rngs_f)_holds_
g_._z_in_(rngs_f)_._z
let z be set ; ::_thesis: ( z in dom (rngs f) implies g . z in (rngs f) . z )
assume A26: z in dom (rngs f) ; ::_thesis: g . z in (rngs f) . z
then  f . z in SubFuncs (rng f) by A10, FUNCT_1:def_7;
then reconsider h = f . z as Function by Def1;
A27: z in dom f by A10, A26, FUNCT_1:def_7;
then  dom h = (doms f) . z by Th22;
then  dom h in rng (doms f) by A2, A10, A26, FUNCT_1:def_3;
then A28: x in dom h by A1, A13, SETFAM_1:def_1;
then A29: h . x in rng h by FUNCT_1:def_3;
 ( g . z = ((uncurry' f) | [:(meet (doms f)),(dom f):]) . (x,z) & [x,z] in dom ((uncurry' f) | [:(meet (doms f)),(dom f):]) ) by A13, A14, A16, A26, FUNCT_5:31;
then  (uncurry' f) . (x,z) = g . z by FUNCT_1:47;
then  g . z = h . x by A27, A28, FUNCT_5:39;
hence  g . z in (rngs f) . z by A27, A29, Th22; ::_thesis: verum
end;
hence  y in product (rngs f) by A16, CARD_3:def_5; ::_thesis: verum
end;
end;

theorem Th30: :: FUNCT_6:30
for x being set
for f being Function st x in dom <:f:> holds
<:f:> . x is Function
proof
let x be set ; ::_thesis: for f being Function st x in dom <:f:> holds
<:f:> . x is Function
let f be Function; ::_thesis: ( x in dom <:f:> implies <:f:> . x is Function )
assume  x in dom <:f:> ; ::_thesis: <:f:> . x is Function
then A1: <:f:> . x in rng <:f:> by FUNCT_1:def_3;
 rng <:f:> c= product (rngs f) by Th29;
then  ex g being Function st
( <:f:> . x = g & dom g = dom (rngs f) & ( for x being set st x in dom (rngs f) holds
g . x in (rngs f) . x ) ) by A1, CARD_3:def_5;
hence  <:f:> . x is Function ; ::_thesis: verum
end;

theorem Th31: :: FUNCT_6:31
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
let x be set ; ::_thesis: 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) ) ) )
let f, g be Function; ::_thesis: ( x in dom <:f:> & g = <:f:> . x implies ( 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) ) ) ) )
A1: ( rng <:f:> c= product (rngs f) & dom (rngs f) = f " (SubFuncs (rng f)) ) by Def3, Th29;
assume A2: ( x in dom <:f:> & g = <:f:> . x ) ; ::_thesis: ( 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) ) ) )
then  g in rng <:f:> by FUNCT_1:def_3;
hence  dom g = f " (SubFuncs (rng f)) by A1, CARD_3:9; ::_thesis: for y being set st y in dom g holds
( [y,x] in dom (uncurry f) & g . y = (uncurry f) . (y,x) )
let y be set ; ::_thesis: ( y in dom g implies ( [y,x] in dom (uncurry f) & g . y = (uncurry f) . (y,x) ) )
assume A3: y in dom g ; ::_thesis: ( [y,x] in dom (uncurry f) & g . y = (uncurry f) . (y,x) )
A4: [x,y] in dom ((uncurry' f) | [:(meet (doms f)),(dom f):]) by A2, A3, FUNCT_5:31;
then  [x,y] in (dom (uncurry' f)) /\ [:(meet (doms f)),(dom f):] by RELAT_1:61;
then A5: [x,y] in dom (uncurry' f) by XBOOLE_0:def_4;
 g . y = ((uncurry' f) | [:(meet (doms f)),(dom f):]) . (x,y) by A2, A3, FUNCT_5:31;
then A6: g . y = (uncurry' f) . (x,y) by A4, FUNCT_1:47;
 ~ (uncurry f) = uncurry' f by FUNCT_5:def_4;
hence  ( [y,x] in dom (uncurry f) & g . y = (uncurry f) . (y,x) ) by A6, A5, FUNCT_4:42, FUNCT_4:43; ::_thesis: verum
end;

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
proof
let x be set ; ::_thesis: for f being Function st x in dom <:f:> holds
for g being Function st g in rng f holds
x in dom g
let f be Function; ::_thesis: ( x in dom <:f:> implies for g being Function st g in rng f holds
x in dom g )
assume A1: x in dom <:f:> ; ::_thesis: for g being Function st g in rng f holds
x in dom g
let g be Function; ::_thesis: ( g in rng f implies x in dom g )
assume  g in rng f ; ::_thesis: x in dom g
then consider y being set  such that
A2: ( y in dom f & g = f . y ) by FUNCT_1:def_3;
 ( y in dom (doms f) & (doms f) . y = dom g ) by A2, Th22;
then  dom g in rng (doms f) by FUNCT_1:def_3;
then A3: meet (rng (doms f)) c= dom g by SETFAM_1:3;
 meet (doms f) = dom <:f:> by Th29;
hence  x in dom g by A1, A3; ::_thesis: verum
end;

theorem :: FUNCT_6:33
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
let x be set ; ::_thesis: 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:>
let g, f be Function; ::_thesis: ( g in rng f & ( for g being Function st g in rng f holds
x in dom g ) implies x in dom <:f:> )
assume that
A1: g in rng f and
A2: for g being Function st g in rng f holds
x in dom g ; ::_thesis: x in dom <:f:>
 ex y being set st
( y in dom f & g = f . y ) by A1, FUNCT_1:def_3;
then A3: doms f <> {} by Th22, RELAT_1:38;
A4: now__::_thesis:_for_y_being_set_st_y_in_dom_(doms_f)_holds_
x_in_(doms_f)_._y
let y be set ; ::_thesis: ( y in dom (doms f) implies x in (doms f) . y )
assume  y in dom (doms f) ; ::_thesis: x in (doms f) . y
then A5: y in f " (SubFuncs (rng f)) by Def2;
then  f . y in SubFuncs (rng f) by FUNCT_1:def_7;
then reconsider g = f . y as Function by Def1;
A6: y in dom f by A5, FUNCT_1:def_7;
then  g in rng f by FUNCT_1:def_3;
then  x in dom g by A2;
hence  x in (doms f) . y by A6, Th22; ::_thesis: verum
end;
 dom <:f:> = meet (doms f) by Th29;
hence  x in dom <:f:> by A3, A4, Th25; ::_thesis: verum
end;

theorem Th34: :: FUNCT_6:34
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
let x, y be set ; ::_thesis: 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
let f, g, h be Function; ::_thesis: ( x in dom f & g = f . x & y in dom <:f:> & h = <:f:> . y implies g . y = h . x )
assume that
A1: ( x in dom f & g = f . x ) and
A2: y in dom <:f:> and
A3: h = <:f:> . y ; ::_thesis: g . y = h . x
 dom h = f " (SubFuncs (rng f)) by A2, A3, Th31;
then  x in dom h by A1, Th19;
then A4: h . x = (uncurry f) . (x,y) by A2, A3, Th31;
 g in rng f by A1, FUNCT_1:def_3;
then  y in dom g by A2, Th32;
hence  g . y = h . x by A1, A4, FUNCT_5:38; ::_thesis: verum
end;

theorem :: FUNCT_6:35
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
let x, y be set ; ::_thesis: for f being Function st x in dom f & f . x is Function & y in dom <:f:> holds
f .. (x,y) = <:f:> .. (y,x)
let f be Function; ::_thesis: ( x in dom f & f . x is Function & y in dom <:f:> implies f .. (x,y) = <:f:> .. (y,x) )
assume that
A1: x in dom f and
A2: f . x is Function and
A3: y in dom <:f:> ; ::_thesis: f .. (x,y) = <:f:> .. (y,x)
reconsider g = f . x, h = <:f:> . y as Function by A2, A3, Th30;
A4: dom h = f " (SubFuncs (rng f)) by A3, Th31;
A5: g in rng f by A1, FUNCT_1:def_3;
then  g in SubFuncs (rng f) by Def1;
then A6: x in dom h by A1, A4, FUNCT_1:def_7;
 y in dom g by A3, A5, Th32;
hence f .. (x,y) = g . y by A1, FUNCT_5:38
.= h . x by A1, A3, Th34
.= <:f:> .. (y,x) by A3, A6, FUNCT_5:38 ;
::_thesis: verum
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
defpred S1[ set , set ] means  ex g, h being Function st
( $1 = g & $2 = h & dom h = f " (SubFuncs (rng f)) & ( for z being set st z in dom h holds
h . z = (uncurry f) . (z,(g . z)) ) );
A1: for x being set st x in product (doms f) holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in product (doms f) implies ex y being set st S1[x,y] )
assume  x in product (doms f) ; ::_thesis: ex y being set st S1[x,y]
then consider g being Function such that
A2: x = g and
 dom g = dom (doms f) and
 for x being set st x in dom (doms f) holds
g . x in (doms f) . x by CARD_3:def_5;
deffunc H1( set ) ->  set = (uncurry f) . [$1,(g . $1)];
consider h being Function such that
A3: ( dom h = f " (SubFuncs (rng f)) & ( for z being set st z in f " (SubFuncs (rng f)) holds
h . z = H1(z) ) ) from FUNCT_1:sch_3();
reconsider y = h as set ;
take  y ; ::_thesis: S1[x,y]
take  g ; ::_thesis: ex h being Function st
( x = g & y = h & dom h = f " (SubFuncs (rng f)) & ( for z being set st z in dom h holds
h . z = (uncurry f) . (z,(g . z)) ) )
take  h ; ::_thesis: ( x = g & y = h & dom h = f " (SubFuncs (rng f)) & ( for z being set st z in dom h holds
h . z = (uncurry f) . (z,(g . z)) ) )
thus  ( x = g & y = h & dom h = f " (SubFuncs (rng f)) & ( for z being set st z in dom h holds
h . z = (uncurry f) . (z,(g . z)) ) ) by A2, A3; ::_thesis: verum
end;
consider F being Function such that
A4: ( dom F = product (doms f) & ( for x being set st x in product (doms f) holds
S1[x,F . x] ) ) from CLASSES1:sch_1(A1);
take  F ; ::_thesis: ( dom F = product (doms f) & ( for g being Function st g in product (doms f) holds
ex h being Function st
( F . 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)) ) ) ) )
thus  dom F = product (doms f) by A4; ::_thesis: for g being Function st g in product (doms f) holds
ex h being Function st
( F . 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)) ) )
let g be Function; ::_thesis: ( g in product (doms f) implies ex h being Function st
( F . 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)) ) ) )
assume  g in product (doms f) ; ::_thesis: ex h being Function st
( F . 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)) ) )
then  ex g1, h being Function st
( g = g1 & F . g = h & dom h = f " (SubFuncs (rng f)) & ( for z being set st z in dom h holds
h . z = (uncurry f) . (z,(g1 . z)) ) ) by A4;
hence  ex h being Function st
( F . 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)) ) ) ; ::_thesis: verum
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
let f1, f2 be Function; ::_thesis: ( dom f1 = product (doms f) & ( for g being Function st g in product (doms f) holds
ex h being Function st
( f1 . 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 f2 = product (doms f) & ( for g being Function st g in product (doms f) holds
ex h being Function st
( f2 . 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)) ) ) ) implies f1 = f2 )
assume that
A5: dom f1 = product (doms f) and
A6: for g being Function st g in product (doms f) holds
ex h being Function st
( f1 . 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)) ) ) and
A7: dom f2 = product (doms f) and
A8: for g being Function st g in product (doms f) holds
ex h being Function st
( f2 . 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)) ) ) ; ::_thesis: f1 = f2
now__::_thesis:_for_x_being_set_st_x_in_product_(doms_f)_holds_
f1_._x_=_f2_._x
let x be set ; ::_thesis: ( x in product (doms f) implies f1 . x = f2 . x )
assume A9: x in product (doms f) ; ::_thesis: f1 . x = f2 . x
then consider g being Function such that
A10: x = g and
 dom g = dom (doms f) and
 for x being set st x in dom (doms f) holds
g . x in (doms f) . x by CARD_3:def_5;
consider h2 being Function such that
A11: f2 . g = h2 and
A12: dom h2 = f " (SubFuncs (rng f)) and
A13: for y being set st y in dom h2 holds
h2 . y = (uncurry f) . (y,(g . y)) by A8, A9, A10;
consider h1 being Function such that
A14: f1 . g = h1 and
A15: dom h1 = f " (SubFuncs (rng f)) and
A16: for y being set st y in dom h1 holds
h1 . y = (uncurry f) . (y,(g . y)) by A6, A9, A10;
now__::_thesis:_for_z_being_set_st_z_in_f_"_(SubFuncs_(rng_f))_holds_
h1_._z_=_h2_._z
let z be set ; ::_thesis: ( z in f " (SubFuncs (rng f)) implies h1 . z = h2 . z )
assume A17: z in f " (SubFuncs (rng f)) ; ::_thesis: h1 . z = h2 . z
then  h1 . z = (uncurry f) . (z,(g . z)) by A15, A16;
hence  h1 . z = h2 . z by A12, A13, A17; ::_thesis: verum
end;
hence  f1 . x = f2 . x by A10, A14, A15, A11, A12, FUNCT_1:2; ::_thesis: verum
end;
hence  f1 = f2 by A5, A7, FUNCT_1:2; ::_thesis: verum
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:36
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
let x be set ; ::_thesis: for g, f being Function st g in product (doms f) & x in dom g holds
(Frege f) .. (g,x) = f .. (x,(g . x))
let g, f be Function; ::_thesis: ( g in product (doms f) & x in dom g implies (Frege f) .. (g,x) = f .. (x,(g . x)) )
assume that
A1: g in product (doms f) and
A2: x in dom g ; ::_thesis: (Frege f) .. (g,x) = f .. (x,(g . x))
A3: dom g = dom (doms f) by A1, CARD_3:9;
A4: dom (doms f) = f " (SubFuncs (rng f)) by Def2;
consider h being Function such that
A5: (Frege f) . g = h and
A6: dom h = f " (SubFuncs (rng f)) and
A7: for x being set st x in dom h holds
h . x = (uncurry f) . (x,(g . x)) by A1, Def7;
 dom (Frege f) = product (doms f) by Def7;
hence (Frege f) .. (g,x) = h . x by A1, A2, A5, A6, A3, A4, FUNCT_5:38
.= f .. (x,(g . x)) by A2, A6, A7, A3, A4 ;
::_thesis: verum
end;

Lm2:  for f being Function holds rng (Frege f) c= product (rngs f)
proof
let f be Function; ::_thesis: rng (Frege f) c= product (rngs f)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (Frege f) or x in product (rngs f) )
assume  x in rng (Frege f) ; ::_thesis: x in product (rngs f)
then consider y being set  such that
A1: y in dom (Frege f) and
A2: x = (Frege f) . y by FUNCT_1:def_3;
A3: dom (Frege f) = product (doms f) by Def7;
then consider g being Function such that
A4: y = g and
 dom g = dom (doms f) and
A5: for z being set st z in dom (doms f) holds
g . z in (doms f) . z by A1, CARD_3:def_5;
consider h being Function such that
A6: (Frege f) . g = h and
A7: dom h = f " (SubFuncs (rng f)) and
A8: for z being set st z in dom h holds
h . z = (uncurry f) . (z,(g . z)) by A1, A3, A4, Def7;
A9: dom (rngs f) = f " (SubFuncs (rng f)) by Def3;
A10: dom (doms f) = f " (SubFuncs (rng f)) by Def2;
now__::_thesis:_for_z_being_set_st_z_in_dom_(rngs_f)_holds_
h_._z_in_(rngs_f)_._z
let z be set ; ::_thesis: ( z in dom (rngs f) implies h . z in (rngs f) . z )
assume A11: z in dom (rngs f) ; ::_thesis: h . z in (rngs f) . z
then  f . z in SubFuncs (rng f) by A9, FUNCT_1:def_7;
then reconsider t = f . z as Function by Def1;
A12: g . z in (doms f) . z by A5, A9, A10, A11;
A13: z in dom f by A9, A11, FUNCT_1:def_7;
then A14: (rngs f) . z = rng t by Th22;
A15: (doms f) . z = dom t by A13, Th22;
then A16: t . (g . z) in rng t by A12, FUNCT_1:def_3;
 t . (g . z) = (uncurry f) . (z,(g . z)) by A13, A12, A15, FUNCT_5:38;
hence  h . z in (rngs f) . z by A7, A8, A9, A11, A14, A16; ::_thesis: verum
end;
hence  x in product (rngs f) by A2, A4, A6, A7, A9, CARD_3:def_5; ::_thesis: verum
end;

theorem :: FUNCT_6:37
for x being set
for f, g, h, h9 being 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
let x be set ; ::_thesis: for f, g, h, h9 being 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) )
let f, g, h, h9 be Function; ::_thesis: ( x in dom f & g = f . x & h in product (doms f) & h9 = (Frege f) . h implies ( h . x in dom g & h9 . x = g . (h . x) & h9 in product (rngs f) ) )
assume that
A1: ( x in dom f & g = f . x ) and
A2: h in product (doms f) and
A3: h9 = (Frege f) . h ; ::_thesis: ( h . x in dom g & h9 . x = g . (h . x) & h9 in product (rngs f) )
A4: x in f " (SubFuncs (rng f)) by A1, Th19;
A5: dom (doms f) = f " (SubFuncs (rng f)) by Def2;
 ( ex f2 being Function st
( h = f2 & dom f2 = dom (doms f) & ( for x being set st x in dom (doms f) holds
f2 . x in (doms f) . x ) ) & (doms f) . x = dom g ) by A1, A2, Th22, CARD_3:def_5;
hence A6: h . x in dom g by A5, A4; ::_thesis: ( h9 . x = g . (h . x) & h9 in product (rngs f) )
 ex f1 being Function st
( (Frege f) . h = f1 & dom f1 = f " (SubFuncs (rng f)) & ( for x being set st x in dom f1 holds
f1 . x = (uncurry f) . (x,(h . x)) ) ) by A2, Def7;
hence h9 . x = (uncurry f) . (x,(h . x)) by A3, A4
.= g . (h . x) by A1, A6, FUNCT_5:38 ;
::_thesis: h9 in product (rngs f)
A7: rng (Frege f) c= product (rngs f) by Lm2;
 dom (Frege f) = product (doms f) by Def7;
then  h9 in rng (Frege f) by A2, A3, FUNCT_1:def_3;
hence  h9 in product (rngs f) by A7; ::_thesis: verum
end;

Lm3:  for f being Function holds product (rngs f) c= rng (Frege f)
proof
let f be Function; ::_thesis: product (rngs f) c= rng (Frege f)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in product (rngs f) or x in rng (Frege f) )
deffunc H1( set ) ->  set = (doms f) . $1;
assume  x in product (rngs f) ; ::_thesis: x in rng (Frege f)
then consider g being Function such that
A1: x = g and
A2: dom g = dom (rngs f) and
A3: for y being set st y in dom (rngs f) holds
g . y in (rngs f) . y by CARD_3:def_5;
defpred S1[ set , set ] means  ex f1 being Function st
( f1 = f . $1 & f1 . $2 = g . $1 );
consider h being Function such that
A4: ( dom h = f " (SubFuncs (rng f)) & ( for x being set st x in f " (SubFuncs (rng f)) holds
for y being set holds
( y in h . x iff ( y in H1(x) & S1[x,y] ) ) ) ) from CARD_3:sch_2();
A5: product (doms f) = dom (Frege f) by Def7;
A6: dom (doms f) = f " (SubFuncs (rng f)) by Def2;
A7: dom (rngs f) = f " (SubFuncs (rng f)) by Def3;
A8: now__::_thesis:_for_X_being_set_st_X_in_rng_h_holds_
X_<>_{}
let X be set ; ::_thesis: ( X in rng h implies X <> {} )
assume  X in rng h ; ::_thesis: X <> {}
then consider x being set  such that
A9: x in dom h and
A10: X = h . x by FUNCT_1:def_3;
 f . x in SubFuncs (rng f) by A4, A9, FUNCT_1:def_7;
then reconsider fx = f . x as Function by Def1;
A11: x in dom f by A4, A9, FUNCT_1:def_7;
then A12: (rngs f) . x = rng fx by Th22;
 g . x in (rngs f) . x by A3, A7, A4, A9;
then A13: ex y being set st
( y in dom fx & g . x = fx . y ) by A12, FUNCT_1:def_3;
 (doms f) . x = dom fx by A11, Th22;
hence  X <> {} by A4, A9, A10, A13; ::_thesis: verum
end;
A14: now__::_thesis:_(_f_"_(SubFuncs_(rng_f))_<>_{}_implies_x_in_rng_(Frege_f)_)
assume  f " (SubFuncs (rng f)) <> {} ; ::_thesis: x in rng (Frege f)
then reconsider D = rng h as non empty set by A4, RELAT_1:42;
consider Ch being Function such that
A15: dom Ch = D and
A16: for x being set st x in D holds
Ch . x in x by A8, FUNCT_1:111;
A17: dom (Ch * h) = dom h by A15, RELAT_1:27;
now__::_thesis:_for_y_being_set_st_y_in_dom_(doms_f)_holds_
(Ch_*_h)_._y_in_(doms_f)_._y
let y be set ; ::_thesis: ( y in dom (doms f) implies (Ch * h) . y in (doms f) . y )
assume A18: y in dom (doms f) ; ::_thesis: (Ch * h) . y in (doms f) . y
then  ( (Ch * h) . y = Ch . (h . y) & h . y in rng h ) by A6, A4, A17, FUNCT_1:12, FUNCT_1:def_3;
then  (Ch * h) . y in h . y by A16;
hence  (Ch * h) . y in (doms f) . y by A6, A4, A18; ::_thesis: verum
end;
then A19: Ch * h in product (doms f) by A6, A4, A17, CARD_3:def_5;
then consider h1 being Function such that
A20: (Frege f) . (Ch * h) = h1 and
A21: dom h1 = f " (SubFuncs (rng f)) and
A22: for x being set st x in dom h1 holds
h1 . x = (uncurry f) . (x,((Ch * h) . x)) by Def7;
now__::_thesis:_for_z_being_set_st_z_in_f_"_(SubFuncs_(rng_f))_holds_
h1_._z_=_g_._z
let z be set ; ::_thesis: ( z in f " (SubFuncs (rng f)) implies h1 . z = g . z )
assume A23: z in f " (SubFuncs (rng f)) ; ::_thesis: h1 . z = g . z
then A24: h1 . z = (uncurry f) . (z,((Ch * h) . z)) by A21, A22;
 ( (Ch * h) . z = Ch . (h . z) & h . z in rng h ) by A4, A17, A23, FUNCT_1:12, FUNCT_1:def_3;
then A25: (Ch * h) . z in h . z by A16;
then consider f1 being Function such that
A26: f1 = f . z and
A27: f1 . ((Ch * h) . z) = g . z by A4, A23;
A28: (Ch * h) . z in (doms f) . z by A4, A23, A25;
A29: z in dom f by A23, FUNCT_1:def_7;
then  (doms f) . z = dom f1 by A26, Th22;
hence  h1 . z = g . z by A29, A24, A26, A27, A28, FUNCT_5:38; ::_thesis: verum
end;
then  x = h1 by A1, A2, A7, A21, FUNCT_1:2;
hence  x in rng (Frege f) by A5, A19, A20, FUNCT_1:def_3; ::_thesis: verum
end;
now__::_thesis:_(_f_"_(SubFuncs_(rng_f))_=_{}_implies_x_in_rng_(Frege_f)_)
assume A30: f " (SubFuncs (rng f)) = {} ; ::_thesis: x in rng (Frege f)
then A31: g = {} by A2, Def3;
 dom (Frege f) = {{}} by A6, A5, A30, CARD_3:10, RELAT_1:41;
then A32: {} in dom (Frege f) by TARSKI:def_1;
then consider h being Function such that
A33: (Frege f) . {} = h and
A34: dom h = f " (SubFuncs (rng f)) and
 for x being set st x in dom h holds
h . x = (uncurry f) . (x,({} . x)) by A5, Def7;
 h = {} by A30, A34;
hence  x in rng (Frege f) by A1, A31, A32, A33, FUNCT_1:def_3; ::_thesis: verum
end;
hence  x in rng (Frege f) by A14; ::_thesis: verum
end;

theorem Th38: :: FUNCT_6:38
for f being Function holds rng (Frege f) = product (rngs f)
proof
let f be Function; ::_thesis: rng (Frege f) = product (rngs f)
thus  ( rng (Frege f) c= product (rngs f) & product (rngs f) c= rng (Frege f) ) by Lm2, Lm3; :: according to XBOOLE_0:def_10 ::_thesis: verum
end;

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 )
proof
let f be Function; ::_thesis: ( not {} in rng f implies ( Frege f is one-to-one iff for g being Function st g in rng f holds
g is one-to-one ) )
set h0 = the Element of product (doms f);
A1: dom (doms f) = f " (SubFuncs (rng f)) by Def2;
assume A2: not {} in rng f ; ::_thesis: ( Frege f is one-to-one iff for g being Function st g in rng f holds
g is one-to-one )
now__::_thesis:_not_{}_in_rng_(doms_f)
assume  {} in rng (doms f) ; ::_thesis: contradiction
then consider x being set  such that
A3: x in dom (doms f) and
A4: {} = (doms f) . x by FUNCT_1:def_3;
A5: x in f " (SubFuncs (rng f)) by A3, Def2;
then  f . x in SubFuncs (rng f) by FUNCT_1:def_7;
then reconsider g = f . x as Function by Def1;
A6: x in dom f by A5, FUNCT_1:def_7;
then A7: g in rng f by FUNCT_1:def_3;
 {} = dom g by A4, A6, Th22;
hence  contradiction by A2, A7, RELAT_1:41; ::_thesis: verum
end;
then  product (doms f) <> {} by CARD_3:26;
then consider h being Function such that
 the Element of product (doms f) = h and
 dom h = dom (doms f) and
A8: for x being set st x in dom (doms f) holds
h . x in (doms f) . x by CARD_3:def_5;
A9: dom (Frege f) = product (doms f) by Def7;
thus  ( Frege f is one-to-one implies for g being Function st g in rng f holds
g is one-to-one ) ::_thesis: ( ( for g being Function st g in rng f holds
g is one-to-one ) implies Frege f is one-to-one )
proof
deffunc H1( set ) ->  set = h . $1;
assume A10: for x, y being set st x in dom (Frege f) & y in dom (Frege f) & (Frege f) . x = (Frege f) . y holds
x = y ; :: according to FUNCT_1:def_4 ::_thesis: for g being Function st g in rng f holds
g is one-to-one
let g be Function; ::_thesis: ( g in rng f implies g is one-to-one )
assume  g in rng f ; ::_thesis: g is one-to-one
then consider z being set  such that
A11: ( z in dom f & g = f . z ) by FUNCT_1:def_3;
defpred S1[ set ] means $1 = z;
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in dom g or not b1 in dom g or not g . x = g . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in dom g or not y in dom g or not g . x = g . y or x = y )
deffunc H2( set ) ->  set = x;
consider h1 being Function such that
A12: ( dom h1 = f " (SubFuncs (rng f)) & ( for a being set st a in f " (SubFuncs (rng f)) holds
( ( S1[a] implies h1 . a = H2(a) ) & ( not S1[a] implies h1 . a = H1(a) ) ) ) ) from PARTFUN1:sch_1();
assume that
A13: x in dom g and
A14: y in dom g and
A15: g . x = g . y ; ::_thesis: x = y
now__::_thesis:_for_a_being_set_st_a_in_dom_(doms_f)_holds_
h1_._a_in_(doms_f)_._a
let a be set ; ::_thesis: ( a in dom (doms f) implies h1 . a in (doms f) . a )
assume A16: a in dom (doms f) ; ::_thesis: h1 . a in (doms f) . a
then A17: ( a <> z implies h1 . a = h . a ) by A1, A12;
 ( a = z implies h1 . a = x ) by A1, A12, A16;
hence  h1 . a in (doms f) . a by A8, A11, A13, A16, A17, Th22; ::_thesis: verum
end;
then A18: h1 in product (doms f) by A1, A12, CARD_3:def_5;
then consider g1 being Function such that
A19: (Frege f) . h1 = g1 and
A20: dom g1 = f " (SubFuncs (rng f)) and
A21: for x being set st x in dom g1 holds
g1 . x = (uncurry f) . (x,(h1 . x)) by Def7;
defpred S2[ set ] means $1 = z;
deffunc H3( set ) ->  set = h . $1;
deffunc H4( set ) ->  set = y;
consider h2 being Function such that
A22: ( dom h2 = f " (SubFuncs (rng f)) & ( for a being set st a in f " (SubFuncs (rng f)) holds
( ( S2[a] implies h2 . a = H4(a) ) & ( not S2[a] implies h2 . a = H3(a) ) ) ) ) from PARTFUN1:sch_1();
now__::_thesis:_for_a_being_set_st_a_in_dom_(doms_f)_holds_
h2_._a_in_(doms_f)_._a
let a be set ; ::_thesis: ( a in dom (doms f) implies h2 . a in (doms f) . a )
assume A23: a in dom (doms f) ; ::_thesis: h2 . a in (doms f) . a
then A24: ( a <> z implies h2 . a = h . a ) by A1, A22;
 ( a = z implies h2 . a = y ) by A1, A22, A23;
hence  h2 . a in (doms f) . a by A8, A11, A14, A23, A24, Th22; ::_thesis: verum
end;
then A25: h2 in product (doms f) by A1, A22, CARD_3:def_5;
then consider g2 being Function such that
A26: (Frege f) . h2 = g2 and
A27: dom g2 = f " (SubFuncs (rng f)) and
A28: for x being set st x in dom g2 holds
g2 . x = (uncurry f) . (x,(h2 . x)) by Def7;
now__::_thesis:_for_a_being_set_st_a_in_f_"_(SubFuncs_(rng_f))_holds_
g1_._a_=_g2_._a
let a be set ; ::_thesis: ( a in f " (SubFuncs (rng f)) implies g1 . b1 = g2 . b1 )
assume A29: a in f " (SubFuncs (rng f)) ; ::_thesis: g1 . b1 = g2 . b1
then A30: g2 . a = (uncurry f) . (a,(h2 . a)) by A27, A28;
A31: g1 . a = (uncurry f) . (a,(h1 . a)) by A20, A21, A29;
percases ( a <> z or a = z ) ;
supposeA32: a <> z ; ::_thesis: g1 . b1 = g2 . b1
then  h1 . a = h . a by A12, A29;
hence  g1 . a = g2 . a by A22, A29, A30, A31, A32; ::_thesis: verum
end;
supposeA33: a = z ; ::_thesis: g1 . b1 = g2 . b1
then  h1 . a = x by A12, A29;
then A34: g1 . a = g . x by A11, A13, A31, A33, FUNCT_5:38;
 h2 . a = y by A22, A29, A33;
hence  g1 . a = g2 . a by A11, A14, A15, A30, A33, A34, FUNCT_5:38; ::_thesis: verum
end;
end;
end;
then  g1 = g2 by A20, A27, FUNCT_1:2;
then A35: h1 = h2 by A9, A10, A18, A19, A25, A26;
 g in rng f by A11, FUNCT_1:def_3;
then  g in SubFuncs (rng f) by Def1;
then A36: z in f " (SubFuncs (rng f)) by A11, FUNCT_1:def_7;
then  h1 . z = x by A12;
hence  x = y by A36, A22, A35; ::_thesis: verum
end;
assume A37: for g being Function st g in rng f holds
g is one-to-one ; ::_thesis: Frege f is one-to-one
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in dom (Frege f) or not b1 in dom (Frege f) or not (Frege f) . x = (Frege f) . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in dom (Frege f) or not y in dom (Frege f) or not (Frege f) . x = (Frege f) . y or x = y )
assume that
A38: x in dom (Frege f) and
A39: y in dom (Frege f) and
A40: (Frege f) . x = (Frege f) . y ; ::_thesis: x = y
consider g2 being Function such that
A41: y = g2 and
A42: dom g2 = dom (doms f) and
A43: for x being set st x in dom (doms f) holds
g2 . x in (doms f) . x by A9, A39, CARD_3:def_5;
consider g1 being Function such that
A44: x = g1 and
A45: dom g1 = dom (doms f) and
A46: for x being set st x in dom (doms f) holds
g1 . x in (doms f) . x by A9, A38, CARD_3:def_5;
consider h2 being Function such that
A47: (Frege f) . g2 = h2 and
A48: ( dom h2 = f " (SubFuncs (rng f)) & ( for x being set st x in dom h2 holds
h2 . x = (uncurry f) . (x,(g2 . x)) ) ) by A9, A39, A41, Def7;
consider h1 being Function such that
A49: (Frege f) . g1 = h1 and
A50: ( dom h1 = f " (SubFuncs (rng f)) & ( for x being set st x in dom h1 holds
h1 . x = (uncurry f) . (x,(g1 . x)) ) ) by A9, A38, A44, Def7;
now__::_thesis:_for_a_being_set_st_a_in_f_"_(SubFuncs_(rng_f))_holds_
g1_._a_=_g2_._a
let a be set ; ::_thesis: ( a in f " (SubFuncs (rng f)) implies g1 . a = g2 . a )
assume A51: a in f " (SubFuncs (rng f)) ; ::_thesis: g1 . a = g2 . a
then  f . a in SubFuncs (rng f) by FUNCT_1:def_7;
then reconsider g = f . a as Function by Def1;
A52: a in dom f by A51, FUNCT_1:def_7;
then A53: dom g = (doms f) . a by Th22;
then A54: g2 . a in dom g by A1, A43, A51;
A55: g1 . a in dom g by A1, A46, A51, A53;
 h2 . a = (uncurry f) . (a,(g2 . a)) by A48, A51;
then A56: h2 . a = g . (g2 . a) by A52, A54, FUNCT_5:38;
 g in rng f by A52, FUNCT_1:def_3;
then A57: g is one-to-one by A37;
 h1 . a = (uncurry f) . (a,(g1 . a)) by A50, A51;
then  h1 . a = g . (g1 . a) by A52, A55, FUNCT_5:38;
hence  g1 . a = g2 . a by A40, A44, A41, A49, A47, A55, A54, A56, A57, FUNCT_1:def_4; ::_thesis: verum
end;
hence  x = y by A1, A44, A45, A41, A42, FUNCT_1:2; ::_thesis: verum
end;

begin

theorem :: FUNCT_6:40
( <:{}:> = {} & Frege {} = {} .--> {} )
proof
A1: dom (doms {}) = {} " (SubFuncs {}) by Def2, RELAT_1:38;
then A2: product (doms {}) = {{}} by CARD_3:10, RELAT_1:41;
A3: now__::_thesis:_for_x_being_set_st_x_in_{{}}_holds_
(Frege_{})_._x_=_{}
let x be set ; ::_thesis: ( x in {{}} implies (Frege {}) . x = {} )
assume A4: x in {{}} ; ::_thesis: (Frege {}) . x = {}
then A5: x = {} by TARSKI:def_1;
then  ex h being Function st
( (Frege {}) . {} = h & dom h = {} " (SubFuncs (rng {})) & ( for x being set st x in dom h holds
h . x = (uncurry {}) . (x,({} . x)) ) ) by A2, A4, Def7;
hence  (Frege {}) . x = {} by A5; ::_thesis: verum
end;
A6: meet {} = {} by SETFAM_1:def_1;
 rng (doms {}) = {} by A1, RELAT_1:38, RELAT_1:41;
then  dom <:{}:> = {} by A6, Th29;
hence  <:{}:> = {} ; ::_thesis: Frege {} = {} .--> {}
 dom (Frege {}) = product (doms {}) by Def7;
hence  Frege {} = {} .--> {} by A2, A3, FUNCOP_1:11; ::_thesis: verum
end;

theorem :: FUNCT_6:41
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
let X be set ; ::_thesis: 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) ) )
let f be Function; ::_thesis: ( X <> {} implies ( dom <:(X --> f):> = dom f & ( for x being set st x in dom f holds
<:(X --> f):> . x = X --> (f . x) ) ) )
assume A1: X <> {} ; ::_thesis: ( dom <:(X --> f):> = dom f & ( for x being set st x in dom f holds
<:(X --> f):> . x = X --> (f . x) ) )
thus A2: dom <:(X --> f):> = meet (doms (X --> f)) by Th29
.= meet (X --> (dom f)) by Th24
.= dom f by A1, Th27 ; ::_thesis: for x being set st x in dom f holds
<:(X --> f):> . x = X --> (f . x)
A3: ( rng <:(X --> f):> c= product (rngs (X --> f)) & rngs (X --> f) = X --> (rng f) ) by Th24, Th29;
let x be set ; ::_thesis: ( x in dom f implies <:(X --> f):> . x = X --> (f . x) )
assume A4: x in dom f ; ::_thesis: <:(X --> f):> . x = X --> (f . x)
then  <:(X --> f):> . x in rng <:(X --> f):> by A2, FUNCT_1:def_3;
then consider g being Function such that
A5: <:(X --> f):> . x = g and
A6: dom g = dom (X --> (rng f)) and
 for y being set st y in dom (X --> (rng f)) holds
g . y in (X --> (rng f)) . y by A3, CARD_3:def_5;
A7: dom g = X by A6, FUNCOP_1:13;
A8: dom (X --> f) = X by FUNCOP_1:13;
A9: now__::_thesis:_for_y_being_set_st_y_in_X_holds_
g_._y_=_(X_-->_(f_._x))_._y
let y be set ; ::_thesis: ( y in X implies g . y = (X --> (f . x)) . y )
assume A10: y in X ; ::_thesis: g . y = (X --> (f . x)) . y
then  ( g . y = (uncurry (X --> f)) . (y,x) & (X --> f) . y = f ) by A2, A4, A5, A7, Th31, FUNCOP_1:7;
then  g . y = f . x by A4, A8, A10, FUNCT_5:38;
hence  g . y = (X --> (f . x)) . y by A10, FUNCOP_1:7; ::_thesis: verum
end;
 dom (X --> (f . x)) = X by FUNCOP_1:13;
hence  <:(X --> f):> . x = X --> (f . x) by A5, A7, A9, FUNCT_1:2; ::_thesis: verum
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
let X be set ; ::_thesis: 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 ) )
let f be Function; ::_thesis: ( 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 ) )
A1: product (X --> (dom f)) = Funcs (X,(dom f)) by CARD_3:11;
A2: doms (X --> f) = X --> (dom f) by Th24;
 ( rngs (X --> f) = X --> (rng f) & product (X --> (rng f)) = Funcs (X,(rng f)) ) by Th24, CARD_3:11;
hence  ( dom (Frege (X --> f)) = Funcs (X,(dom f)) & rng (Frege (X --> f)) = Funcs (X,(rng f)) ) by A2, A1, Def7, Th38; ::_thesis: for g being Function st g in Funcs (X,(dom f)) holds
(Frege (X --> f)) . g = f * g
let g be Function; ::_thesis: ( g in Funcs (X,(dom f)) implies (Frege (X --> f)) . g = f * g )
assume A3: g in Funcs (X,(dom f)) ; ::_thesis: (Frege (X --> f)) . g = f * g
then consider h being Function such that
A4: (Frege (X --> f)) . g = h and
A5: dom h = (X --> f) " (SubFuncs (rng (X --> f))) and
A6: for x being set st x in dom h holds
h . x = (uncurry (X --> f)) . (x,(g . x)) by A2, A1, Def7;
 dom (X --> (dom f)) = X by FUNCOP_1:13;
then A7: dom h = X by A2, A5, Def2;
A8: ex g9 being Function st
( g = g9 & dom g9 = X & rng g9 c= dom f ) by A3, FUNCT_2:def_2;
then A9: dom (f * g) = X by RELAT_1:27;
A10: dom (X --> f) = X by FUNCOP_1:13;
now__::_thesis:_for_x_being_set_st_x_in_X_holds_
(f_*_g)_._x_=_h_._x
let x be set ; ::_thesis: ( x in X implies (f * g) . x = h . x )
assume A11: x in X ; ::_thesis: (f * g) . x = h . x
then A12: ( h . x = (uncurry (X --> f)) . (x,(g . x)) & (X --> f) . x = f ) by A6, A7, FUNCOP_1:7;
 ( g . x in rng g & (f * g) . x = f . (g . x) ) by A8, A9, A11, FUNCT_1:12, FUNCT_1:def_3;
hence  (f * g) . x = h . x by A8, A10, A11, A12, FUNCT_5:38; ::_thesis: verum
end;
hence  (Frege (X --> f)) . g = f * g by A4, A7, A9, FUNCT_1:2; ::_thesis: verum
end;

theorem Th43: :: FUNCT_6:43
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
let X be set ; ::_thesis: 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
let f, g be Function; ::_thesis: ( dom f = X & dom g = X & ( for x being set st x in X holds
f . x,g . x are_equipotent ) implies product f, product g are_equipotent )
assume that
A1: dom f = X and
A2: dom g = X and
A3: for x being set st x in X holds
f . x,g . x are_equipotent ; ::_thesis: product f, product g are_equipotent
defpred S1[ set , set ] means  ex f1 being Function st
( $2 = f1 & f1 is one-to-one & dom f1 = f . $1 & rng f1 = g . $1 );
A4: for x being set st x in X holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in X implies ex y being set st S1[x,y] )
assume  x in X ; ::_thesis: ex y being set st S1[x,y]
then  f . x,g . x are_equipotent by A3;
then  ex h being Function st
( h is one-to-one & dom h = f . x & rng h = g . x ) by WELLORD2:def_4;
hence  ex y being set st S1[x,y] ; ::_thesis: verum
end;
consider h being Function such that
A5: ( dom h = X & ( for x being set st x in X holds
S1[x,h . x] ) ) from CLASSES1:sch_1(A4);
A6: now__::_thesis:_for_x_being_set_st_x_in_X_holds_
(rngs_h)_._x_=_g_._x
let x be set ; ::_thesis: ( x in X implies (rngs h) . x = g . x )
assume A7: x in X ; ::_thesis: (rngs h) . x = g . x
then  ex f1 being Function st
( h . x = f1 & f1 is one-to-one & dom f1 = f . x & rng f1 = g . x ) by A5;
hence  (rngs h) . x = g . x by A5, A7, Th22; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_rng_h_holds_
x_is_Function
let x be set ; ::_thesis: ( x in rng h implies x is Function )
assume  x in rng h ; ::_thesis: x is Function
then consider a being set  such that
A8: ( a in X & x = h . a ) by A5, FUNCT_1:def_3;
 ex f1 being Function st
( x = f1 & f1 is one-to-one & dom f1 = f . a & rng f1 = g . a ) by A5, A8;
hence  x is Function ; ::_thesis: verum
end;
then  SubFuncs (rng h) = rng h by Lm1;
then A9: h " (SubFuncs (rng h)) = X by A5, RELAT_1:134;
then  dom (rngs h) = X by Def3;
then A10: rngs h = g by A2, A6, FUNCT_1:2;
A11: now__::_thesis:_for_x_being_set_st_x_in_X_holds_
(doms_h)_._x_=_f_._x
let x be set ; ::_thesis: ( x in X implies (doms h) . x = f . x )
assume A12: x in X ; ::_thesis: (doms h) . x = f . x
then  ex f1 being Function st
( h . x = f1 & f1 is one-to-one & dom f1 = f . x & rng f1 = g . x ) by A5;
hence  (doms h) . x = f . x by A5, A12, Th22; ::_thesis: verum
end;
 dom (doms h) = X by A9, Def2;
then A13: doms h = f by A1, A11, FUNCT_1:2;
now__::_thesis:_product_f,_product_g_are_equipotent
percases ( {} in rng h or not {} in rng h ) ;
suppose {} in rng h ; ::_thesis: product f, product g are_equipotent
then consider x being set  such that
A14: x in X and
A15: {} = h . x by A5, FUNCT_1:def_3;
A16: ex f1 being Function st
( {} = f1 & f1 is one-to-one & dom f1 = f . x & rng f1 = g . x ) by A5, A14, A15;
then  {} in rng f by A1, A14, FUNCT_1:def_3, RELAT_1:38;
then A17: product f = {} by CARD_3:26;
 {} in rng g by A2, A14, A16, FUNCT_1:def_3, RELAT_1:38;
hence  product f, product g are_equipotent by A17, CARD_3:26; ::_thesis: verum
end;
supposeA18: not {} in rng h ; ::_thesis: product f, product g are_equipotent
A19: now__::_thesis:_for_f1_being_Function_st_f1_in_rng_h_holds_
f1_is_one-to-one
let f1 be Function; ::_thesis: ( f1 in rng h implies f1 is one-to-one )
assume  f1 in rng h ; ::_thesis: f1 is one-to-one
then consider x being set  such that
A20: x in X and
A21: f1 = h . x by A5, FUNCT_1:def_3;
 ex f1 being Function st
( h . x = f1 & f1 is one-to-one & dom f1 = f . x & rng f1 = g . x ) by A5, A20;
hence  f1 is one-to-one by A21; ::_thesis: verum
end;
thus  product f, product g are_equipotent ::_thesis: verum
proof
take  Frege h ; :: according to WELLORD2:def_4 ::_thesis: ( Frege h is one-to-one & dom (Frege h) = product f & rng (Frege h) = product g )
thus  ( Frege h is one-to-one & dom (Frege h) = product f & rng (Frege h) = product g ) by A13, A10, A18, A19, Def7, Th38, Th39; ::_thesis: verum
end;
end;
end;
end;
hence  product f, product g are_equipotent ; ::_thesis: verum
end;

theorem Th44: :: FUNCT_6:44
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
let f, h, g be Function; ::_thesis: ( 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 ) implies product f, product g are_equipotent )
set X = dom f;
assume that
A1: dom f = dom h and
A2: dom g = rng h and
A3: h is one-to-one and
A4: for x being set st x in dom h holds
f . x,g . (h . x) are_equipotent ; ::_thesis: product f, product g are_equipotent
A5: h * (h ") = id (dom g) by A2, A3, FUNCT_1:39;
A6: dom (g * h) = dom f by A1, A2, RELAT_1:27;
now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_
f_._x,(g_*_h)_._x_are_equipotent
let x be set ; ::_thesis: ( x in dom f implies f . x,(g * h) . x are_equipotent )
assume A7: x in dom f ; ::_thesis: f . x,(g * h) . x are_equipotent
then  f . x,g . (h . x) are_equipotent by A1, A4;
hence  f . x,(g * h) . x are_equipotent by A6, A7, FUNCT_1:12; ::_thesis: verum
end;
then A8: product f, product (g * h) are_equipotent by A6, Th43;
defpred S1[ set , set ] means  ex f1 being Function st
( $1 = f1 & $2 = f1 * (h ") );
A9: for x being set st x in product (g * h) holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in product (g * h) implies ex y being set st S1[x,y] )
assume  x in product (g * h) ; ::_thesis: ex y being set st S1[x,y]
then  ex f1 being Function st
( x = f1 & dom f1 = dom (g * h) & ( for y being set st y in dom (g * h) holds
f1 . y in (g * h) . y ) ) by CARD_3:def_5;
then consider f1 being Function such that
A10: x = f1 ;
 f1 * (h ") = f1 * (h ") ;
hence  ex y being set st S1[x,y] by A10; ::_thesis: verum
end;
consider F being Function such that
A11: ( dom F = product (g * h) & ( for x being set st x in product (g * h) holds
S1[x,F . x] ) ) from CLASSES1:sch_1(A9);
A12: rng (h ") = dom f by A1, A3, FUNCT_1:33;
A13: F is one-to-one
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in dom F or not b1 in dom F or not F . x = F . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in dom F or not y in dom F or not F . x = F . y or x = y )
assume that
A14: x in dom F and
A15: y in dom F and
A16: F . x = F . y ; ::_thesis: x = y
consider g2 being Function such that
A17: y = g2 and
A18: F . y = g2 * (h ") by A11, A15;
A19: dom g2 = dom f by A6, A11, A15, A17, CARD_3:9;
consider g1 being Function such that
A20: x = g1 and
A21: F . x = g1 * (h ") by A11, A14;
 dom g1 = dom f by A6, A11, A14, A20, CARD_3:9;
hence  x = y by A12, A16, A20, A21, A17, A18, A19, FUNCT_1:86; ::_thesis: verum
end;
A22: ( (g * h) * (h ") = g * (h * (h ")) & g * (id (dom g)) = g ) by RELAT_1:36, RELAT_1:52;
A23: product g c= rng F
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in product g or x in rng F )
assume  x in product g ; ::_thesis: x in rng F
then consider f1 being Function such that
A24: x = f1 and
A25: dom f1 = dom g and
A26: for z being set st z in dom g holds
f1 . z in g . z by CARD_3:def_5;
A27: dom (f1 * h) = dom f by A1, A2, A25, RELAT_1:27;
now__::_thesis:_for_z_being_set_st_z_in_dom_f_holds_
(f1_*_h)_._z_in_(g_*_h)_._z
let z be set ; ::_thesis: ( z in dom f implies (f1 * h) . z in (g * h) . z )
assume A28: z in dom f ; ::_thesis: (f1 * h) . z in (g * h) . z
then A29: h . z in dom g by A1, A2, FUNCT_1:def_3;
A30: (h ") . (h . z) = z by A1, A3, A28, FUNCT_1:34;
 (f1 * h) . z = f1 . (h . z) by A27, A28, FUNCT_1:12;
then  (f1 * h) . z in ((g * h) * (h ")) . (h . z) by A5, A22, A26, A29;
hence  (f1 * h) . z in (g * h) . z by A5, A22, A29, A30, FUNCT_1:12; ::_thesis: verum
end;
then A31: f1 * h in product (g * h) by A6, A27, CARD_3:def_5;
then  ex f2 being Function st
( f1 * h = f2 & F . (f1 * h) = f2 * (h ") ) by A11;
then F . (f1 * h) = f1 * (id (dom g)) by A5, RELAT_1:36
.= x by A24, A25, RELAT_1:51 ;
hence  x in rng F by A11, A31, FUNCT_1:def_3; ::_thesis: verum
end;
A32: dom (h ") = rng h by A3, FUNCT_1:33;
 rng F c= product g
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng F or x in product g )
assume  x in rng F ; ::_thesis: x in product g
then consider y being set  such that
A33: y in dom F and
A34: x = F . y by FUNCT_1:def_3;
consider f1 being Function such that
A35: y = f1 and
A36: dom f1 = dom f and
A37: for z being set st z in dom f holds
f1 . z in (g * h) . z by A6, A11, A33, CARD_3:def_5;
A38: dom (f1 * (h ")) = dom g by A2, A12, A32, A36, RELAT_1:27;
A39: now__::_thesis:_for_z_being_set_st_z_in_dom_g_holds_
(f1_*_(h_"))_._z_in_g_._z
let z be set ; ::_thesis: ( z in dom g implies (f1 * (h ")) . z in g . z )
assume A40: z in dom g ; ::_thesis: (f1 * (h ")) . z in g . z
then A41: (h ") . z in dom f by A2, A12, A32, FUNCT_1:def_3;
 ( g . z = (g * h) . ((h ") . z) & (f1 * (h ")) . z = f1 . ((h ") . z) ) by A5, A22, A38, A40, FUNCT_1:12;
hence  (f1 * (h ")) . z in g . z by A37, A41; ::_thesis: verum
end;
 ex f1 being Function st
( y = f1 & F . y = f1 * (h ") ) by A11, A33;
hence  x in product g by A34, A35, A38, A39, CARD_3:def_5; ::_thesis: verum
end;
then  rng F = product g by A23, XBOOLE_0:def_10;
then  product (g * h), product g are_equipotent by A11, A13, WELLORD2:def_4;
hence  product f, product g are_equipotent by A8, WELLORD2:15; ::_thesis: verum
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
let X be set ; ::_thesis: for f being Function
for P being Permutation of X st dom f = X holds
product f, product (f * P) are_equipotent
let f be Function; ::_thesis: for P being Permutation of X st dom f = X holds
product f, product (f * P) are_equipotent
let P be Permutation of X; ::_thesis: ( dom f = X implies product f, product (f * P) are_equipotent )
assume A1: dom f = X ; ::_thesis: product f, product (f * P) are_equipotent
A2: rng P = X by FUNCT_2:def_3;
 dom P = X by FUNCT_2:52;
then A3: dom (f * P) = X by A1, A2, RELAT_1:27;
A4: rng (P ") = X by FUNCT_2:def_3;
A5: dom (P ") = X by FUNCT_2:52;
now__::_thesis:_for_x_being_set_st_x_in_dom_(P_")_holds_
f_._x,(f_*_P)_._((P_")_._x)_are_equipotent
let x be set ; ::_thesis: ( x in dom (P ") implies f . x,(f * P) . ((P ") . x) are_equipotent )
assume A6: x in dom (P ") ; ::_thesis: f . x,(f * P) . ((P ") . x) are_equipotent
then  (P ") . x in X by A4, FUNCT_1:def_3;
then (f * P) . ((P ") . x) = f . (P . ((P ") . x)) by A3, FUNCT_1:12
.= f . x by A5, A2, A6, FUNCT_1:35 ;
hence  f . x,(f * P) . ((P ") . x) are_equipotent ; ::_thesis: verum
end;
hence  product f, product (f * P) are_equipotent by A1, A5, A4, A3, Th44; ::_thesis: verum
end;

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 & ( 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
deffunc H1( set ) ->  set = Funcs ((f . $1),X);
 ex F being Function st
( dom F = dom f & ( for x being set st x in dom f holds
F . x = H1(x) ) ) from FUNCT_1:sch_3();
hence  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) ) ) ; ::_thesis: verum
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
let f1, f2 be Function; ::_thesis: ( dom f1 = dom f & ( for x being set st x in dom f holds
f1 . x = Funcs ((f . x),X) ) & dom f2 = dom f & ( for x being set st x in dom f holds
f2 . x = Funcs ((f . x),X) ) implies f1 = f2 )
assume that
A1: dom f1 = dom f and
A2: for x being set st x in dom f holds
f1 . x = Funcs ((f . x),X) and
A3: dom f2 = dom f and
A4: for x being set st x in dom f holds
f2 . x = Funcs ((f . x),X) ; ::_thesis: f1 = f2
now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_
f1_._x_=_f2_._x
let x be set ; ::_thesis: ( x in dom f implies f1 . x = f2 . x )
assume A5: x in dom f ; ::_thesis: f1 . x = f2 . x
then  f1 . x = Funcs ((f . x),X) by A2;
hence  f1 . x = f2 . x by A4, A5; ::_thesis: verum
end;
hence  f1 = f2 by A1, A3, FUNCT_1:2; ::_thesis: verum
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:46
for f being Function st not {} in rng f holds
Funcs (f,{}) = (dom f) --> {}
proof
let f be Function; ::_thesis: ( not {} in rng f implies Funcs (f,{}) = (dom f) --> {} )
assume A1: not {} in rng f ; ::_thesis: Funcs (f,{}) = (dom f) --> {}
A2: now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_
((dom_f)_-->_{})_._x_=_Funcs_((f_._x),{})
let x be set ; ::_thesis: ( x in dom f implies ((dom f) --> {}) . x = Funcs ((f . x),{}) )
assume A3: x in dom f ; ::_thesis: ((dom f) --> {}) . x = Funcs ((f . x),{})
then A4: f . x <> {} by A1, FUNCT_1:def_3;
thus ((dom f) --> {}) . x = {} by A3, FUNCOP_1:7
.= Funcs ((f . x),{}) by A4 ; ::_thesis: verum
end;
 dom ((dom f) --> {}) = dom f by FUNCOP_1:13;
hence  Funcs (f,{}) = (dom f) --> {} by A2, Def8; ::_thesis: verum
end;

theorem :: FUNCT_6:47
for X being set holds Funcs ({},X) = {}
proof
let X be set ; ::_thesis: Funcs ({},X) = {}
 dom (Funcs ({},X)) = dom {} by Def8;
hence  Funcs ({},X) = {} ; ::_thesis: verum
end;

theorem :: FUNCT_6:48
for X, Y, Z being set holds Funcs ((X --> Y),Z) = X --> (Funcs (Y,Z))
proof
let X, Y, Z be set ; ::_thesis: Funcs ((X --> Y),Z) = X --> (Funcs (Y,Z))
A1: X = dom (X --> Y) by FUNCOP_1:13;
A2: now__::_thesis:_for_x_being_set_st_x_in_X_holds_
(Funcs_((X_-->_Y),Z))_._x_=_Funcs_(Y,Z)
let x be set ; ::_thesis: ( x in X implies (Funcs ((X --> Y),Z)) . x = Funcs (Y,Z) )
assume A3: x in X ; ::_thesis: (Funcs ((X --> Y),Z)) . x = Funcs (Y,Z)
then  (Funcs ((X --> Y),Z)) . x = Funcs (((X --> Y) . x),Z) by A1, Def8;
hence  (Funcs ((X --> Y),Z)) . x = Funcs (Y,Z) by A3, FUNCOP_1:7; ::_thesis: verum
end;
 dom (Funcs ((X --> Y),Z)) = dom (X --> Y) by Def8;
hence  Funcs ((X --> Y),Z) = X --> (Funcs (Y,Z)) by A1, A2, FUNCOP_1:11; ::_thesis: verum
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
let x, y, z be set ; ::_thesis: 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
let f, g be Function; ::_thesis: ( [x,y] in dom f & g = (curry f) . x & z in dom g implies [x,z] in dom f )
assume  [x,y] in dom f ; ::_thesis: ( not g = (curry f) . x or not z in dom g or [x,z] in dom f )
then  x in proj1 (dom f) by XTUPLE_0:def_12;
then A1: ex g9 being Function st
( (curry f) . x = g9 & dom g9 = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in dom g9 holds
g9 . y = f . (x,y) ) ) by FUNCT_5:def_1;
assume  ( g = (curry f) . x & z in dom g ) ; ::_thesis: [x,z] in dom f
then consider y being set  such that
A2: [y,z] in (dom f) /\ [:{x},(proj2 (dom f)):] by A1, XTUPLE_0:def_13;
 [y,z] in [:{x},(proj2 (dom f)):] by A2, XBOOLE_0:def_4;
then A3: y in {x} by ZFMISC_1:87;
 [y,z] in dom f by A2, XBOOLE_0:def_4;
hence  [x,z] in dom f by A3, TARSKI:def_1; ::_thesis: verum
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
proof
let X be set ; ::_thesis: for f being Function holds Funcs ((Union (disjoin f)),X), product (Funcs (f,X)) are_equipotent
let f be Function; ::_thesis: Funcs ((Union (disjoin f)),X), product (Funcs (f,X)) are_equipotent
defpred S1[ set , set ] means  ex g, h being Function st
( $1 = g & $2 = h & dom h = dom f & ( for y being set st y in dom f holds
( ( f . y = {} implies h . y = {} ) & ( f . y <> {} implies h . y = (curry' g) . y ) ) ) );
A1: for x being set st x in Funcs ((Union (disjoin f)),X) holds
ex z being set st S1[x,z]
proof
defpred S2[ set ] means f . $1 = {} ;
deffunc H1( set ) ->  set = {} ;
let x be set ; ::_thesis: ( x in Funcs ((Union (disjoin f)),X) implies ex z being set st S1[x,z] )
assume  x in Funcs ((Union (disjoin f)),X) ; ::_thesis: ex z being set st S1[x,z]
then consider g being Function such that
A2: x = g and
 dom g = Union (disjoin f) and
 rng g c= X by FUNCT_2:def_2;
deffunc H2( set ) ->  set = (curry' g) . $1;
 ex h being Function st
( dom h = dom f & ( for y being set st y in dom f holds
( ( S2[y] implies h . y = H1(y) ) & ( not S2[y] implies h . y = H2(y) ) ) ) ) from PARTFUN1:sch_1();
hence  ex z being set st S1[x,z] by A2; ::_thesis: verum
end;
consider F being Function such that
A3: ( dom F = Funcs ((Union (disjoin f)),X) & ( for x being set st x in Funcs ((Union (disjoin f)),X) holds
S1[x,F . x] ) ) from CLASSES1:sch_1(A1);
take  F ; :: according to WELLORD2:def_4 ::_thesis: ( F is one-to-one & dom F = Funcs ((Union (disjoin f)),X) & rng F = product (Funcs (f,X)) )
thus  F is one-to-one ::_thesis: ( dom F = Funcs ((Union (disjoin f)),X) & rng F = product (Funcs (f,X)) )
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in dom F or not b1 in dom F or not F . x = F . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in dom F or not y in dom F or not F . x = F . y or x = y )
assume that
A4: x in dom F and
A5: y in dom F and
A6: F . x = F . y ; ::_thesis: x = y
A7: ex f2 being Function st
( y = f2 & dom f2 = Union (disjoin f) & rng f2 c= X ) by A3, A5, FUNCT_2:def_2;
consider g1, h1 being Function such that
A8: x = g1 and
A9: F . x = h1 and
 dom h1 = dom f and
A10: for y being set st y in dom f holds
( ( f . y = {} implies h1 . y = {} ) & ( f . y <> {} implies h1 . y = (curry' g1) . y ) ) by A3, A4;
consider g2, h2 being Function such that
A11: y = g2 and
A12: F . y = h2 and
 dom h2 = dom f and
A13: for y being set st y in dom f holds
( ( f . y = {} implies h2 . y = {} ) & ( f . y <> {} implies h2 . y = (curry' g2) . y ) ) by A3, A5;
A14: ex f1 being Function st
( x = f1 & dom f1 = Union (disjoin f) & rng f1 c= X ) by A3, A4, FUNCT_2:def_2;
now__::_thesis:_for_z_being_set_st_z_in_Union_(disjoin_f)_holds_
g1_._z_=_g2_._z
let z be set ; ::_thesis: ( z in Union (disjoin f) implies g1 . z = g2 . z )
assume A15: z in Union (disjoin f) ; ::_thesis: g1 . z = g2 . z
then A16: z = [(z `1),(z `2)] by CARD_3:22;
A17: ( z `2 in dom f & z `1 in f . (z `2) ) by A15, CARD_3:22;
then A18: h2 . (z `2) = (curry' g2) . (z `2) by A13;
then reconsider g91 = h1 . (z `2), g92 = h2 . (z `2) as Function by A6, A7, A9, A11, A12, A15, A16, FUNCT_5:21;
A19: g2 . ((z `1),(z `2)) = g92 . (z `1) by A7, A11, A15, A16, A18, FUNCT_5:22;
 h1 . (z `2) = (curry' g1) . (z `2) by A10, A17;
then  g1 . ((z `1),(z `2)) = g91 . (z `1) by A14, A8, A15, A16, FUNCT_5:22;
hence  g1 . z = g2 . z by A6, A9, A12, A16, A19; ::_thesis: verum
end;
hence  x = y by A14, A7, A8, A11, FUNCT_1:2; ::_thesis: verum
end;
thus  dom F = Funcs ((Union (disjoin f)),X) by A3; ::_thesis: rng F = product (Funcs (f,X))
thus  rng F c= product (Funcs (f,X)) :: according to XBOOLE_0:def_10 ::_thesis: product (Funcs (f,X)) c= rng F
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng F or y in product (Funcs (f,X)) )
assume  y in rng F ; ::_thesis: y in product (Funcs (f,X))
then consider x being set  such that
A20: x in dom F and
A21: y = F . x by FUNCT_1:def_3;
consider g, h being Function such that
A22: x = g and
A23: F . x = h and
A24: dom h = dom f and
A25: for y being set st y in dom f holds
( ( f . y = {} implies h . y = {} ) & ( f . y <> {} implies h . y = (curry' g) . y ) ) by A3, A20;
A26: ex f1 being Function st
( x = f1 & dom f1 = Union (disjoin f) & rng f1 c= X ) by A3, A20, FUNCT_2:def_2;
A27: now__::_thesis:_for_z_being_set_st_z_in_dom_(Funcs_(f,X))_holds_
h_._z_in_(Funcs_(f,X))_._z
let z be set ; ::_thesis: ( z in dom (Funcs (f,X)) implies h . z in (Funcs (f,X)) . z )
assume  z in dom (Funcs (f,X)) ; ::_thesis: h . z in (Funcs (f,X)) . z
then A28: z in dom f by Def8;
then A29: (Funcs (f,X)) . z = Funcs ((f . z),X) by Def8;
A30: now__::_thesis:_(_f_._z_<>_{}_implies_h_._z_in_(Funcs_(f,X))_._z_)
set a = the Element of f . z;
assume A31: f . z <> {} ; ::_thesis: h . z in (Funcs (f,X)) . z
 ( [ the Element of f . z,z] `1 = the Element of f . z & [ the Element of f . z,z] `2 = z ) ;
then A32: [ the Element of f . z,z] in Union (disjoin f) by A28, A31, CARD_3:22;
then reconsider k = (curry' g) . z as Function by A22, A26, FUNCT_5:21;
A33: z in dom (curry' g) by A22, A26, A32, FUNCT_5:21;
then  rng k c= rng g by FUNCT_5:34;
then A34: rng k c= X by A22, A26, XBOOLE_1:1;
A35: dom k = proj1 ((dom g) /\ [:(proj1 (dom g)),{z}:]) by A33, FUNCT_5:34;
A36: dom k = f . z
proof
thus  dom k c= f . z :: according to XBOOLE_0:def_10 ::_thesis: f . z c= dom k
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in dom k or b in f . z )
assume  b in dom k ; ::_thesis: b in f . z
then consider c being set  such that
A37: [b,c] in (dom g) /\ [:(proj1 (dom g)),{z}:] by A35, XTUPLE_0:def_12;
 [b,c] in [:(proj1 (dom g)),{z}:] by A37, XBOOLE_0:def_4;
then A38: c in {z} by ZFMISC_1:87;
A39: ( [b,c] `1 = b & [b,c] `2 = c ) ;
 [b,c] in dom g by A37, XBOOLE_0:def_4;
then  b in f . c by A22, A26, A39, CARD_3:22;
hence  b in f . z by A38, TARSKI:def_1; ::_thesis: verum
end;
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in f . z or b in dom k )
assume A40: b in f . z ; ::_thesis: b in dom k
A41: z in {z} by TARSKI:def_1;
 ( [b,z] `1 = b & [b,z] `2 = z ) ;
then A42: [b,z] in dom g by A22, A26, A28, A40, CARD_3:22;
then  b in proj1 (dom g) by XTUPLE_0:def_12;
then  [b,z] in [:(proj1 (dom g)),{z}:] by A41, ZFMISC_1:87;
then  [b,z] in (dom g) /\ [:(proj1 (dom g)),{z}:] by A42, XBOOLE_0:def_4;
hence  b in dom k by A35, XTUPLE_0:def_12; ::_thesis: verum
end;
 h . z = k by A25, A28, A31;
hence  h . z in (Funcs (f,X)) . z by A29, A34, A36, FUNCT_2:def_2; ::_thesis: verum
end;
now__::_thesis:_(_f_._z_=_{}_implies_h_._z_in_(Funcs_(f,X))_._z_)
assume  f . z = {} ; ::_thesis: h . z in (Funcs (f,X)) . z
then  ( h . z = {} & (Funcs (f,X)) . z = {{}} ) by A25, A28, A29, FUNCT_5:57;
hence  h . z in (Funcs (f,X)) . z by TARSKI:def_1; ::_thesis: verum
end;
hence  h . z in (Funcs (f,X)) . z by A30; ::_thesis: verum
end;
 dom h = dom (Funcs (f,X)) by A24, Def8;
hence  y in product (Funcs (f,X)) by A21, A23, A27, CARD_3:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in product (Funcs (f,X)) or x in rng F )
assume  x in product (Funcs (f,X)) ; ::_thesis: x in rng F
then consider s being Function such that
A43: x = s and
A44: dom s = dom (Funcs (f,X)) and
A45: for z being set st z in dom (Funcs (f,X)) holds
s . z in (Funcs (f,X)) . z by CARD_3:def_5;
A46: dom s = dom f by A44, Def8;
A47: uncurry' s = ~ (uncurry s) by FUNCT_5:def_4;
A48: dom (uncurry' s) = Union (disjoin f)
proof
thus  dom (uncurry' s) c= Union (disjoin f) :: according to XBOOLE_0:def_10 ::_thesis: Union (disjoin f) c= dom (uncurry' s)
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in dom (uncurry' s) or z in Union (disjoin f) )
assume A49: z in dom (uncurry' s) ; ::_thesis: z in Union (disjoin f)
then consider z1, z2 being set  such that
A50: z = [z1,z2] by A47, Th2;
A51: ( z `1 = z1 & z `2 = z2 ) by A50, MCART_1:7;
 [z2,z1] in dom (uncurry s) by A47, A49, A50, FUNCT_4:42;
then consider a being set , u being Function, b being set  such that
A52: [z2,z1] = [a,b] and
A53: a in dom s and
A54: u = s . a and
A55: b in dom u by FUNCT_5:def_2;
A56: ( [a,b] `1 = a & [z2,z1] `1 = z2 ) ;
 ( u in (Funcs (f,X)) . a & (Funcs (f,X)) . a = Funcs ((f . a),X) ) by A44, A45, A46, A53, A54, Def8;
then A57: ex j being Function st
( u = j & dom j = f . z2 & rng j c= X ) by A52, A56, FUNCT_2:def_2;
 ( [a,b] `2 = b & [z2,z1] `2 = z1 ) ;
hence  z in Union (disjoin f) by A46, A50, A52, A53, A55, A51, A56, A57, CARD_3:22; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Union (disjoin f) or z in dom (uncurry' s) )
assume A58: z in Union (disjoin f) ; ::_thesis: z in dom (uncurry' s)
then A59: ( z `1 in f . (z `2) & z = [(z `1),(z `2)] ) by CARD_3:22;
A60: z `2 in dom f by A58, CARD_3:22;
then  ( s . (z `2) in (Funcs (f,X)) . (z `2) & (Funcs (f,X)) . (z `2) = Funcs ((f . (z `2)),X) ) by A44, A45, A46, Def8;
then  ex j being Function st
( s . (z `2) = j & dom j = f . (z `2) & rng j c= X ) by FUNCT_2:def_2;
hence  z in dom (uncurry' s) by A46, A60, A59, FUNCT_5:39; ::_thesis: verum
end;
 rng (uncurry' s) c= X
proof
let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in rng (uncurry' s) or d in X )
assume  d in rng (uncurry' s) ; ::_thesis: d in X
then consider z being set  such that
A61: z in dom (uncurry' s) and
A62: d = (uncurry' s) . z by FUNCT_1:def_3;
consider z1, z2 being set  such that
A63: z = [z1,z2] by A47, A61, Th2;
 [z2,z1] in dom (uncurry s) by A47, A61, A63, FUNCT_4:42;
then consider a being set , u being Function, b being set  such that
A64: [z2,z1] = [a,b] and
A65: ( a in dom s & u = s . a ) and
A66: b in dom u by FUNCT_5:def_2;
A67: ( [a,b] `1 = a & [z2,z1] `1 = z2 ) ;
 ( u in (Funcs (f,X)) . a & (Funcs (f,X)) . a = Funcs ((f . a),X) ) by A44, A45, A46, A65, Def8;
then A68: ex j being Function st
( u = j & dom j = f . z2 & rng j c= X ) by A64, A67, FUNCT_2:def_2;
A69: ( [a,b] `2 = b & [z2,z1] `2 = z1 ) ;
 (uncurry' s) . (b,a) = u . b by A65, A66, FUNCT_5:39;
then  d in rng u by A62, A63, A64, A66, A67, A69, FUNCT_1:def_3;
hence  d in X by A68; ::_thesis: verum
end;
then A70: uncurry' s in dom F by A3, A48, FUNCT_2:def_2;
then consider g, h being Function such that
A71: uncurry' s = g and
A72: F . (uncurry' s) = h and
A73: dom h = dom f and
A74: for y being set st y in dom f holds
( ( f . y = {} implies h . y = {} ) & ( f . y <> {} implies h . y = (curry' g) . y ) ) by A3;
now__::_thesis:_for_z_being_set_st_z_in_dom_f_holds_
s_._z_=_h_._z
let z be set ; ::_thesis: ( z in dom f implies s . z = h . z )
assume A75: z in dom f ; ::_thesis: s . z = h . z
then  ( s . z in (Funcs (f,X)) . z & (Funcs (f,X)) . z = Funcs ((f . z),X) ) by A44, A45, A46, Def8;
then consider v being Function such that
A76: s . z = v and
A77: dom v = f . z and
 rng v c= X by FUNCT_2:def_2;
A78: now__::_thesis:_(_f_._z_<>_{}_implies_s_._z_=_h_._z_)
set a = the Element of f . z;
assume A79: f . z <> {} ; ::_thesis: s . z = h . z
then A80: [ the Element of f . z,z] in dom (uncurry' s) by A46, A75, A76, A77, FUNCT_5:39;
then reconsider j = (curry' (uncurry' s)) . z as Function by FUNCT_5:21;
A81: j = (curry (~ (uncurry' s))) . z by FUNCT_5:def_3;
A82: ~ (uncurry' s) = uncurry s by Th4;
then A83: [z, the Element of f . z] in dom (uncurry s) by A80, FUNCT_4:42;
A84: dom j = dom v
proof
thus  dom j c= dom v :: according to XBOOLE_0:def_10 ::_thesis: dom v c= dom j
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in dom j or b in dom v )
assume  b in dom j ; ::_thesis: b in dom v
then  [z,b] in dom (uncurry s) by A81, A82, A83, Lm4;
then consider a1 being set , g1 being Function, a2 being set  such that
A85: [z,b] = [a1,a2] and
 a1 in dom s and
A86: ( g1 = s . a1 & a2 in dom g1 ) by FUNCT_5:def_2;
 z = a1 by A85, XTUPLE_0:1;
hence  b in dom v by A76, A85, A86, XTUPLE_0:1; ::_thesis: verum
end;
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in dom v or b in dom j )
assume  b in dom v ; ::_thesis: b in dom j
then  [z,b] in dom (uncurry s) by A46, A75, A76, FUNCT_5:38;
hence  b in dom j by A81, A82, FUNCT_5:20; ::_thesis: verum
end;
now__::_thesis:_for_b_being_set_st_b_in_f_._z_holds_
j_._b_=_v_._b
let b be set ; ::_thesis: ( b in f . z implies j . b = v . b )
assume  b in f . z ; ::_thesis: j . b = v . b
then A87: [z,b] in dom (uncurry s) by A77, A81, A82, A83, A84, Lm4;
then consider a1 being set , g1 being Function, a2 being set  such that
A88: [z,b] = [a1,a2] and
A89: ( a1 in dom s & g1 = s . a1 & a2 in dom g1 ) by FUNCT_5:def_2;
A90: j . b = (uncurry s) . (z,b) by A81, A82, A87, FUNCT_5:20;
 ( z = a1 & b = a2 ) by A88, XTUPLE_0:1;
hence  j . b = v . b by A76, A89, A90, FUNCT_5:38; ::_thesis: verum
end;
then  v = j by A77, A84, FUNCT_1:2;
hence  s . z = h . z by A71, A74, A75, A76, A79; ::_thesis: verum
end;
 ( f . z = {} implies ( s . z = {} & h . z = {} ) ) by A74, A75, A76, A77;
hence  s . z = h . z by A78; ::_thesis: verum
end;
then  h = s by A46, A73, FUNCT_1:2;
hence  x in rng F by A43, A70, A72, FUNCT_1:def_3; ::_thesis: verum
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
deffunc H1( set ) ->  set = Funcs (X,(f . $1));
 ex F being Function st
( dom F = dom f & ( for x being set st x in dom f holds
F . x = H1(x) ) ) from FUNCT_1:sch_3();
hence  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)) ) ) ; ::_thesis: verum
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
let f1, f2 be Function; ::_thesis: ( dom f1 = dom f & ( for x being set st x in dom f holds
f1 . x = Funcs (X,(f . x)) ) & dom f2 = dom f & ( for x being set st x in dom f holds
f2 . x = Funcs (X,(f . x)) ) implies f1 = f2 )
assume that
A1: dom f1 = dom f and
A2: for x being set st x in dom f holds
f1 . x = Funcs (X,(f . x)) and
A3: dom f2 = dom f and
A4: for x being set st x in dom f holds
f2 . x = Funcs (X,(f . x)) ; ::_thesis: f1 = f2
now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_
f1_._x_=_f2_._x
let x be set ; ::_thesis: ( x in dom f implies f1 . x = f2 . x )
assume A5: x in dom f ; ::_thesis: f1 . x = f2 . x
then  f1 . x = Funcs (X,(f . x)) by A2;
hence  f1 . x = f2 . x by A4, A5; ::_thesis: verum
end;
hence  f1 = f2 by A1, A3, FUNCT_1:2; ::_thesis: verum
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
let X be set ; ::_thesis: for f being Function st f <> {} & X <> {} holds
product (Funcs (X,f)), Funcs (X,(product f)) are_equipotent
let f be Function; ::_thesis: ( f <> {} & X <> {} implies product (Funcs (X,f)), Funcs (X,(product f)) are_equipotent )
defpred S1[ set , set ] means  ex g being Function st
( $1 = g & $2 = <:g:> );
assume that
A1: f <> {} and
A2: X <> {} ; ::_thesis: product (Funcs (X,f)), Funcs (X,(product f)) are_equipotent
A3: for x being set st x in product (Funcs (X,f)) holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in product (Funcs (X,f)) implies ex y being set st S1[x,y] )
assume  x in product (Funcs (X,f)) ; ::_thesis: ex y being set st S1[x,y]
then  ex g being Function st
( x = g & dom g = dom (Funcs (X,f)) & ( for x being set st x in dom (Funcs (X,f)) holds
g . x in (Funcs (X,f)) . x ) ) by CARD_3:def_5;
then reconsider g = x as Function ;
reconsider y = <:g:> as set ;
take  y ; ::_thesis: S1[x,y]
take  g ; ::_thesis: ( x = g & y = <:g:> )
thus  ( x = g & y = <:g:> ) ; ::_thesis: verum
end;
consider F being Function such that
A4: ( dom F = product (Funcs (X,f)) & ( for x being set st x in product (Funcs (X,f)) holds
S1[x,F . x] ) ) from CLASSES1:sch_1(A3);
take  F ; :: according to WELLORD2:def_4 ::_thesis: ( F is one-to-one & dom F = product (Funcs (X,f)) & rng F = Funcs (X,(product f)) )
A5: for g being Function st g in product (Funcs (X,f)) holds
( dom <:g:> = X & SubFuncs (rng g) = rng g & rng <:g:> c= product f )
proof
let g be Function; ::_thesis: ( g in product (Funcs (X,f)) implies ( dom <:g:> = X & SubFuncs (rng g) = rng g & rng <:g:> c= product f ) )
A6: g " (rng g) = dom g by RELAT_1:134;
A7: dom (Funcs (X,f)) = dom f by Def9;
assume A8: g in product (Funcs (X,f)) ; ::_thesis: ( dom <:g:> = X & SubFuncs (rng g) = rng g & rng <:g:> c= product f )
then A9: dom g = dom (Funcs (X,f)) by CARD_3:9;
A10: now__::_thesis:_for_a_being_set_st_a_in_rng_g_holds_
a_is_Function
let a be set ; ::_thesis: ( a in rng g implies a is Function )
assume  a in rng g ; ::_thesis: a is Function
then consider z being set  such that
A11: z in dom g and
A12: a = g . z by FUNCT_1:def_3;
 ( g . z in (Funcs (X,f)) . z & (Funcs (X,f)) . z = Funcs (X,(f . z)) ) by A8, A9, A7, A11, Def9, CARD_3:9;
hence  a is Function by A12; ::_thesis: verum
end;
then A13: SubFuncs (rng g) = rng g by Lm1;
A14: now__::_thesis:_for_z_being_set_st_z_in_dom_f_holds_
((dom_f)_-->_X)_._z_=_proj1_(g_._z)
let z be set ; ::_thesis: ( z in dom f implies ((dom f) --> X) . z = proj1 (g . z) )
assume A15: z in dom f ; ::_thesis: ((dom f) --> X) . z = proj1 (g . z)
then  ( g . z in (Funcs (X,f)) . z & (Funcs (X,f)) . z = Funcs (X,(f . z)) ) by A8, A7, Def9, CARD_3:9;
then  ex h being Function st
( g . z = h & dom h = X & rng h c= f . z ) by FUNCT_2:def_2;
hence  ((dom f) --> X) . z = proj1 (g . z) by A15, FUNCOP_1:7; ::_thesis: verum
end;
 dom ((dom f) --> X) = dom f by FUNCOP_1:13;
then  doms g = (dom f) --> X by A9, A7, A13, A6, A14, Def2;
then  meet (doms g) = X by A1, Th27;
hence A16: ( dom <:g:> = X & SubFuncs (rng g) = rng g ) by A10, Lm1, Th29; ::_thesis: rng <:g:> c= product f
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng <:g:> or y in product f )
assume  y in rng <:g:> ; ::_thesis: y in product f
then consider x being set  such that
A17: x in dom <:g:> and
A18: y = <:g:> . x by FUNCT_1:def_3;
reconsider h = y as Function by A17, A18, Th30;
A19: dom h = dom f by A9, A7, A13, A6, A17, A18, Th31;
now__::_thesis:_for_z_being_set_st_z_in_dom_f_holds_
h_._z_in_f_._z
let z be set ; ::_thesis: ( z in dom f implies h . z in f . z )
assume A20: z in dom f ; ::_thesis: h . z in f . z
then A21: (uncurry g) . (z,x) = h . z by A17, A18, A19, Th31;
 ( g . z in (Funcs (X,f)) . z & (Funcs (X,f)) . z = Funcs (X,(f . z)) ) by A8, A7, A20, Def9, CARD_3:9;
then consider j being Function such that
A22: g . z = j and
A23: dom j = X and
A24: rng j c= f . z by FUNCT_2:def_2;
A25: j . x in rng j by A16, A17, A23, FUNCT_1:def_3;
 (uncurry g) . (z,x) = j . x by A9, A7, A16, A17, A20, A22, A23, FUNCT_5:38;
hence  h . z in f . z by A24, A21, A25; ::_thesis: verum
end;
hence  y in product f by A19, CARD_3:def_5; ::_thesis: verum
end;
thus  F is one-to-one ::_thesis: ( dom F = product (Funcs (X,f)) & rng F = Funcs (X,(product f)) )
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in dom F or not b1 in dom F or not F . x = F . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in dom F or not y in dom F or not F . x = F . y or x = y )
assume that
A26: x in dom F and
A27: y in dom F and
A28: F . x = F . y and
A29: x <> y ; ::_thesis: contradiction
consider gy being Function such that
A30: y = gy and
A31: F . y = <:gy:> by A4, A27;
consider gx being Function such that
A32: x = gx and
A33: F . x = <:gx:> by A4, A26;
A34: dom gx = dom (Funcs (X,f)) by A4, A26, A32, CARD_3:9;
A35: dom (Funcs (X,f)) = dom f by Def9;
A36: dom gy = dom (Funcs (X,f)) by A4, A27, A30, CARD_3:9;
now__::_thesis:_for_z_being_set_st_z_in_dom_f_holds_
gx_._z_=_gy_._z
let z be set ; ::_thesis: ( z in dom f implies gx . z = gy . z )
assume A37: z in dom f ; ::_thesis: gx . z = gy . z
then A38: (Funcs (X,f)) . z = Funcs (X,(f . z)) by Def9;
 gy . z in (Funcs (X,f)) . z by A4, A27, A30, A35, A37, CARD_3:9;
then consider hy being Function such that
A39: ( gy . z = hy & dom hy = X ) and
 rng hy c= f . z by A38, FUNCT_2:def_2;
 gx . z in (Funcs (X,f)) . z by A4, A26, A32, A35, A37, CARD_3:9;
then consider hx being Function such that
A40: ( gx . z = hx & dom hx = X ) and
 rng hx c= f . z by A38, FUNCT_2:def_2;
A41: dom <:gx:> = X by A4, A5, A26, A32;
A42: ( SubFuncs (rng gx) = rng gx & gx " (rng gx) = dom gx ) by A4, A5, A26, A32, RELAT_1:134;
now__::_thesis:_for_b_being_set_st_b_in_X_holds_
hx_._b_=_hy_._b
let b be set ; ::_thesis: ( b in X implies hx . b = hy . b )
assume A43: b in X ; ::_thesis: hx . b = hy . b
then reconsider fx = <:gx:> . b as Function by A41, Th30;
A44: ( (uncurry gx) . (z,b) = hx . b & (uncurry gy) . (z,b) = hy . b ) by A34, A36, A35, A37, A40, A39, A43, FUNCT_5:38;
A45: dom fx = dom gx by A41, A42, A43, Th31;
then  fx . z = (uncurry gx) . (z,b) by A34, A35, A37, A41, A43, Th31;
hence  hx . b = hy . b by A28, A33, A31, A34, A35, A37, A41, A43, A45, A44, Th31; ::_thesis: verum
end;
hence  gx . z = gy . z by A40, A39, FUNCT_1:2; ::_thesis: verum
end;
hence  contradiction by A29, A32, A30, A34, A36, A35, FUNCT_1:2; ::_thesis: verum
end;
thus  dom F = product (Funcs (X,f)) by A4; ::_thesis: rng F = Funcs (X,(product f))
thus  rng F c= Funcs (X,(product f)) :: according to XBOOLE_0:def_10 ::_thesis: Funcs (X,(product f)) c= rng F
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng F or y in Funcs (X,(product f)) )
assume  y in rng F ; ::_thesis: y in Funcs (X,(product f))
then consider x being set  such that
A46: x in dom F and
A47: y = F . x by FUNCT_1:def_3;
consider g being Function such that
A48: x = g and
A49: y = <:g:> by A4, A46, A47;
 ( dom <:g:> = X & rng <:g:> c= product f ) by A4, A5, A46, A48;
hence  y in Funcs (X,(product f)) by A49, FUNCT_2:def_2; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Funcs (X,(product f)) or y in rng F )
assume  y in Funcs (X,(product f)) ; ::_thesis: y in rng F
then consider h being Function such that
A50: y = h and
A51: dom h = X and
A52: rng h c= product f by FUNCT_2:def_2;
set g = <:h:>;
A53: h " (rng h) = dom h by RELAT_1:134;
A54: now__::_thesis:_for_z_being_set_st_z_in_X_holds_
(X_-->_(dom_f))_._z_=_(doms_h)_._z
let z be set ; ::_thesis: ( z in X implies (X --> (dom f)) . z = (doms h) . z )
assume A55: z in X ; ::_thesis: (X --> (dom f)) . z = (doms h) . z
then  h . z in rng h by A51, FUNCT_1:def_3;
then A56: ex j being Function st
( h . z = j & dom j = dom f & ( for x being set st x in dom f holds
j . x in f . x ) ) by A52, CARD_3:def_5;
thus (X --> (dom f)) . z = dom f by A55, FUNCOP_1:7
.= (doms h) . z by A51, A55, A56, Th22 ; ::_thesis: verum
end;
A57: meet (doms h) = dom <:h:> by Th29;
now__::_thesis:_for_z_being_set_st_z_in_rng_h_holds_
z_is_Function
let z be set ; ::_thesis: ( z in rng h implies z is Function )
assume  z in rng h ; ::_thesis: z is Function
then  ex j being Function st
( z = j & dom j = dom f & ( for x being set st x in dom f holds
j . x in f . x ) ) by A52, CARD_3:def_5;
hence  z is Function ; ::_thesis: verum
end;
then A58: SubFuncs (rng h) = rng h by Lm1;
 ( dom (doms h) = h " (SubFuncs (rng h)) & dom ((dom h) --> (dom f)) = dom h ) by Def2, FUNCOP_1:13;
then  X --> (dom f) = doms h by A51, A58, A53, A54, FUNCT_1:2;
then A59: dom <:h:> = dom f by A2, A57, Th27;
A60: now__::_thesis:_for_z_being_set_st_z_in_dom_f_holds_
<:h:>_._z_in_(Funcs_(X,f))_._z
let z be set ; ::_thesis: ( z in dom f implies <:h:> . z in (Funcs (X,f)) . z )
assume A61: z in dom f ; ::_thesis: <:h:> . z in (Funcs (X,f)) . z
then reconsider i = <:h:> . z as Function by A59, Th30;
A62: dom i = X by A51, A58, A53, A59, A61, Th31;
 rng i c= f . z
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng i or x in f . z )
assume  x in rng i ; ::_thesis: x in f . z
then consider a being set  such that
A63: a in dom i and
A64: x = i . a by FUNCT_1:def_3;
 h . a in rng h by A51, A62, A63, FUNCT_1:def_3;
then consider j being Function such that
A65: ( h . a = j & dom j = dom f ) and
A66: for x being set st x in dom f holds
j . x in f . x by A52, CARD_3:def_5;
i . a = (uncurry h) . (a,z) by A59, A61, A63, Th31
.= j . z by A51, A61, A62, A63, A65, FUNCT_5:38 ;
hence  x in f . z by A61, A64, A66; ::_thesis: verum
end;
then  <:h:> . z in Funcs (X,(f . z)) by A62, FUNCT_2:def_2;
hence  <:h:> . z in (Funcs (X,f)) . z by A61, Def9; ::_thesis: verum
end;
A67: meet (doms <:h:>) = dom <:<:h:>:> by Th29;
 product f c= Funcs ((dom f),(Union f)) by Th1;
then A68: rng h c= Funcs ((dom f),(Union f)) by A52, XBOOLE_1:1;
then A69: dom (uncurry h) = [:(dom h),(dom f):] by FUNCT_5:26;
 dom f = dom (Funcs (X,f)) by Def9;
then A70: <:h:> in product (Funcs (X,f)) by A59, A60, CARD_3:def_5;
then A71: ex g9 being Function st
( <:h:> = g9 & F . <:h:> = <:g9:> ) by A4;
 dom (uncurry' h) = [:(dom f),(dom h):] by A68, FUNCT_5:26;
then A72: (uncurry' h) | [:(meet (doms h)),(dom h):] = uncurry' h by A57, A59, RELAT_1:68;
A73: ( uncurry' h = ~ (uncurry h) & curry (~ (uncurry h)) = curry' (uncurry h) ) by FUNCT_5:def_3, FUNCT_5:def_4;
 dom <:<:h:>:> = X by A5, A70;
then A74: (uncurry h) | [:(meet (doms <:h:>)),(dom <:h:>):] = uncurry h by A51, A59, A69, A67, RELAT_1:68;
 uncurry' (curry' (uncurry h)) = uncurry h by A69, FUNCT_5:49;
then  <:<:h:>:> = h by A1, A68, A72, A74, A73, FUNCT_5:48;
hence  y in rng F by A4, A50, A70, A71, FUNCT_1:def_3; ::_thesis: verum
end;

theorem Th50: :: FUNCT_6:50
for f being Function holds Funcs ({},f) = (dom f) --> {{}}
proof
let f be Function; ::_thesis: Funcs ({},f) = (dom f) --> {{}}
A1: now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_
(Funcs_({},f))_._x_=_{{}}
let x be set ; ::_thesis: ( x in dom f implies (Funcs ({},f)) . x = {{}} )
assume  x in dom f ; ::_thesis: (Funcs ({},f)) . x = {{}}
hence (Funcs ({},f)) . x = Funcs ({},(f . x)) by Def9
.= {{}} by FUNCT_5:57 ;
::_thesis: verum
end;
 dom (Funcs ({},f)) = dom f by Def9;
hence  Funcs ({},f) = (dom f) --> {{}} by A1, FUNCOP_1:11; ::_thesis: verum
end;

theorem Th51: :: FUNCT_6:51
for X being set holds Funcs (X,{}) = {}
proof
let X be set ; ::_thesis: Funcs (X,{}) = {}
 dom (Funcs (X,{})) = dom {} by Def9;
hence  Funcs (X,{}) = {} ; ::_thesis: verum
end;

theorem :: FUNCT_6:52
for X, Y, Z being set holds Funcs (X,(Y --> Z)) = Y --> (Funcs (X,Z))
proof
let X, Y, Z be set ; ::_thesis: Funcs (X,(Y --> Z)) = Y --> (Funcs (X,Z))
A1: Y = dom (Y --> Z) by FUNCOP_1:13;
A2: now__::_thesis:_for_x_being_set_st_x_in_Y_holds_
(Funcs_(X,(Y_-->_Z)))_._x_=_Funcs_(X,Z)
let x be set ; ::_thesis: ( x in Y implies (Funcs (X,(Y --> Z))) . x = Funcs (X,Z) )
assume A3: x in Y ; ::_thesis: (Funcs (X,(Y --> Z))) . x = Funcs (X,Z)
then  (Funcs (X,(Y --> Z))) . x = Funcs (X,((Y --> Z) . x)) by A1, Def9;
hence  (Funcs (X,(Y --> Z))) . x = Funcs (X,Z) by A3, FUNCOP_1:7; ::_thesis: verum
end;
 dom (Funcs (X,(Y --> Z))) = dom (Y --> Z) by Def9;
hence  Funcs (X,(Y --> Z)) = Y --> (Funcs (X,Z)) by A1, A2, FUNCOP_1:11; ::_thesis: verum
end;

theorem :: FUNCT_6:53
for X being set
for f being Function holds product (Funcs (X,f)), Funcs (X,(product f)) are_equipotent
proof
let X be set ; ::_thesis: for f being Function holds product (Funcs (X,f)), Funcs (X,(product f)) are_equipotent
let f be Function; ::_thesis: product (Funcs (X,f)), Funcs (X,(product f)) are_equipotent
A1: Funcs (X,(product {})) = {(X --> {})} by CARD_3:10, FUNCT_5:59;
A2: product (Funcs ({},f)) = product ((dom f) --> {{}}) by Th50
.= Funcs ((dom f),{{}}) by CARD_3:11
.= {((dom f) --> {})} by FUNCT_5:59 ;
A3: ( Funcs ({},(product f)) = {{}} & product (Funcs (X,{})) = {{}} ) by Th51, CARD_3:10, FUNCT_5:57;
 ( X <> {} & f <> {} implies product (Funcs (X,f)), Funcs (X,(product f)) are_equipotent ) by Lm5;
hence  product (Funcs (X,f)), Funcs (X,(product f)) are_equipotent by A2, A3, A1, CARD_1:28; ::_thesis: verum
end;

begin

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
proof
set g = curry' (uncurry f);
 for x being set st x in dom (curry' (uncurry f)) holds
(curry' (uncurry f)) . x is Function by FUNCT_5:33;
hence  curry' (uncurry f) is Function-yielding Function by FUNCOP_1:def_6; ::_thesis: verum
end;
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 <> {} & B <> {} & f in Funcs (A,(Funcs (B,C))) holds
commute f in Funcs (B,(Funcs (A,C)))
proof
let A, B, C be set ; ::_thesis: for f being Function st A <> {} & B <> {} & f in Funcs (A,(Funcs (B,C))) holds
commute f in Funcs (B,(Funcs (A,C)))
let f be Function; ::_thesis: ( A <> {} & B <> {} & f in Funcs (A,(Funcs (B,C))) implies commute f in Funcs (B,(Funcs (A,C))) )
assume  ( A <> {} & B <> {} & f in Funcs (A,(Funcs (B,C))) ) ; ::_thesis: commute f in Funcs (B,(Funcs (A,C)))
then  ( [:A,B:] <> {} & uncurry f in Funcs ([:A,B:],C) ) by Th11, ZFMISC_1:90;
hence  commute f in Funcs (B,(Funcs (A,C))) by Th10; ::_thesis: verum
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 )
proof
let A, B, C be set ; ::_thesis: 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 )
let f be Function; ::_thesis: ( A <> {} & B <> {} & f in Funcs (A,(Funcs (B,C))) implies 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 ) )
assume that
A1: ( A <> {} & B <> {} ) and
A2: f in Funcs (A,(Funcs (B,C))) ; ::_thesis: 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 )
set uf = uncurry f;
set cf = commute f;
let g, h be Function; ::_thesis: 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 )
let x, y be set ; ::_thesis: ( x in A & y in B & f . x = g & (commute f) . y = h implies ( h . x = g . y & dom h = A & dom g = B & rng h c= C & rng g c= C ) )
assume that
A3: x in A and
A4: y in B and
A5: f . x = g and
A6: (commute f) . y = h ; ::_thesis: ( h . x = g . y & dom h = A & dom g = B & rng h c= C & rng g c= C )
 commute f in Funcs (B,(Funcs (A,C))) by A1, A2, Th55;
then A7: ex g being Function st
( g = commute f & dom g = B & rng g c= Funcs (A,C) ) by FUNCT_2:def_2;
then  (commute f) . y in rng (commute f) by A4, FUNCT_1:def_3;
then A8: ex t being Function st
( t = h & dom t = A & rng t c= C ) by A6, A7, FUNCT_2:def_2;
A9: ex g being Function st
( g = f & dom g = A & rng g c= Funcs (B,C) ) by A2, FUNCT_2:def_2;
then  f . x in rng f by A3, FUNCT_1:def_3;
then A10: ex t being Function st
( t = g & dom t = B & rng t c= C ) by A5, A9, FUNCT_2:def_2;
then  ( [x,y] in dom (uncurry f) & (uncurry f) . (x,y) = g . y ) by A3, A4, A5, A9, FUNCT_5:38;
hence  ( h . x = g . y & dom h = A & dom g = B & rng h c= C & rng g c= C ) by A6, A10, A8, FUNCT_5:22; ::_thesis: verum
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
proof
let A, B, C be set ; ::_thesis: for f being Function st A <> {} & B <> {} & f in Funcs (A,(Funcs (B,C))) holds
commute (commute f) = f
let f be Function; ::_thesis: ( A <> {} & B <> {} & f in Funcs (A,(Funcs (B,C))) implies commute (commute f) = f )
assume that
A1: ( A <> {} & B <> {} ) and
A2: f in Funcs (A,(Funcs (B,C))) ; ::_thesis: commute (commute f) = f
A3: ex g being Function st
( g = f & dom g = A & rng g c= Funcs (B,C) ) by A2, FUNCT_2:def_2;
set cf = commute f;
A4: commute f in Funcs (B,(Funcs (A,C))) by A1, A2, Th55;
then  commute (commute f) in Funcs (A,(Funcs (B,C))) by A1, Th55;
then A5: ex h being Function st
( h = commute (commute f) & dom h = A & rng h c= Funcs (B,C) ) by FUNCT_2:def_2;
A6: ex g being Function st
( g = commute f & dom g = B & rng g c= Funcs (A,C) ) by A4, FUNCT_2:def_2;
 for x being set st x in A holds
f . x = (commute (commute f)) . x
proof
set ccf = commute (commute f);
set uf = uncurry f;
set ucf = uncurry (commute f);
let x be set ; ::_thesis: ( x in A implies f . x = (commute (commute f)) . x )
assume A7: x in A ; ::_thesis: f . x = (commute (commute f)) . x
then  f . x in rng f by A3, FUNCT_1:def_3;
then consider g being Function such that
A8: ( g = f . x & dom g = B ) and
 rng g c= C by A3, FUNCT_2:def_2;
 (commute (commute f)) . x in rng (commute (commute f)) by A5, A7, FUNCT_1:def_3;
then consider h being Function such that
A9: h = (commute (commute f)) . x and
A10: dom h = B and
 rng h c= C by A5, FUNCT_2:def_2;
A11: for y being set st y in B holds
for h being Function st h = (commute f) . y holds
( x in dom h & h . x = g . y )
proof
let y be set ; ::_thesis: ( y in B implies for h being Function st h = (commute f) . y holds
( x in dom h & h . x = g . y ) )
assume  y in B ; ::_thesis: for h being Function st h = (commute f) . y holds
( x in dom h & h . x = g . y )
then A12: ( [x,y] in dom (uncurry f) & (uncurry f) . (x,y) = g . y ) by A3, A7, A8, FUNCT_5:38;
let h be Function; ::_thesis: ( h = (commute f) . y implies ( x in dom h & h . x = g . y ) )
assume  h = (commute f) . y ; ::_thesis: ( x in dom h & h . x = g . y )
hence  ( x in dom h & h . x = g . y ) by A12, FUNCT_5:22; ::_thesis: verum
end;
A13: for y being set st y in B holds
( [y,x] in dom (uncurry (commute f)) & (uncurry (commute f)) . (y,x) = g . y )
proof
let y be set ; ::_thesis: ( y in B implies ( [y,x] in dom (uncurry (commute f)) & (uncurry (commute f)) . (y,x) = g . y ) )
reconsider h = (commute f) . y as Function ;
assume A14: y in B ; ::_thesis: ( [y,x] in dom (uncurry (commute f)) & (uncurry (commute f)) . (y,x) = g . y )
then  ( x in dom h & h . x = g . y ) by A11;
hence  ( [y,x] in dom (uncurry (commute f)) & (uncurry (commute f)) . (y,x) = g . y ) by A6, A14, FUNCT_5:38; ::_thesis: verum
end;
 for y being set st y in B holds
h . y = g . y
proof
let y be set ; ::_thesis: ( y in B implies h . y = g . y )
assume  y in B ; ::_thesis: h . y = g . y
then  ( [y,x] in dom (uncurry (commute f)) & (uncurry (commute f)) . (y,x) = g . y ) by A13;
hence  h . y = g . y by A9, FUNCT_5:22; ::_thesis: verum
end;
hence  f . x = (commute (commute f)) . x by A8, A9, A10, FUNCT_1:2; ::_thesis: verum
end;
hence  commute (commute f) = f by A3, A5, FUNCT_1:2; ::_thesis: verum
end;

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

theorem :: FUNCT_6:59
for f being Function-yielding Function holds dom (doms f) = dom f
proof
let f be Function-yielding Function; ::_thesis: dom (doms f) = dom f
thus  dom (doms f) c= dom f :: according to XBOOLE_0:def_10 ::_thesis: dom f c= dom (doms f)
proof
let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in dom (doms f) or i in dom f )
 dom (doms f) = f " (SubFuncs (rng f)) by Def2;
hence  ( not i in dom (doms f) or i in dom f ) by Th19; ::_thesis: verum
end;
thus  dom f c= dom (doms f) ::_thesis: verum
proof
let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in dom f or i in dom (doms f) )
assume A1: i in dom f ; ::_thesis: i in dom (doms f)
 ( f . i is Function & dom (doms f) = f " (SubFuncs (rng f)) ) by Def2;
hence  i in dom (doms f) by A1, Th19; ::_thesis: verum
end;
end;

theorem :: FUNCT_6:60
for f being Function-yielding Function holds dom (rngs f) = dom f
proof
let f be Function-yielding Function; ::_thesis: dom (rngs f) = dom f
thus  dom (rngs f) c= dom f :: according to XBOOLE_0:def_10 ::_thesis: dom f c= dom (rngs f)
proof
let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in dom (rngs f) or i in dom f )
 dom (rngs f) = f " (SubFuncs (rng f)) by Def3;
hence  ( not i in dom (rngs f) or i in dom f ) by Th19; ::_thesis: verum
end;
thus  dom f c= dom (rngs f) ::_thesis: verum
proof
let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in dom f or i in dom (rngs f) )
assume A1: i in dom f ; ::_thesis: i in dom (rngs f)
 ( f . i is Function & dom (rngs f) = f " (SubFuncs (rng f)) ) by Def3;
hence  i in dom (rngs f) by A1, Th19; ::_thesis: verum
end;
end;