let X, Y be set ; :: thesis: for f being Function st dom f = [:X,Y:] holds
( rng (curry f) c= Funcs (Y,(rng f)) & rng (curry' f) c= Funcs (X,(rng f)) )
let f be Function; :: thesis: ( dom f = [:X,Y:] implies ( rng (curry f) c= Funcs (Y,(rng f)) & rng (curry' f) c= Funcs (X,(rng f)) ) )
assume A1: dom f = [:X,Y:] ; :: thesis: ( rng (curry f) c= Funcs (Y,(rng f)) & rng (curry' f) c= Funcs (X,(rng f)) )
A2: now :: thesis: ( [:X,Y:] <> {} implies ( rng (curry f) c= Funcs (Y,(rng f)) & rng (curry' f) c= Funcs (X,(rng f)) ) )
assume A3: [:X,Y:] <> {} ; :: thesis: ( rng (curry f) c= Funcs (Y,(rng f)) & rng (curry' f) c= Funcs (X,(rng f)) )
then A4: dom (curry f) = X by A1, Th17;
thus rng (curry f) c= Funcs (Y,(rng f)) :: thesis: rng (curry' f) c= Funcs (X,(rng f))
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng (curry f) or z in Funcs (Y,(rng f)) )
assume z in rng (curry f) ; :: thesis: z in Funcs (Y,(rng f))
then consider x being object such that
A5: x in dom (curry f) and
A6: z = (curry f) . x by FUNCT_1:def 3;
ex g being Function st
( (curry f) . x = g & dom g = Y & rng g c= rng f & ( for y being object st y in Y holds
g . y = f . (x,y) ) ) by A1, A3, A4, A5, Th22;
hence z in Funcs (Y,(rng f)) by A6, FUNCT_2:def 2; :: thesis: verum
end;
A7: dom (curry' f) = Y by A1, A3, Th17;
thus rng (curry' f) c= Funcs (X,(rng f)) :: thesis: verum
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng (curry' f) or z in Funcs (X,(rng f)) )
assume z in rng (curry' f) ; :: thesis: z in Funcs (X,(rng f))
then consider y being object such that
A8: y in dom (curry' f) and
A9: z = (curry' f) . y by FUNCT_1:def 3;
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) ) ) by A1, A3, A7, A8, Th25;
hence z in Funcs (X,(rng f)) by A9, FUNCT_2:def 2; :: thesis: verum
end;
end;
now :: thesis: ( dom f = {} implies ( rng (curry f) c= Funcs (Y,(rng f)) & rng (curry' f) c= Funcs (X,(rng f)) ) )
assume A10: dom f = {} ; :: thesis: ( rng (curry f) c= Funcs (Y,(rng f)) & rng (curry' f) c= Funcs (X,(rng f)) )
then ( X = {} or Y = {} ) by A1;
then A11: [:Y,X:] = {} by ZFMISC_1:90;
{} = dom (curry f) by A10, Def1, Th2;
then A12: rng (curry f) = {} by RELAT_1:42;
( dom (~ f) = [:Y,X:] & dom (curry (~ f)) = proj1 (dom (~ f)) ) by A1, Def1, FUNCT_4:46;
then rng (curry' f) = {} by A11, Th2, RELAT_1:42;
hence ( rng (curry f) c= Funcs (Y,(rng f)) & rng (curry' f) c= Funcs (X,(rng f)) ) by A12; :: thesis: verum
end;
hence ( rng (curry f) c= Funcs (Y,(rng f)) & rng (curry' f) c= Funcs (X,(rng f)) ) by A1, A2; :: thesis: verum