let X, Y, y be set ; :: 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 set 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 set st x in X holds
g . x = f . x,y ) ) )
assume A1: ( [:X,Y:] <> {} & dom f = [:X,Y:] & y in Y ) ; :: thesis: ex g being Function st
( (curry' f) . y = g & dom g = X & rng g c= rng f & ( for x being set st x in X holds
g . x = f . x,y ) )
then ( X <> {} & Y <> {} ) by ZFMISC_1:113;
then A2: ( [:Y,X:] <> {} & dom (~ f) = [:Y,X:] ) by A1, FUNCT_4:47;
then consider g being Function such that
A3: ( (curry (~ f)) . y = g & dom g = X & rng g c= rng (~ f) & ( for x being set st x in X holds
g . x = (~ f) . y,x ) ) by A1, Th36;
take g ; :: thesis: ( (curry' f) . y = g & dom g = X & rng g c= rng f & ( for x being set st x in X holds
g . x = f . x,y ) )
( curry' f = curry (~ f) & rng (~ f) c= rng f ) by FUNCT_4:42;
hence ( (curry' f) . y = g & dom g = X & rng g c= rng f ) by A3, XBOOLE_1:1; :: thesis: for x being set st x in X holds
g . x = f . x,y
let x be set ; :: thesis: ( x in X implies g . x = f . x,y )
assume x in X ; :: thesis: g . x = f . x,y
then ( g . x = (~ f) . y,x & [y,x] in dom (~ f) ) by A1, A2, A3, ZFMISC_1:106;
hence g . x = f . x,y by FUNCT_4:44; :: thesis: verum