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

A2: now :: thesis: not dom (uncurry f) <> {}

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

end;

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