let X, Y be set ; :: thesis: for y being object
for f being Function st [:X,Y:] <> {} & dom f = [:X,Y:] & y in Y holds
ex g being Function st
( (curry' f) . y = g & dom g = X & rng g c= rng f & ( for x being object st x in X holds
g . x = f . (x,y) ) )
let y be object ; :: thesis: for f being Function st [:X,Y:] <> {} & dom f = [:X,Y:] & y in Y holds
ex g being Function st
( (curry' f) . y = g & dom g = X & rng g c= rng f & ( for x being object st x in X holds
g . x = f . (x,y) ) )
let f be Function; :: thesis: ( [:X,Y:] <> {} & dom f = [:X,Y:] & y in Y implies ex g being Function st
( (curry' f) . y = g & dom g = X & rng g c= rng f & ( for x being object st x in X holds
g . x = f . (x,y) ) ) )
assume that
A1: [:X,Y:] <> {} and
A2: dom f = [:X,Y:] and
A3: y in Y ; :: thesis: ex g being Function st
( (curry' f) . y = g & dom g = X & rng g c= rng f & ( for x being object st x in X holds
g . x = f . (x,y) ) )
A4: dom (~ f) = [:Y,X:] by A2, FUNCT_4:46;
X <> {} by A1, ZFMISC_1:90;
then consider g being Function such that
A5: ( (curry (~ f)) . y = g & dom g = X & rng g c= rng (~ f) ) and
A6: for x being object st x in X holds
g . x = (~ f) . (y,x) by A3, A4, Th22;
take g ; :: thesis: ( (curry' f) . y = g & dom g = X & rng g c= rng f & ( for x being object st x in X holds
g . x = f . (x,y) ) )
rng (~ f) c= rng f by FUNCT_4:41;
hence ( (curry' f) . y = g & dom g = X & rng g c= rng f ) by A5; :: thesis: for x being object st x in X holds
g . x = f . (x,y)
let x be object ; :: thesis: ( x in X implies g . x = f . (x,y) )
assume A7: x in X ; :: thesis: g . x = f . (x,y)
then A8: g . x = (~ f) . (y,x) by A6;
[y,x] in dom (~ f) by A3, A4, A7, ZFMISC_1:87;
hence g . x = f . (x,y) by A8, FUNCT_4:43; :: thesis: verum