let a, b, c, x, y, z, w, d be object ; :: 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 Th62;
dom ((w,z) --> (c,d)) = {w,z} by Th62;
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 Def1; :: thesis: verum