let I be set ; :: thesis: uncurry (I --> {}) = {}

per cases ( I = {} or I <> {} ) ;

suppose I = {} ; :: thesis: uncurry (I --> {}) = {}

hence uncurry (I --> {}) = {} by FUNCT_5:43; :: thesis: verum

end;

suppose I <> {} ; :: thesis: uncurry (I --> {}) = {}

then rng (I --> {}) = {{}} by FUNCOP_1:8
.= Funcs ({},{}) by FUNCT_5:57 ;
then dom (uncurry (I --> {})) = [:(dom (I --> {})),{}:] by FUNCT_5:26
.= {} by ZFMISC_1:90 ;
hence uncurry (I --> {}) = {} ; :: thesis: verum

end;

end;