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;