let x, y, w, z, a, b, c, d be set ; :: thesis: dom ((x,y,w,z) --> (a,b,c,d)) = {x,y,w,z}
set f = (x,y) --> (a,b);
set g = (w,z) --> (c,d);
A1: dom ((x,y) --> (a,b)) = {x,y} by FUNCT_4:62;
dom ((w,z) --> (c,d)) = {w,z} by FUNCT_4:62;
then (dom ((x,y) --> (a,b))) \/ (dom ((w,z) --> (c,d))) = {x,y,w,z} by A1, ENUMSET1:5;
hence dom ((x,y,w,z) --> (a,b,c,d)) = {x,y,w,z} by FUNCT_4:def 1; :: thesis: verum