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:33;
( rng (uncurry f) c= Z & rng (uncurry' f) c= Z ) by A1, FUNCT_5:48;
hence ( uncurry f in Funcs [:X,Y:],Z & uncurry' f in Funcs [:Y,X:],Z ) by A2, FUNCT_2:def 2; :: thesis: verum