let X, Y, Z be set ; :: thesis: for f being Function st f in Funcs (X,(Funcs (Y,Z))) holds
( uncurry f in Funcs ([:X,Y:],Z) & uncurry' f in Funcs ([:Y,X:],Z) )
let f be Function; :: thesis: ( f in Funcs (X,(Funcs (Y,Z))) implies ( uncurry f in Funcs ([:X,Y:],Z) & uncurry' f in Funcs ([:Y,X:],Z) ) )
assume f in Funcs (X,(Funcs (Y,Z))) ; :: thesis: ( uncurry f in Funcs ([:X,Y:],Z) & uncurry' f in Funcs ([:Y,X:],Z) )
then A1: ex g being Function st
( f = g & dom g = X & rng g c= Funcs (Y,Z) ) by FUNCT_2:def 2;
then A2: ( dom (uncurry f) = [:X,Y:] & dom (uncurry' f) = [:Y,X:] ) by FUNCT_5:26;
( rng (uncurry f) c= Z & rng (uncurry' f) c= Z ) by A1, FUNCT_5:41;
hence ( uncurry f in Funcs ([:X,Y:],Z) & uncurry' f in Funcs ([:Y,X:],Z) ) by A2, FUNCT_2:def 2; :: thesis: verum