let X, Y be set ; :: thesis: 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; :: thesis: ( rng f c= Funcs X,Y implies ( dom (uncurry f) = [:(dom f),X:] & dom (uncurry' f) = [:X,(dom f):] ) )
assume A1:
rng f c= Funcs X,Y
; :: thesis: ( dom (uncurry f) = [:(dom f),X:] & dom (uncurry' f) = [:X,(dom f):] )
defpred S1[ set ] means ex x being set ex g being Function ex y being set st
( $1 = [x,y] & x in dom f & g = f . x & y in dom g );
A2:
for t being set holds
( t in dom (uncurry f) iff S1[t] )
by Def4;
A3:
for t being set holds
( t in [:(dom f),X:] iff S1[t] )
proof
let t be
set ;
:: thesis: ( t in [:(dom f),X:] iff S1[t] )
thus
(
t in [:(dom f),X:] implies ex
x being
set ex
g being
Function ex
y being
set st
(
t = [x,y] &
x in dom f &
g = f . x &
y in dom g ) )
:: thesis: ( S1[t] implies t in [:(dom f),X:] )proof
assume A4:
t in [:(dom f),X:]
;
:: thesis: ex x being set ex g being Function ex y being set st
( t = [x,y] & x in dom f & g = f . x & y in dom g )
then
(
t = [(t `1 ),(t `2 )] &
t `1 in dom f &
t `2 in X )
by MCART_1:10, MCART_1:23;
then
f . (t `1 ) in rng f
by FUNCT_1:def 5;
then consider g being
Function such that A5:
(
f . (t `1 ) = g &
dom g = X &
rng g c= Y )
by A1, FUNCT_2:def 2;
take
t `1
;
:: thesis: ex g being Function ex y being set st
( t = [(t `1 ),y] & t `1 in dom f & g = f . (t `1 ) & y in dom g )
take
g
;
:: thesis: ex y being set st
( t = [(t `1 ),y] & t `1 in dom f & g = f . (t `1 ) & y in dom g )
take
t `2
;
:: thesis: ( 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 A4, A5, MCART_1:10, MCART_1:23;
:: thesis: verum
end;
given x being
set ,
g being
Function,
y being
set such that A6:
(
t = [x,y] &
x in dom f &
g = f . x &
y in dom g )
;
:: thesis: t in [:(dom f),X:]
g in rng f
by A6, FUNCT_1:def 5;
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 A6, ZFMISC_1:106;
:: thesis: verum
end;
thus
dom (uncurry f) = [:(dom f),X:]
from XBOOLE_0:sch 2(A2, A3); :: thesis: dom (uncurry' f) = [:X,(dom f):]
hence
dom (uncurry' f) = [:X,(dom f):]
by FUNCT_4:47; :: thesis: verum