let f be Function; :: thesis: ( ( for x being set holds
( not x in dom f or not f . x is Function ) ) implies ( uncurry f = {} & uncurry' f = {} ) )
assume A1: for x being set holds
( not x in dom f or not f . x is Function ) ; :: thesis: ( uncurry f = {} & uncurry' f = {} )

A2: now

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

end;

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