let X, Y, Z be set ; 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; ( [: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:] <> {}
; ( 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)
; ( 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; verum