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)) & Funcs (Y,(rng f)) c= Funcs (Y,Z) ) by FUNCT_5:35, FUNCT_5:56;
then A3: rng (curry f) c= Funcs (Y,Z) ;
( rng (curry' f) c= Funcs (X,(rng f)) & Funcs (X,(rng f)) c= Funcs (X,Z) ) by A2, FUNCT_5:35, FUNCT_5:56;
then A4: rng (curry' f) c= Funcs (X,Z) ;
( dom (curry f) = X & dom (curry' f) = Y ) by A1, A2, FUNCT_5:24;
hence ( curry f in Funcs (X,(Funcs (Y,Z))) & curry' f in Funcs (Y,(Funcs (X,Z))) ) by A3, A4, FUNCT_2:def 2; :: thesis: verum