A1: now :: thesis: not dom (uncurry {}) <> {}
set t = the Element of dom (uncurry {});
assume dom (uncurry {}) <> {} ; :: thesis: contradiction
then ex x being object ex g being Function ex y being object st
( the Element of dom (uncurry {}) = [x,y] & x in dom {} & g = {} . x & y in dom g ) by Def2;
hence contradiction ; :: thesis: verum
end;
hence uncurry {} = {} ; :: thesis: uncurry' {} = {}
thus uncurry' {} = {} by A1, Th1, RELAT_1:41; :: thesis: verum