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 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 set st x in X holds
g . x = f . x,y ) )
A4: dom (~ f) = [:Y,X:] by A2, FUNCT_4:47;
X <> {} by A1, ZFMISC_1:113;
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 set st x in X holds
g . x = (~ f) . y,x by A3, A4, 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 ) )
rng (~ f) c= rng f by FUNCT_4:42;
hence ( (curry' f) . y = g & dom g = X & rng g c= rng f ) by A5, 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 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:106;
hence g . x = f . x,y by A8, FUNCT_4:44; :: thesis: verum