let X, Y be set ; for f being Function st rng f c= Funcs (X,Y) holds
( dom (uncurry f) = [:(dom f),X:] & dom (uncurry' f) = [:X,(dom f):] )
let f be Function; ( rng f c= Funcs (X,Y) implies ( dom (uncurry f) = [:(dom f),X:] & dom (uncurry' f) = [:X,(dom f):] ) )
defpred S1[ object ] means ex x being object ex g being Function ex y being object st
( $1 = [x,y] & x in dom f & g = f . x & y in dom g );
assume A1:
rng f c= Funcs (X,Y)
; ( dom (uncurry f) = [:(dom f),X:] & dom (uncurry' f) = [:X,(dom f):] )
A2:
for t being object holds
( t in [:(dom f),X:] iff S1[t] )
proof
let t be
object ;
( t in [:(dom f),X:] iff S1[t] )
thus
(
t in [:(dom f),X:] implies ex
x being
object ex
g being
Function ex
y being
object st
(
t = [x,y] &
x in dom f &
g = f . x &
y in dom g ) )
( S1[t] implies t in [:(dom f),X:] )proof
assume A3:
t in [:(dom f),X:]
;
ex x being object ex g being Function ex y being object st
( t = [x,y] & x in dom f & g = f . x & y in dom g )
then
t `1 in dom f
by MCART_1:10;
then
f . (t `1) in rng f
by FUNCT_1:def 3;
then consider g being
Function such that A4:
(
f . (t `1) = g &
dom g = X )
and
rng g c= Y
by A1, FUNCT_2:def 2;
take
t `1
;
ex g being Function ex y being object st
( t = [(t `1),y] & t `1 in dom f & g = f . (t `1) & y in dom g )
take
g
;
ex y being object st
( t = [(t `1),y] & t `1 in dom f & g = f . (t `1) & y in dom g )
take
t `2
;
( t = [(t `1),(t `2)] & t `1 in dom f & g = f . (t `1) & t `2 in dom g )
thus
(
t = [(t `1),(t `2)] &
t `1 in dom f &
g = f . (t `1) &
t `2 in dom g )
by A3, A4, MCART_1:10, MCART_1:21;
verum
end;
given x being
object ,
g being
Function,
y being
object such that A5:
t = [x,y]
and A6:
x in dom f
and A7:
g = f . x
and A8:
y in dom g
;
t in [:(dom f),X:]
g in rng f
by A6, A7, FUNCT_1:def 3;
then
ex
g1 being
Function st
(
g = g1 &
dom g1 = X &
rng g1 c= Y )
by A1, FUNCT_2:def 2;
hence
t in [:(dom f),X:]
by A5, A6, A8, ZFMISC_1:87;
verum
end;
A9:
for t being object holds
( t in dom (uncurry f) iff S1[t] )
by Def2;
thus
dom (uncurry f) = [:(dom f),X:]
from XBOOLE_0:sch 2(A9, A2); dom (uncurry' f) = [:X,(dom f):]
hence
dom (uncurry' f) = [:X,(dom f):]
by FUNCT_4:46; verum