A1: now

consider t being Element of dom (uncurry {});
assume dom (uncurry {}) <> {} ; :: thesis: contradiction
then ex x being set ex g being Function ex y being set st
( t = [x,y] & x in dom {} & g = {} . x & y in dom g ) by Def4;
hence contradiction ; :: thesis: verum

end;

hence uncurry {} = {} ; :: thesis: uncurry' {} = {}
thus uncurry' {} = {} by A1, Th1, RELAT_1:64; :: thesis: verum