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):] ) )
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) ; :: thesis: ( 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 ; :: thesis: ( 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 ) ) :: thesis: ( S1[t] implies t in [:(dom f),X:] )
proof
assume A3: t in [:(dom f),X:] ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: 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 ; :: 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 A3, A4, MCART_1:10, MCART_1:21; :: thesis: 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 ; :: thesis: 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; :: thesis: 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); :: thesis: dom (uncurry' f) = [:X,(dom f):]
hence dom (uncurry' f) = [:X,(dom f):] by FUNCT_4:46; :: thesis: verum