let X, Y, Z be set ; :: thesis: for f being Function st [:X,Y:] <> {} & f in Funcs [:X,Y:],Z holds
( curry f in Funcs X,(Funcs Y,Z) & curry' f in Funcs Y,(Funcs X,Z) )
let f be Function; :: thesis: ( [:X,Y:] <> {} & f in Funcs [:X,Y:],Z implies ( curry f in Funcs X,(Funcs Y,Z) & curry' f in Funcs Y,(Funcs X,Z) ) )
assume A1: [:X,Y:] <> {} ; :: thesis: ( not f in Funcs [:X,Y:],Z or ( curry f in Funcs X,(Funcs Y,Z) & curry' f in Funcs Y,(Funcs X,Z) ) )
assume f in Funcs [:X,Y:],Z ; :: thesis: ( curry f in Funcs X,(Funcs Y,Z) & curry' f in Funcs Y,(Funcs X,Z) )
then A2: ex g being Function st
( f = g & dom g = [:X,Y:] & rng g c= Z ) by FUNCT_2:def 2;
then ( rng (curry f) c= Funcs Y,(rng f) & rng (curry' f) c= Funcs X,(rng f) & Funcs Y,(rng f) c= Funcs Y,Z & Funcs X,(rng f) c= Funcs X,Z ) by FUNCT_5:42, FUNCT_5:63;
then ( rng (curry f) c= Funcs Y,Z & rng (curry' f) c= Funcs X,Z & dom (curry f) = X & dom (curry' f) = Y ) by A1, A2, FUNCT_5:31, XBOOLE_1:1;
hence ( curry f in Funcs X,(Funcs Y,Z) & curry' f in Funcs Y,(Funcs X,Z) ) by FUNCT_2:def 2; :: thesis: verum